Abstract
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 first-order formulas in the Bernays-Schönfinkel fragment. We then employ a tableaux-based 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.
This work was supported by FWF under project P18019-N04 and the European Commission under projects IST-2001-37004 WASP and IST-2001-33570 INFOMIX.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365–385 (1991)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly Equivalent Logic Programs. ACM Transactions on Computational Logic 2, 526–541 (2001)
Turner, H.: Strong Equivalence Made Easy: Nested Expressions and Weight Constraints. Theory and Practice of Logic Programming 3, 602–622 (2003)
Lin, F.: Reducing Strong Equivalence of Logic Programs to Entailment in Classical Propositional Logic. In: Proc. KR 2002, pp. 170–176 (2002)
Eiter, T., Faber, W., Greco, G., Fink, M., Lembo, D., Tompits, H., Woltran, S.: Methods and Techniques for Query Optimization. TR D5.3, EC Project IST-2001-33570, INFOMIX (2004), Available at http://www.mat.unical.it/infomix/
Eiter, T., Fink, M., Tompits, H., Woltran, S.: Simplifying logic programs under uniform and strong equivalence. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 87–99. Springer, Heidelberg (2003)
Pearce, D., Tompits, H., Woltran, S.: Encodings for Equilibrium Logic and Logic Programs with Nested Expressions. In: Brazdil, P.B., Jorge, A.M. (eds.) EPIA 2001. LNCS (LNAI), vol. 2258, pp. 306–320. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eiter, T., Faber, W., Traxler, P. (2005). Testing Strong Equivalence of Datalog Programs – Implementation and Examples. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2005. Lecture Notes in Computer Science(), vol 3662. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11546207_42
Download citation
DOI: https://doi.org/10.1007/11546207_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28538-0
Online ISBN: 978-3-540-31827-9
eBook Packages: Computer ScienceComputer Science (R0)