Testing Strong Equivalence of Datalog Programs - Implementation and Examples

In this work we describe a system for determining strong equivalence of disjunctive non-ground datalog programs under the stable model semantics. The problem is tackled by reducing it to the unsatisfiability problem of firstorder formulas in the Bernays-Sch¨onfinkel fragment. We then employ a tableauxbased theorem prover, which (unlike most other currently available provers) is guaranteed to terminate for these formulas. To the best of our knowledge, this is the first strong equivalence tester for disjunctive non-ground datalog.

• Type: Conference
• Year: 2005
• Where: LPNMR
• Authors: Thomas Eiter, Wolfgang Faber, Patrick Traxler
• Keywords: Disjunctive Non-ground Datalog, LPNMR 2005, Non-ground Datalog Programs, Strong Equivalence