Thomas Eiter
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
Available for Download
pdf
a17-eiter-apndx.pdf (108.6 KB)
Online appendix to designing mediation for context-aware applications. The appendix supports the information on article a17.
- 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.Google Scholar
Cross Ref
- Anger, C., Konczak, K., and Linke, T. 2001. NoMoRe: A system for non-monotonic reasoning. In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), T. Eiter et al., Eds. vol. 2173. Springer Verlag, 406--410. Google ScholarDigital Library
- Barrington, D., Immerman, N., and Straubing, H. 1990. On uniformity within NC1. J. Comput. Syst. Sci. 41, 274--306. Google ScholarDigital Library
- Ben-Eliyahu, R. and Dechter, R. 1994. Propositional semantics for disjunctive logic programs. Annals Math. Artif. Intell. 12, 53--87.Google ScholarCross Ref
- Buntine, W. 1988. Generalised subsumption and its applications to induction and redundancy. Artif. Intell. 36, 2, 149--176. Google ScholarDigital Library
- Buss, S. 1987. The Boolean formula value problem is in ALOGTIME. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing. 123--131. Google ScholarDigital Library
- Cabalar, P. 2002. A three-valued characterization for strong equivalence of logic programs. In Proceedings of the 18th National Conference on Artificial Intelligence (AAAI). AAAI Press/MIT Press, Cambridge, MA, 106--111. Google ScholarDigital Library
- Cadoli, M. and Lenzerini, M. 1994. The complexity of propositional closed world reasoning and circumscription. J. Comput. Syst. Sci. 48, 2, 255--310. Google ScholarDigital Library
- Chaudhuri, S. and Vardi, M. Y. 1992. On the equivalence of recursive and nonrecursive datalog programs. In Proceedings of the 11th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS). ACM Press, New York, 55--66. Google ScholarDigital Library
- Cosmadakis, S. and Kanellakis, P. 1986. Parallel evaluation of recursive rule queries. In Proceedings of the 5th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS). ACM Press, New York, 280--293. Google ScholarDigital Library
- de Jongh, D. and Hendriks, L. 2003. Characterizations of strongly equivalent logic programs in intermediate logics. Theory Pract. Logic Program. 3, 3, 259--270. Google ScholarDigital Library
- Dimopoulos, Y., Nebel, B., and Koehler, J. 1997. Encoding planning problems in nonmonotonic logic programs. In Proceedings of the European Conference on Planning (ECP), S. Steel and R. Alami, Eds. Lecture Notes in Computer Science, vol. 1348. Springer Verlag, 169--181. Google ScholarDigital Library
- Eiter, T., Faber, W., Leone, N., Pfeifer, G., and Polleres, A. 2003. A logic programming approach to knowledge-state planning, II: The small DLVK system. Artif. Intell. 144, 1-2, 157--211. Google ScholarDigital Library
- Eiter, T., Faber, W., Leone, N., Pfeifer, G., and Polleres, A. 2004. A logic programming approach to knowledge-state planning: Semantics and complexity. ACM Trans. Comput. Logic 5, 2, 206--263. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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). Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Eiter, T., Gottlob, G., and Mannila, H. 1997. Disjunctive datalog. ACM Trans. Database Syst. 22, 3, 364--418. Google ScholarDigital Library
- Erdem, E., Lifschitz, V., Nakhleh, L., and Ringe, D. 2003. Reconstructing the evolutionary history of Indo-European languages using answer set programming. In Proceedings of the 5th International Symposium on Practical Aspects of Declarative Languages (PADL), V. Dahl and P. Wadler, Eds. Lecture Notes in Computer Science, vol. 2562. Springer Verlag, 160--176. Google ScholarDigital Library
- 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.Google Scholar
- Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Gen. Comput. 9, 365--385.Google ScholarDigital Library
- 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.Google Scholar
- Halevy, A. Y., Mumick, I. S., Sagiv, Y., and Shmueli, O. 2001. Static analysis in datalog extensions. J. ACM 48, 5, 971--1012. Google ScholarDigital Library
- Heljanko, K. and Niemelä, I. 2001. Bounded LTL model checking with stable models. In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), T. Eiter et al., Eds. Lecture Notes in Computer Science, vol. 2173. Springer Verlag, 200--212. Google ScholarDigital Library
- Immerman, N. 1999. Descriptive Complexity. Springer Verlag.Google Scholar
- Inoue, K. and Sakama, C. 1999. Updating extended logic programs through abduction. In Proceedings of the 5th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), M. Gelfond et al., Eds. Lecture Notes in Computer Science, vol. 1730. Springer Verlag, 147--161. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Kautz, H. and Selman, B. 1992. Planning as satisfiability. In Proceedings of the 10th European Conference on Artificial Intelligence (ECAI), B. Neumann, Ed. Wiley, 359--363. Google ScholarDigital Library
- Kowalski, V. 1968. The calculus of the weak “Law of Excluded Middle”. Math. USSR 8, 648--658.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Lifschitz, V., Pearce, D., and Valverde, A. 2001. Strongly equivalent logic programs. ACM Trans. Comput. Logic 2, 4, 526--541. Google ScholarDigital Library
- Lifschitz, V., Tang, L., and Turner, H. 1999. Nested expressions in logic programs. Annals Math. Artif. Intell. 25, 3-4, 369--389. Google ScholarDigital Library
- Lifschitz, V. and Turner, H. 1994. Splitting a logic program. In Proceedings of the 11th International Conference on Logic Programming (ICLP), P. Van Hentenryck, Ed. MIT-Press, Cambridge, MA, 23--38. Google ScholarDigital Library
- 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.Google Scholar
- Lin, F. and Zhao, Y. 2002. ASSAT: Computing answer sets of a logic program by SAT solvers. In Proceedings of the 18th National Conference on Artificial Intelligence (AAAI). AAAI Press /MIT Press, Cambridge, MA, 112--117. Google ScholarDigital Library
- 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.Google Scholar
- Maher, M. J. 1988. Equivalences of logic programs. In Foundations of Deductive Databases and Logic Programming, J. Minker. Morgan, Kauffman, San Fransico, CA, 627--658. Google ScholarDigital Library
- Minker, J., 1988. Foundations of Deductive Databases and Logic Programming. Morgan Kaufmann, San Fransico, CA. Google ScholarDigital Library
- Osorio, M., Navarro, J., and Arrazola, J. 2001. Equivalence in answer set programming. In Proceedings of the 11th International Workshop on Logic Based Program Synthesis and Transformation (LOPSTR), A. Pettorossi, Ed. Lecture Notes in Computer Science, vol. 2372. Springer Verlag, 57--75. Google ScholarDigital Library
- 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.Google Scholar
- Pearce, D., Tompits, H., and Woltran., S. 2001. Encodings for equilibrium logic and logic programs with nested expressions. In Proceedings of the 10th Portuguese Conference on Artificial Intelligence (EPIA), P. Brazdil and A. Jorge, Eds. Lecture Notes in Computer Science, vol. 2258. Springer Verlag, 306--320. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Przymusinski, T. 1991. Stable semantics for disjunctive programs. New Gen. Comput. 9, 401--424.Google ScholarDigital Library
- Sagiv, Y. 1988. Optimizing datalog programs. In Foundations of Deductive Databases and Logic Programming, J. Minker. Morgan, Kauffman, San Fransico, CA, 659--698. Google ScholarDigital Library
- Shmueli, O. 1993. Equivalence of datalog queries is undecidable. J. Logic Program. 15, 3, 231--242. Google ScholarDigital Library
- Simons, P., Niemelä, I., and Soininen, T. 2002. Extending and implementing the stable model semantics. Artif. Intell. 138, 1-2, 181--234. Google ScholarDigital Library
- 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.Google Scholar
- Turner, H. 2003. Strong equivalence made easy: Nested expressions and weight constraints. Theory Pract. Logic Programm. 3, 4-5, 602--622. Google ScholarDigital Library
- Turner, H. 2001. Strong equivalence for logic programs and default theories (made easy). In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), T. Eiter et al., Eds. Lecture Notes in Computer Science, vol. 2173. Springer Verlag, 81--92. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
Index Terms
- Semantical characterizations and complexity of equivalences in answer set programming
Recommendations
Equivalences in Answer-Set Programming by Countermodels in the Logic of Here-and-There
ICLP '08: Proceedings of the 24th International Conference on Logic ProgrammingIn Answer-Set Programming different notions of equivalence, such as the prominent notions of strong and uniform equivalence, have been studied and characterized by various selections of models in the logic of Here-and-There (HT). For uniform ...
A general framework for equivalences in answer-set programming by countermodels in the logic of here-and-there*
Different notions of equivalence, such as the prominent notions of strong and uniform equivalence, have been studied in Answer-Set Programming, mainly for the purpose of identifying programs that can serve as substitutes without altering the semantics, ...
A common view on strong, uniform, and other notions of equivalence in answer-set programming*
Logic programming under the answer-set semantics nowadays deals with numerous different notions of program equivalence. This is due to the fact that equivalence for substitution (known as strong equivalence) and ordinary equivalence are different ...
Comments