Semantical characterizations and complexity of equivalences in answer set programming

ABSTRACT

In recent research on nonmonotonic logic programming, repeatedly strong equivalence of logic programs P and Q has been considered, which holds if the programs P∪R and Q∪R have the same answer sets for any other program R. This property strengthens the equivalence of P and Q with respect to answer sets (which is the particular case for R=∅), and has its applications in program optimization, verification, and modular logic programming. In this article, we consider more liberal notions of strong equivalence, in which the actual form of R may be syntactically restricted. On the one hand, we consider uniform equivalence where R is a set of facts, rather than a set of rules. This notion, which is well-known in the area of deductive databases, is particularly useful for assessing whether programs P and Q are equivalent as components of a logic program which is modularly structured. On the other hand, we consider relativized notions of equivalence where R ranges over rules over a fixed alphabet, and thus generalize our results to relativized notions of strong and uniform equivalence. For all these notions, we consider disjunctive logic programs in the propositional (ground) case as well as some restricted classes, providing semantical characterizations and analyzing the computational complexity. Our results, which naturally extend to answer set semantics for programs with strong negation, complement the results on strong equivalence of logic programs and pave the way for optimizations in answer set solvers as a tool for input-based problem solving.

REFERENCES

• 1: Alferes, J. J., Leite, J. A., Pereira, L. M., Przymusinska, H., and Przymusinski, T. C. 2000. Dynamic updates of non-monotonic knowledge bases. J. Logic Program. 45, 1-3, 43--70.
• 2: Christian Anger , Kathrin Konczak , Thomas Linke, NoMoRe: A System for Non-Monotonic Reasoning under Answer Set Semantics, Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, p.406-410, September 17-19, 2001
• 3: David A. Mix-Barrington , Neil Immerman , Howard Straubing, On uniformity within NC1, Journal of Computer and System Sciences, v.41 n.3, p.274-306, Dec. 1990 [doi>10.1016/0022-0000(90)90022-D]
• 4: Ben-Eliyahu, R. and Dechter, R. 1994. Propositional semantics for disjunctive logic programs. Annals Math. Artif. Intell. 12, 53--87.
• 5: Wray Buntine, Generalized subsumption and its applications to induction and redundancy, Artificial Intelligence, v.36 n.2, p.149-176, September 1988 [doi>10.1016/0004-3702(88)90001-X ]
• 6: S. R. Buss, The Boolean formula value problem is in ALOGTIME, Proceedings of the nineteenth annual ACM conference on Theory of computing, p.123-131, January 1987, New York, New York, United States [doi>10.1145/28395.28409]
• 7: Pedro Cabalar, A three-valued characterization for strong equivalence of logic programs, Eighteenth national conference on Artificial intelligence, p.106-111, July 28-August 01, 2002, Edmonton, Alberta, Canada
• 8: Marco Cadoli , Maurizio Lenzerini, The complexity of propositional closed world reasoning and circumscription, Journal of Computer and System Sciences, v.48 n.2, p.255-310, April 1994 [doi>10.1016/S0022-0000(05)80004-2]
• 9: Surajit Chaudhuri , Moshe Y. Vardi, On the equivalence of recursive and nonrecursive datalog programs, Proceedings of the eleventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.55-66, June 02-05, 1992, San Diego, California, United States [doi>10.1145/137097.137109]
• 10: S Cosmadakis , P Kanellakis, Parallel evaluation of recursive rule queries, Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.280-293, March 24-26, 1986, Cambridge, Massachusetts, United States [doi>10.1145/6012.15421]
• 11: Dick H. J. De Jongh , Lex Hendriks, Characterization of strongly equivalent logic programs in intermediate logics, Theory and Practice of Logic Programming, v.3 n.3, p.259-270, May 2003 [doi>10.1017/S147106840200159X]
• 12: Yannis Dimopoulos , Bernhard Nebel , Jana Koehler, Encoding Planning Problems in Nonmonotonic Logic Programs, Proceedings of the 4th European Conference on Planning: Recent Advances in AI Planning, p.169-181, September 24-26, 1997
• 13: Thomas Eiter , Wolfgang Faber , Nicola Leone , Gerald Pfeifer , Axel Polleres, A logic programming approach to knowledge-state planning, II: the DLV^k system, Artificial Intelligence, v.144 n.1-2, p.157-211, March 2003 [doi>10.1016/S0004-3702(02)00367-3]
• 14: Thomas Eiter , Wolfgang Faber , Nicola Leone , Gerald Pfeifer , Axel Polleres, A logic programming approach to knowledge-state planning: Semantics and complexity, ACM Transactions on Computational Logic (TOCL), v.5 n.2, p.206-263, April 2004 [doi>10.1145/976706.976708]
• 15: Eiter, T. and Fink, M. 2003a. Uniform equivalence of logic programs under the stable model semantics. In Proceedings of the 19th International Conference on Logic Programming (ICLP), C. Palamidessi, Ed. Lecture Notes in Computer Science, vol. 2916. Springer Verlag, 224--238.
• 16: Eiter, T. and Fink, M. 2003b. Uniform equivalence of logic programs under the stable model semantics. Tech. Rep. INFSYS RR-1843-03-08, Institut für Informationssysteme, Technische Universität Wien, Austria.
• 17: Eiter, T., Fink, M., Sabbatini, G., and Tompits, H. 2001. A framework for declarative update specifications in logic programs. In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), B. Nebel, Ed. Morgan Kaufmann, San Fransisco, CA; 649--654.
• 18: Eiter, T., Fink, M., Tompits, H., and Woltran, S. 2004a. On eliminating disjunctions in stable logic programming. In Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR), D. Dubois et al., Eds. AAAI Press, 447--458.
• 19: Eiter, T., Fink, M., Tompits, H., and Woltran, S. 2004b. Simplifying logic programs under uniform and strong equivalence. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), V. Lifschitz and I. Niemelä, Eds. Lecture Notes in Computer Science, vol. 2923. Springer Verlag, 87--99.
• 20: Eiter, T., Fink, M., Tompits, H., and Woltran, S. 2005. Strong and uniform equivalence in answer-set programming: Characterizations and complexity results for the non-ground case. Accepted for publication in the Proceedings of the 20th National Conference on Artificial Intelligence (AAAI).
• 21: Eiter, T. and Gottlob, G. 1995. On the computational cost of disjunctive logic programming: Propositional case. Annals Math. Artif. Intell. 15, 3/4, 289--323.
• 22: Thomas Eiter , Georg Gottlob , Heikki Mannila, Disjunctive datalog, ACM Transactions on Database Systems (TODS), v.22 n.3, p.364-418, Sept. 1997 [doi>10.1145/261124.261126]
• 23: Esra Erdem , Vladimir Lifschitz , Luay Nakhleh , Donald Ringe, Reconstructing the Evolutionary History of Indo-European Languages Using Answer Set Programming, Proceedings of the 5th International Symposium on Practical Aspects of Declarative Languages, p.160-176, January 13-14, 2003
• 24: Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the 5th International Conference on Logic Programming (ICLP), R. Kowalski and K. Bowen, Eds. MIT Press, Cambridge, MA, 1070--1080.
• 25: Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Gen. Comput. 9, 365--385.
• 26: Giorgini, P., Massacci, F., Mylopoulos, J., and Zannone, N. 2004. Requirements engineering meets trust management: Model, methodology, and reasoning. In Proceedings of the 2nd International Conference on Trust Management (iTrust). Lecture Notes in Computer Science, vol. 2995. Springer Verlag, 176--190.
• 27: Alon Y. Halevy , Inderpal Singh Mumick , Yehoshua Sagiv , Oded Shmueli, Static analysis in datalog extensions, Journal of the ACM (JACM), v.48 n.5, p.971-1012, September 2001 [doi>10.1145/502102.502104]
• 28: Keijo Heljanko , Ilkka Niemelä, Bounded LTL Model Checking with Stable Models, Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, p.200-212, September 17-19, 2001
• 29: Immerman, N. 1999. Descriptive Complexity. Springer Verlag.
• 30: Chiaki Sakama , Katsumi Inoue, Updating Extended Logic Programs through Abduction, Proceedings of the 5th International Conference on Logic Programming and Nonmonotonic Reasoning, p.147-161, December 02-04, 1999
• 31: Inoue, K. and Sakama, C. 2004. Equivalence of logic programs under updates. In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA), J. J. Alferes and J. A. Leite, Eds. Lecture Notes in Computer Science, vol. 3229. Springer Verlag, 174--186.
• 32: Janhunen, T. and Oikarinen, E. 2004. LPEQ and DLPEQ-Translators for automated equivalence testing of logic programs. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), V. Lifschitz and I. Niemelä, Eds. Lecture Notes in Computer Science, vol. 2923. Springer Verlag, 336--340.
• 33: Henry Kautz , Bart Selman, Planning as satisfiability, Proceedings of the 10th European conference on Artificial intelligence, p.359-363, August 1992, Vienna, Austria
• 34: Kowalski, V. 1968. The calculus of the weak “Law of Excluded Middle”. Math. USSR 8, 648--658.
• 35: Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., and Scarcello, F. 2002. The DLV system for knowledge representation and reasoning. Tech. Rep. cs.AI/0211004, arXiv.org. November. To appear in ACM Trans. Comput. Logic.
• 36: Lifschitz, V. 1999. Action languages, answer sets and planning. In The Logic Programming Paradigm -- A 25-Year Perspective, K. Apt et al., Eds. Springer Verlag, 357--373.
• 37: Vladimir Lifschitz , David Pearce , Agustín Valverde, Strongly equivalent logic programs, ACM Transactions on Computational Logic (TOCL), v.2 n.4, p.526-541, Oct. 2001 [doi>10.1145/383779.383783]
• 38: Vladimir Lifschitz , Lappoon R. Tang , Hudson Turner, Nested expressions in logic programs, Annals of Mathematics and Artificial Intelligence, v.25 n.3-4, p.369-389, 1999
• 39: Vladimir Lifschitz , Hudson Turner, Splitting a logic program, Proceedings of the eleventh international conference on Logic programming, p.23-37, August 1994
• 40: Lin, F. 2002. Reducing strong equivalence of logic programs to entailment in classical propositional logic. In Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning (KR), D. Fensel et al., Eds. Morgan Kaufmann, San Fransisco, CA, 170--176.
• 41: Fangzhen Lin , Yuting Zhao, ASSAT: computing answer sets of a logic program by SAT solvers, Eighteenth national conference on Artificial intelligence, p.112-117, July 28-August 01, 2002, Edmonton, Alberta, Canada
• 42: Linke, T., Tompits, H., and Woltran, S. 2004. On acyclic and head-cycle free nested logic programs. In Proceedings of the 20th International Conference on Logic Programming (ICLP), B. Demoen and V. Lifschitz, Eds. Lecture Notes in Computer Science, vol. 3132. Springer Verlag, 225--239.
• 43: M. J. Maher, Equivalences of logic programs, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 44: J. Minker, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 45: Mauricio Osorio , Juan A. Navarro , José Arrazola, Equivalence in Answer Set Programming, Selected papers from the 11th International Workshop on Logic Based Program Synthesis and Transformation, p.57-75, November 28-30, 2001
• 46: Pearce, D. 2004. Simplifying logic programs under answer set semantics. In Proceedings of the 20th International Conference on Logic Programming (ICLP), B. Demoen and V. Lifschitz, Eds. Lecture Notes in Computer Science, vol. 3132. Springer Verlag.
• 47: David Pearce , Hans Tompits , Stefan Woltran, Encodings for Equilibrium Logic and Logic Programs with Nested Expressions, Proceedings of the10th Portuguese Conference on Artificial Intelligence on Progress in Artificial Intelligence, Knowledge Extraction, Multi-agent Systems, Logic Programming and Constraint Solving, p.306-320, December 17-20, 2001
• 48: Pearce, D. and Valverde, A. 2004a. Synonymous theories in answer set programming and equilibrium logic. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI), R. L. de Mántaras and L. Saitta, Eds. IOS Press, Amsterdam, the Netherland, 388--392.
• 49: Pearce, D. and Valverde, A. 2004b. Uniform equivalence for equilibrium logic and logic programs. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), V. Lifschitz and I. Niemelä, Eds. Lecture Notes in Computer Science, vol. 2923. Springer Verlag, 194--206.
• 50: Provetti, A. and Son, T. C. 2001. Proceedings of the Spring Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning. AAAI Press.
• 51: Przymusinski, T. 1991. Stable semantics for disjunctive programs. New Gen. Comput. 9, 401--424.
• 52: Y. Sagiv, Optimizing datalog programs, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 53: Oded Shmueli, Equivalence of datalog queries is undecidable, Journal of Logic Programming, v.15 n.3, p.231-241, Feb. 1993 [doi>10.1016/0743-1066(93)90040-N ]
• 54: Patrik Simons , Ilkka Niemelá , Timo Soininen, Extending and implementing the stable model semantics, Artificial Intelligence, v.138 n.1-2, p.181-234, June 2002 [doi>10.1016/S0004-3702(02)00187-X ]
• 55: Subrahmanian, V. S. and Zaniolo, C. 1995. Relating stable models and AI planning domains. In Proceedings of the 12th International Conference on Logic Programming (ICLP), L. Sterling, Ed. MIT Press, Cambridge, MA, 233--247.
• 56: Hudson Turner, Strong equivalence made easy: nested expressions and weight constraints, Theory and Practice of Logic Programming, v.3 n.4, p.609-622, July 2003 [doi>10.1017/S1471068403001819]
• 57: Hudson Turner, Strong Equivalence for Logic Programs and Default Theories (Made Easy), Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, p.81-92, September 17-19, 2001
• 58: Woltran, S. 2004. Characterizations for relativized notions of equivalence in answer set programming. In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA), J. J. Alferes and J. A. Leite, Eds. Lecture Notes in Computer Science, vol. 3229. Springer Verlag, 161--173.
• 59: Zhang, Y. and Foo, N. Y. 1998. Updating logic programs. In Proceedings of the 13th European Conference on Artificial Intelligence (ECAI), H. Prade, Ed. Wiley, 403--407.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Nonmonotonic reasoning and belief revision; Logic programming

General Terms:
Theory

Keywords:
Answer set semantics, computational complexity, program optimization, stable models, strong equivalence, uniform equivalence