In this work strong equivalence of disjunctive first order datalog programs under the stable model semantic is considered. The problem is reduced to the unsatisfiability problem of Bernays-Schoenfinkel formulas. An implementation is described in detail.
Complete work out: se.pdf, se.ps.
Download setest-1.0.tar.gz, unpack it, and call
make in the directory
Darwin is an automated theorem prover for first order logic. Instead of Darwin a theorem prover which supports
*.tme files as input can be used. But be aware that Darwin terminates for Bernays-Schoenfinkel formulas which is not true for most other theorem provers.
Two disjunctive datalog programs P and Q are strongly equivalent iff for all sets of rules R the programs (P union R) and (Q union R) are equivalent, i.e. iff they have the same stable models.
The input format is a subset of the DLV
syntax. See also http://www.dlvsystem.com
for DLV. For two programs
se prog1.dl prog2.dl
out.2.tme. If a refutation is found in
prog2.dl are strongly equivalent. So, call
if both calls yield a refutation, then
prog2.dl are strongly equivalent.
setest integrates the above steps, so calling
setest prog1.dl prog2.dl
prog1.dl and prog2.dl are strongly equivalent.
prog2.dl are strongly equivalent, or
prog1.dl and prog2.dl are NOT strongly equivalent.
if they are not strongly equivalent.
setest-1.0.tar.gz contains some examples in the directory
Not strongly equivalent:
Send an e-mail to Patrick Traxler. Put together "e0027287" and "student.tuwien.ac.at" with "@" in the middle.