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`

.

- GNU C++ (http://gcc.gnu.org)
- flex, bison (http://www.gnu.org/software/flex/flex.html, http://www.gnu.org/software/bison/bison.html)
- Darwin (http://goedel.cs.uiowa.edu/Darwin/)

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:

- se.1.1.dl and se.1.2.dl
- se.2.1.dl and se.2.2.dl
- se.3.1.dl and se.3.2.dl
- se.4.1.dl and se.4.2.dl
- se.5.1.dl and se.5.2.dl
- constraints.1.dl and constraints.2.dl
- sagiv.1.dl and sagiv.2.dl (from the paper "Optimizing Datalog Programs" by Y. Sagiv, 1988)

Not strongly equivalent:

- nse.1.1.dl and nse.1.2.dl
- nse.2.1.dl and nse.2.2.dl
- nse.3.1.dl and nse.3.2.dl
- nse.4.1.dl and nse.4.2.dl

Send an e-mail to Patrick Traxler. Put together "e0027287" and "student.tuwien.ac.at" with "@" in the middle.