Vladimir Lifschitz
Abstract
A logic program Π1 is said to be equivalent to a logic program Π2 in the sense of the answer set semantics if Π1 and Π2 have the same answer sets. We are interested in the following stronger condition: for every logic program, Π, Π1, ∪ Π has the same answer sets as Π2 ∪ Π. The study of strong equivalence is important, because we learn from it how one can simplify a part of a logic program without looking at the rest of it. The main theorem shows that the verification of strong equivalence can be accomplished by cheching the equivalence of formulas in a monotonic logic, called the logic of here-and-there, which is intermediate between classical logic and intuitionistic logic.
- BIBEL,W.AND EDER, E. 1993. A survey of logical calculi. In The Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger, and J. Robinson, Eds. Vol. 1. Oxford University Press, 67-182.]]Google Scholar
- ERDEM,E.AND LIFSCHITZ, V. 1999. Transformations of logic programs related to causality and planning. In Logic Programming and Non-monotonic Reasoning: Proc. Fifth Int'l Conf. (Lecture Notes in Artificial Intelligence 1730). 107-116.]] Google ScholarDigital Library
- GELFOND,M.AND LIFSCHITZ, V. 1988. The stable model semantics for logic programming. In Logic Programming: Proc. Fifth Int'l Conf. and Symp., R. Kowalski and K. Bowen, Eds. 1070-1080.]]Google Scholar
- GELFOND,M.AND LIFSCHITZ, V. 1991. Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 365-385.]]Google ScholarDigital Library
- GODEL, K. 1932. Zum intuitionistischen Aussagenkalk ul. Anzeiger der Akademie der Wissenschaften in Wien, 65-66. Reproduced in: Kurt Godel, Collected Works, Vol. 1, OUP, 1986.]]Google Scholar
- GUREVICH, Y. 1977. Intuitionistic logic with strong negation. Studia Logica 36, 49-59.]]Google ScholarCross Ref
- HEYTING, A. 1930. Die formalen Regeln der intuitionistischen Logik. Sitz. Berlin, 42-56.]]Google Scholar
- INOUE,K.AND SAKAMA, C. 1998. Negation as failure in the head. J. Logic Programming 35, 39-78.]]Google ScholarCross Ref
- KRACHT, M. 1998. On extensions of intermediate logics by strong negation. J. Philosophical Logic 27.]]Google Scholar
- LIFSCHITZ, V., TANG,L.R.,AND TURNER, H. 1999. Nested expressions in logic programs. Annals of Math. and Artificial Intelligence 25, 369-389.]] Google ScholarDigital Library
- LUKASIEWICZ, J. 1941. Die Logik und das Grundlagenproblem. In Les Entretiens de Zurich sue les Fondements et la methode des sciences mathematiques 1938.Zurich, 82-100.]]Google Scholar
- NELSON, D. 1949. Constructible falsity. J. Symb. Logic 14, 16-26.]]Google ScholarCross Ref
- PEARCE, D. 1997. A new logical characterization of stable models and answer sets. In Non-Monotonic Extensions of Logic Programming (Lecture Notes in Artificial Intelligence 1216), J. Dix, L. Pereira, and T. Przymusinski, Eds. Springer-Verlag, 57-70.]] Google ScholarDigital Library
- PEARCE, D. 1999. From here to there: Stable negation in logic programming. In What Is Negation?, D. Gabbay and H. Wansing, Eds. Kluwer.]]Google Scholar
- PEARCE,D.,DE GUZMAN, I., AND VALVERDE, A. 2000a. A tableau calculus for equilibrium entailment. In Proc. TABLEAUX-2000. 352-367.]] Google ScholarDigital Library
- PEARCE,D.,DE GUZMAN, I., AND VALVERDE, A. 2000b. Computing equilibrium models using signed formulas. In Proc. CL-2000. 688-702.]] Google ScholarDigital Library
- REITER, R. 1980. A logic for default reasoning. Artificial Intelligence 13, 81-132.]]Google ScholarDigital Library
- VOROB'EV, N. 1952a. Constructive propositional calculus with strong negation. Doklady Akademii Nauk SSSR 85, 465-468. In Russian.]]Google Scholar
- VOROB'EV, N. 1952b. The problem of deducibility in constructive propositional calculus with strong negation. Doklady Akademii Nauk SSSR 85, 689-692. In Russian.]]Google Scholar
- VOROB'EV, N. 1964. Constructive propositional calculus with strong negation. Transactions of Steklov's Institute 72, 195-227. In Russian.]]Google Scholar
Index Terms
- Strongly equivalent logic programs
Recommendations
Reducts of propositional theories, satisfiability relations, and generalizations of semantics of logic programs
Over the years, the stable-model semantics has gained a position of the correct (two-valued) interpretation of default negation in programs. However, for programs with aggregates (constraints), the stable-model semantics, in its broadly accepted ...
Propositional theories are strongly equivalent to logic programs
This paper presents a property of propositional theories under the answer sets semantics (called Equilibrium Logic for this general syntax): any theory can always be reexpressed as a strongly equivalent disjunctive logic program, possibly with negation ...
Disjunctive logic programs, answer sets, and the cut rule
AbstractIn Minker and Rajasekar (J Log Program 9(1):45–74, 1990), Minker proposed a semantics for negation-free disjunctive logic programs that offers a natural generalisation of the fixed point semantics for definite logic programs. We show that this ...
Reviews
Ralph Walter Wilkerson
This paper concerns logic programs with negation as failure, using the answer set semantics. Two logic programs, L1 and L2, are said to be equivalent if they have the same answer sets. This paper studies the following stronger condition: for every logic program L, L1 U L is equivalent to L2 U L, which is called strong equivalence. In their main theorem, the authors prove that the verification of strong equivalence can be done by checking the equivalence of formulas in a monotonic logic, called the logic of here-and-there. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments