Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-25T04:58:14.743Z Has data issue: false hasContentIssue false
  • English
  • Français

Strong Equivalence and Program Structure in Arguing Essential Equivalence between Logic Programs

Published online by Cambridge University Press:  18 March 2022

YULIYA LIERLER Open the ORCID record for YULIYA LIERLER [Opens in a new window]
YULIYA LIERLER*
Affiliation:
University of Nebraska, 6001 Dodge St, Omaha, NE 68182, USA (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Answer set programming is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing different knowledge representation formalisms. Frequently, several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper presents formal results carefully relating a number of interesting program rewritings. It also provides the proof of correctness of system projector concerned with automatic program rewritings for the sake of efficiency.

Keywords

program analysisstrongessential equivalence
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 22 , Issue 3 , May 2022 , pp. 335 - 366
Check for updates
Copyright
© The Author(s), 2022. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

We are grateful to Pedro Cabalar, Jorge Fandinno, Nicholas Hippen, Vladimir Lifschitz, Miroslaw Truszczynski for valuable discussions on the subject of this paper. We are also thankful to the anonymous reviewers for their help to improve the presentation of the material in the paper. Yuliya Lierler was partially supported by the NSF 1707371 grant.

References

Babb, J. and Lee, J. 2013. Cplus 2asp: Computing action language c+ in answer set programming. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), P. Cabalar and T. C. Son, Eds. Springer Berlin Heidelberg, Berlin, Heidelberg, 122–134.Google Scholar
Ben-Eliyahu, R. and Dechter, R. 1994. Propositional semantics for disjunctive logic programs. Annals of Mathematics and Artificial Intelligence 12, 53–87.CrossRefGoogle Scholar
Bichler, M., Morak, M. and Woltran, S. 2016. lpopt: A rule optimization tool for answer set programming. In Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation.CrossRefGoogle Scholar
Brewka, G., Eiter, T. and Truszczyński, M. 2011. Answer set programming at a glance. Communications of the ACM 54(12), 92–103.CrossRefGoogle Scholar
Buddenhagen, M. and Lierler, Y. 2015. Performance tuning in answer set programming. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR).CrossRefGoogle Scholar
Eiter, T. and Fink, M. 2003. Uniform equivalence of logic programs under the stable model semantics. In Logic Programming, C. Palamidessi, Ed. Springer Berlin Heidelberg, Berlin, Heidelberg, 224–238.Google Scholar
Eiter, T., Fink, M., Tompits, H., Traxler, P. and Woltran, S. 2006a. Replacements in nonground answer-set programming. In Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR).Google Scholar
Eiter, T., Tompits, H. and Woltran, S. 2005. On solution correspondences in answer-set programming. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 97–102.Google Scholar
Eiter, T., Traxler, P. and Woltran, S. 2006b. An implementation for recognizing rule replacements in non-ground answer-set programs. In Proceedings of European Conference On Logics In Artificial Intelligence (JELIA).CrossRefGoogle Scholar
Erdoğan, S. T. and Lifschitz, V. 2004. Definitions in answer set programming. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), V. Lifschitz and I. NiemelÄ, Eds. Springer-Verlag, 114–126.Google Scholar
Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 119–131.CrossRefGoogle Scholar
Ferraris, P., Lee, J. and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence 175, 236–263.CrossRefGoogle Scholar
Ferraris, P., Lee, J., Lifschitz, V. and Palla, R. 2009. Symmetric splitting in the general theory of stable models. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI). IJCAI press, 797–803.Google Scholar
Ferraris, P. and Lifschitz, V. 2005. Weight constraints as nested expressions. Theory and Practice of Logic Programming 5, 45–74.CrossRefGoogle Scholar
Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V. and Schaub, T. 2015. Abstract gringo. Theory and Practice of Logic Programming 15, 449–463.CrossRefGoogle Scholar
Gelfond, M. and Kahl, Y. 2014. Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach. Cambridge University Press.CrossRefGoogle Scholar
Gelfond, M. and Lifschitz, V. 1998. Action languages (http://www.ep.liu.se/ea/cis/1998/016/). Electronic Transactions on Artificial Intelligence 3, 195–210.Google Scholar
Gelfond, M., Lifschitz, V., Przymusińska, H. and Truszczyński, M. 1991. Disjunctive defaults. In Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), J. Allen, R. Fikes and E. Sandewall, Eds., 230–237.Google Scholar
Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N. and Turner, H. 2004. Nonmonotonic causal theories. Artificial Intelligence 153(1–2), 49–104.CrossRefGoogle Scholar
Harrison, A. and Lierler, Y. 2016. First-order modular logic programs and their conservative extensions. In Theory and Practice of Logic programming, 32nd Int’l. Conference on Logic Programming (ICLP) Special Issue.CrossRefGoogle Scholar
Hippen, N. and Lierler, Y. 2019. Automatic program rewriting in non-ground answer set programs. In Proceedings of the 21st International Symposium on Practical Aspects of Declarative Languages (PADL).CrossRefGoogle Scholar
Janhunen, T., Oikarinen, E., Tompits, H. and Woltran, S. 2007. Modularity aspects of disjunctive stable models. In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 175–187.Google Scholar
Lee, J., Lifschitz, V. and Palla, R. 2008. A reductive semantics for counting and choice in answer set programming. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 472–479.Google Scholar
Lee, J., Lifschitz, V. and Yang, F. 2013. Action language bc: Preliminary report. In IJCAI, 983–989.Google Scholar
Leite, J. 2017. A bird’s-eye view of forgetting in answer-set programming. In Logic Programming and Nonmonotonic Reasoning, M. Balduccini and T. Janhunen, Eds. Springer International Publishing, Cham, 10–22.Google Scholar
Lierler, Y. 2019. Strong equivalence and program’s structure in arguing essential equivalence between first-order logic programs. In Proceedings of the 21st International Symposium on Practical Aspects of Declarative Languages (PADL).CrossRefGoogle Scholar
Lifschitz, V. 2016. Introduction to Mathematical Logic, Handout 4, Natural Deduction. URL: https://www.cs.utexas.edu/users/vl/teaching/388L/h4.pdf. [Accessed on August 2017].Google Scholar
Lifschitz, V., Morgenstern, L. and Plaisted, D. 2008. Knowledge representation and classical logic. In Handbook of Knowledge Representation, F. van Harmelen, V. Lifschitz and B. Porter, Eds. Elsevier, 3–88.CrossRefGoogle Scholar
Lifschitz, V., Pearce, D. and Valverde, A. 2001. Strongly equivalent logic programs. ACM Transactions on Computational Logic 2, 526–541.CrossRefGoogle Scholar
Lifschitz, V., Pearce, D. and Valverde, A. 2007. A characterization of strong equivalence for logic programs with variables. In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 188–200.Google Scholar
Lifschitz, V., Tang, L. R. and Turner, H. 1999. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence 25, 369–389.CrossRefGoogle Scholar
Lifschitz, V. and Turner, H. 1994. Splitting a logic program. In Proceedings of International Conference on Logic Programming (ICLP), P. Van Hentenryck, Ed. 23–37.Google Scholar
Lifschitz, V. and Turner, H. 1999. Representing transition systems by logic programs. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 92–106.Google Scholar
Linke, T., Tompits, H. and Woltran, S. 2004. On acyclic and head-cycle free nested logic programs. In Proceedings of 19th International Conference on Logic Programming (ICLP). 225–239.CrossRefGoogle Scholar
Lukasiewicz, J. 1941. Die logik und das grundlagenproblem. Les Entries de Zürich sur les Fondaments et la Méthode des Sciences Mathématiques 12, 6–9 (1938), 82–100.Google Scholar
Mints, G. 2000. A Short Introduction to Intuitionistic Logic. Kluwer.Google Scholar
Mints, G. 2010. Cut-free formulations for a quantified logic of here and there. Annals of Pure and Applied Logic 162, 3, 237–242. Special Issue: Dedicated to Nikolai Alexandrovich Shanin on the occasion of his 90th birthday.CrossRefGoogle Scholar
Oetsch, J. and Tompits, H. 2008. Program correspondence under the answer-set semantics: The non-ground case. In Logic Programming, M. Garcia de la Banda and E. Pontelli, Eds. Springer Berlin Heidelberg, Berlin, Heidelberg, 591–605.Google Scholar
Pearce, D. and Valverde, A. 2012. Synonymous theories and knowledge representations in answer set programming. Journal of Computer and System Sciences 78, 1, 86–104. JCSS Knowledge Representation and Reasoning.CrossRefGoogle Scholar
Woltran, S. 2004. Characterizations for relativized notions of equivalence in answer set programming. In Logics in Artificial Intelligence, J. J. Alferes and J. Leite, Eds. Springer Berlin Heidelberg, Berlin, Heidelberg, 161–173.Google Scholar
Woltran, S. 2008. 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.CrossRefGoogle Scholar
Supplementary material: File

Lierler supplementary material

Lierler supplementary material 1

Download Lierler supplementary material(File)
File 387.2 KB
Supplementary material: File

Lierler supplementary material

Lierler supplementary material 2

Download Lierler supplementary material(File)
File 41.9 KB
Supplementary material: File

Lierler supplementary material

Lierler supplementary material 3

Download Lierler supplementary material(File)
File 36.9 KB