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 setest-1.0/src.
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 prog1.dl and
prog2.dl
se prog1.dl prog2.dl
generates out.1.tme and out.2.tme. If a refutation is found in out.1.tme and out.2.tme then prog1.dl and prog2.dl are strongly equivalent. So, call
darwin out.1.tme
darwin out.2.tme
if both calls yield a refutation, then prog1.dl and prog2.dl are strongly equivalent.
The script setest integrates the above steps, so calling
setest prog1.dl prog2.dl
yields either
prog1.dl and prog2.dl are strongly equivalent.
if prog1.dl and 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 setest-1.0/examples.
Strongly equivalent:
Not strongly equivalent:
Send an e-mail to Patrick Traxler. Put together "e0027287" and "student.tuwien.ac.at" with "@" in the middle.