Abstract
Two sets of rules are said to be strongly equivalent to each other if replacing one by the other within any logic program preserves the program’s stable models. The familiar characterization of strong equivalence of grounded programs in terms of the propositional logic of here-and-there is extended in this paper to a large class of logic programs with variables. This class includes, in particular, programs with conditional literals and cardinality constraints. The first-order version of the logic of here-and-there required for this purpose involves two additional non-intuitionistic axiom schemas.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
van Dalen, D.: Intuitionistic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Volume III: Alternatives in Classical Logic, D. Reidel, Dordrecht (1986)
De Jongh, D., Hendriks, L.: Characterization of strongly equivalent logic programs in intermediate logics. Theory and Practice of Logic Programming 3, 250–270 (2003)
Eiter, T., et al.: Strong and Uniform Equivalence in Answer-Set Programming: Characterizations and Complexity Results for the Non-Ground Case. In: KR 2005, AAAI Press, Menlo Park (2005)
Ferraris, P., Lee, J., Lifschitz, V.: A new perspective on stable models. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), pp. 372–379 (2007)
Ferraris, P.: Answer Sets for Propositional Theories. In: Baral, C., et al. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 119–131. Springer, Heidelberg (2005)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R., Bowen, K. (eds.) Proceedings of International Logic Programming Conference and Symposium, pp. 1070–1080 (1988)
Hosoi, T.: The axiomatization of the intermediate propositional systems s n of gödel. Journal of the Faculty of Science of the University of Tokyo 13, 183–187 (1996)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Transactions on Computational Logic 2, 526–541 (2001)
Lin, F.: Reducing Strong Equivalence of Logic Programs to Entailment in Classical Propositional Logic. In: Proc. KR’02, pp. 170–176 (2002)
Pearce, D.J., Valverde, A.: Towards a First Order Equilibrium Logic for Nonmonotonic Reasoning. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 147–160. Springer, Heidelberg (2004)
Pearce, D., Valverde, A.: A first order nonmonotonic extension of constructive logic. Studia Logica 80, 323–348 (2005)
Pearce, D., Valverde, A.: Quantified Equilibrium Logic and the First Order Logic of Here-and-There. Technical Report, Univ. Rey Juan Carlos (2006), available at http://www.satd.uma.es/matap/investig/tr/ma06_02.pdf
Pearce, D.: A new logical characterization of stable models and answer sets. In: Dix, J., Przymusinski, T.C., Moniz Pereira, L. (eds.) NMELP 1996. LNCS, vol. 1216, pp. 57–70. Springer, Heidelberg (1997)
Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence 138, 181–234 (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Lifschitz, V., Pearce, D., Valverde, A. (2007). A Characterization of Strong Equivalence for Logic Programs with Variables. In: Baral, C., Brewka, G., Schlipf, J. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2007. Lecture Notes in Computer Science(), vol 4483. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72200-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-72200-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72199-4
Online ISBN: 978-3-540-72200-7
eBook Packages: Computer ScienceComputer Science (R0)