Abstract
We apply tableau methods to the problem of computing entailment in the nonmonotonic system of equilibrium logic, a generalisation of the inference relation associated with the stable model and answer set semantics for logic programs. We describe tableau calculi for the nonclassical logics underlying equilibrium entailment, namely here-and-there with strong negation and its strengthening classical logic with strong negation. A further tableau calculus is then presented for computing equilibrium entailment. This makes use of a new method for reducing the complexity of the tableau expansion rules, which we call signing-up.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bonatti, P.A.: Sequent calculi for default and autoepistemic logics. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol. 1071, pp. 107–121. Springer, Heidelberg (1996)
Bonatti, P.A., Olivetti, N.: A sequent calculi for skeptical default logic. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS (LNAI), vol. 1227, pp. 127–142. Springer, Heidelberg (1997)
Brass, S, & Dix, J, Characterizations of the Disjunctive Stable Semantics by Partial Evaluation, J Logic Programming 32(3) (1997), pages 207{228.
Chagrov, A., Zakharyaschev, M.: Modal Logic. Clarendon Press, Oxford (1997)
van Dalen, D.: Intuitionistic Logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. III, pp. 225–340. Kluwer, Dordrecht (1986)
Gelfond, M., Lifschitz, V.: The Stable Model Semantics for Logic Programs. In: Bowen, K., Kowalski, R. (eds.) Proc 5th Int Conf on Logic Programming 2, pp. 1070–1080. MIT Press, Cambridge (1988)
Gelfond, M., Lifschitz, V.: Logic Programs with Classical Negation. In: Warren, D., Szeredi, P. (eds.) Proc ICLP 1990, pp. 579–597. MIT Press, Cambridge (1990)
Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 365–387 (1991)
Gödel, K.: Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien 69, 65–66 (1932)
Gurevich, Y.: Intuitionistic Logic with Strong Negation. Studia Logica 36, 49–59 (1977)
de Guzmán, P., Ojeda, I., Valverde, A.: Multiple-Valued Tableaux with Δ- reductions. In: Proceedings of IC-AI 1999, pp. 177–183. CSREA Press (1999)
Hähnle, R.: Towards an efficient tableau proof procedure for multiple-valued logics. In: Schönfeld, W., Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1990. LNCS, vol. 533, pp. 248–260. Springer, Heidelberg (1991)
Hähnle, R.: Automated Deduction in Multiple-valued Logics. Oxford University Press, Oxford (1993)
Heyting, A.: Die formalen Regeln der intuitionistischen Logik. Sitzung Preuss. Akad. Wiss. Phys. Math. Kl, 42–56 (1930)
Inoue, K., Koshimura, M., Hasegawa, R.: Embedding negation as failure into a model generation theorem prover. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 400–415. Springer, Heidelberg (1992)
Kracht, M, On Extensions of Intermediate Logics by Strong Negation, J Philosophical Logic 27, pages 49{73, 1998.
Leone, N., Rullo, P., Scarcello, F.: Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics, and Computation. Information and Computation 135(2), 69–112 (1997)
Lifschitz, V., Tang, L.R., Turner, H.: Nested expressions in logic programs, Annals of Mathematics and Artificial Intelligence (to appear)
Lukasiewicz, J.: Die Logik und das Grundlagenproblem.In: Les Entreties de Zürich sur les Fondaments et la Méthode des Sciences Mathématiques 12, 6–9 (1938); Zürich, pages 82–100, (1941)
Maksimova, L.: Craig’s interpolation theorem and amalgamable varieties. Doklady Akademii Nauk SSSR 237(6), 1281–1284 (1977); (translated as Soviet Math. Doklady)
Nelson, D.: Constructible Falsity. J Symbolic Logic 14, 16–26 (1949)
Niemelä, I.: A tableau calculus for minimal model reasoning. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D., et al. (eds.) TABLEAUX 1996. LNCS (LNAI), vol. 1071, pp. 278–294. Springer, Heidelberg (1996)
Niemelä, I.: Implementing Circumscription Using a Tableau Method. In: Proc European Conference on Artificial Intelligence, ECAI 1996, pp. 80–84. John Wiley, Chichester (1996)
Niemelä, I., Simons, P.: Efficient Implementation of the Well-founded and Stable Model Semantics. In: Proc JICSLP 1996, pp. 289–303. MIT Press, Cambridge (1996)
Ojeda, M., de Guzmán, P., Aguilera, I., Brewka, G., Valverde, A.: Reducing signed propositional formulas. Soft Computing 2(4), 157–166 (1998)
Olivetti, N.: A tableau and sequent calculus for minimal entailment. J Automated Reasoning 9, 99–139 (1992)
Olivetti, N.: Tableaux for nonmonotonic logics. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods. Kluwer, Dordrecht (1999)
Pearce, D.: A New Logical Characterisation of Stable Models and Answer Sets. In: Dix, J., Przymusinski, T.C., Moniz Pereira, L. (eds.) NMELP 1996. LNCS (LNAI), vol. 1216, pp. 57–70. Springer, Heidelberg (1997)
Pearce, D.: From Here to There: Stable Negation in Logic Programming. In: Gabbay, D., Wansing, H. (eds.) What is Negation?, pp. 161–181. Kluwer, Dordrecht (1999)
Przymusinski, T.: Stable Semantics for Disjunctive Programs. New Generation Computing 9, 401–424 (1991)
Rautenberg, W.: Klassische und Nichtklassische Aussagenlogik. Vieweg (1979)
Smetanich, Ya.S.: On Completeness of a Propositional Calculus with an additional Operation of One Variable (in Russian). Trudy Moscovskogo matrmaticheskogo obshchestva 9, 357–372 (1960)
Stuber, J.: Computing stable models by program transformation. In: Van Hentenryck, P. (ed.) Proc. ICLP 1994, pp. 58–73. MIT Press, Cambridge (1994)
Valverde, A.: Δ- Árboles de implicantes e implicados y reducciones de lógicas signadas en ATPs. PhD thesis. University of Málaga, Spain (July 1998)
Vorob’ev, N.N.: A Constructive Propositional Calculus with Strong Negation (in Russian). Doklady Akademii Nauk SSR 85, 465–468 (1952)
Vorob’ev, N.N.: The Problem of Deducibility in Constructive Propositional Calculus with Strong Negation (in Russian). Doklady Akademii Nauk SSR 85, 689–692 (1952)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pearce, D., de Guzmán, I.P., Valverde, A. (2000). A Tableau Calculus for Equilibrium Entailment. In: Dyckhoff, R. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000. Lecture Notes in Computer Science(), vol 1847. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722086_28
Download citation
DOI: https://doi.org/10.1007/10722086_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67697-3
Online ISBN: 978-3-540-45008-5
eBook Packages: Springer Book Archive