Abstract
Strong equivalence is one of the basic notions of equivalence that have been proposed for logic programs subject to the answer-set semantics. In this paper, we propose a new generalization of strong equivalence which takes the visibility of atoms into account and we characterize it in terms of revised SE-models. Our design resembles (relativized) strong equivalence but is essentially different due to the strict correspondence of models adopted from the notion of visible equivalence. We illustrate the use of visible strong equivalence when showing correct program transformations introducing lots of auxiliary atoms. Moreover, we present a translation which enables us to automate the task of verifying the visible strong equivalence of smodels programs having enough visible atoms.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
The support from the Finnish Centre of Excellence in Computational Inference Research (COIN) funded by the Academy of Finland (under grant #251170) is gratefully acknowledged.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Communications of the ACM 54(12), 92–103 (2011)
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1–4), 1–26 (2006)
Eiter, T., Fink, M.: Uniform Equivalence of Logic Programs under the Stable Model Semantics. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 224–238. Springer, Heidelberg (2003)
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)
Eiter, T., Fink, M., Woltran, S.: Semantical characterizations and complexity of equivalences in answer set programming. ACM Transactions on Computational Logic 8(3) (2007)
Eiter, T., Tompits, H., Woltran, S.: On solution correspondences in answer-set programming. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI 2005, pp. 97–102. Professional Book Center (2005)
Fink, M.: A general framework for equivalences in answer-set programming by countermodels in the logic of here-and-there. Theory and Practice of Logic Programming 11(2-3), 171–202 (2011)
Gebser, M., Kaufmann, B., Schaub, T.: The Conflict-Driven Answer Set Solver clasp: Progress Report. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 509–514. Springer, Heidelberg (2009)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proceedings of the 6th International Conference on Logic Programming, ICLP 1988, pp. 1070–1080 (1988)
Gelfond, M., Lifschitz, V.: Logic programs with classical negation. In: Proceedings of the 7th International Conference on Logic Programming, ICLP 1990, pp. 579–597 (1990)
Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 365–385 (1991)
Janhunen, T.: Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics 16(1–2), 35–86 (2006)
Janhunen, T., Niemelä, I.: Compact Translations of Non-disjunctive Answer Set Programs to Propositional Clauses. In: Balduccini, M., Son, T.C. (eds.) Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning. LNCS, vol. 6565, pp. 111–130. Springer, Heidelberg (2011)
Janhunen, T., Oikarinen, E.: Automated verification of weak equivalence within the Smodels system. Theory and Practice of Logic Programming 7(6), 697–744 (2007)
Janhunen, T., Oikarinen, E., Tompits, H., Woltran, S.: Modularity aspects of disjunctive stable models. Journal of Artificial Intelligence Research 35, 813–857 (2009)
Lifschitz, V.: Computing circumscription. In: Proceedings of the 9th International Joint Conference on Artificial Intelligence, Los Angeles, California, USA, pp. 121–127. Morgan Kaufmann (August 1985)
Lifschitz, V.: Answer set planning. In: Proceedings of the 16th International Conference on Logic Programming, ICLP 1999, pp. 23–37 (1999)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Transactions on Computational Logic 2(4), 526–541 (2001)
Lifschitz, V., Turner, H.: Splitting a logic program. In: Proceedings of the 11th International Conference on Logic Programming, ICLP 1994, Santa Margherita Ligure, Italy, pp. 23–37. MIT Press (1994)
Liu, L., Truszczynski, M.: Properties and applications of programs with monotone and convex constraints. Journal of Artificial Intelligence Research 27, 299–334 (2006)
McCarthy, J.: Applications of circumscription to formalizing commonsense knowledge. Artificial Intelligence 28, 89–116 (1986)
Oikarinen, E., Janhunen, T.: Achieving compositionality of the stable model semantics for smodels programs. Theory and Practice of Logic Programming 8(5-6), 717–761 (2008)
Pearce, D.: Equilibrium logic. Annals of Mathematics and Artificial Intelligence 47(1-2), 3–41 (2006)
Pührer, J., Tompits, H.: Casting Away Disjunction and Negation under a Generalisation of Strong Equivalence with Projection. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 264–276. Springer, Heidelberg (2009)
Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence 138(1-2), 181–234 (2002)
Turner, H.: Strong Equivalence for Logic Programs and Default Theories (Made Easy). In: Eiter, T., Faber, W., Truszczyński, M. (eds.) LPNMR 2001. LNCS (LNAI), vol. 2173, pp. 81–92. Springer, Heidelberg (2001)
Turner, H.: Strong equivalence made easy: nested expressions and weight constraints. Theory and Practice of Logic Programming 3(4-5), 609–622 (2003)
Woltran, S.: Characterizations for Relativized Notions of Equivalence in Answer Set Programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 161–173. Springer, Heidelberg (2004)
Woltran, S.: A common view on strong, uniform, and other notions of equivalence in answer-set programming. Theory and Practice of Logic Programming 8(2), 217–234 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Janhunen, T., Niemelä, I. (2012). Applying Visible Strong Equivalence in Answer-Set Program Transformations. In: Erdem, E., Lee, J., Lierler, Y., Pearce, D. (eds) Correct Reasoning. Lecture Notes in Computer Science, vol 7265. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30743-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-30743-0_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30742-3
Online ISBN: 978-3-642-30743-0
eBook Packages: Computer ScienceComputer Science (R0)