Analytic tableaux calculi for KLM logics of nonmonotonic reasoning

ABSTRACT

We present tableau calculi for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative, and rational logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. We provide a decision procedure for the logics considered and we study their complexity.

REFERENCES

• 1: Arieli, O. and Avron, A. 2000. General patterns for nonmonotonic reasoning: From basic entailments to plausible relations. Logic J. IGPL 8, 2, 119--148.
• 2: Artosi, A., Governatori, G., and Rotolo, A. 2002. Labelled tableaux for non-monotonic reasoning: Cumulative consequence relations. J. Logic Comput. 12, 6, 1027--1060.
• 3: Arnon Avron, The method of hypersequents in the proof theory of propositional non-classical logics, Logic: from foundations to applications: European logic colloquium, Clarendon Press, New York, NY, 1996
• 4: Beckert, B. and Posegga, J. 1995. leantap: Lean tableau-based deduction. J. Automated Reasoning 15, 3, 339--358.
• 5: Beckert, B. and Posegga, J. 1996. Logic programming as a basis for lean automated deduction. J. Logic Program. 28, 3, 231--236.
• 6: Salem Benferhat , Didier Dubois , Henri Prade, Nonmonotonic reasoning, conditional objects and possibility theory, Artificial Intelligence, v.92 n.1-2, p.259-276, May 1997 [doi>10.1016/S0004-3702(97)00012-X]
• 7: S. Benferhat , A. Saffiotti , P. Smets, Belief functions and default reasoning, Artificial Intelligence, v.122 n.1-2, p.1-69, Sept., 2000 [doi>10.1016/S0004-3702(00)00041-2]
• 8: Craig Boutilier, Conditional logics of normality: a modal approach, Artificial Intelligence, v.68 n.1, p.87-154, July 1994 [doi>10.1016/0004-3702(94)90096-5]
• 9: Crocco, G. and Lamarre, P. 1992. On the connection between non-monotonic inference systems and conditional logics. In Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning, B. Nebel and E. Sandewall, Eds., 565--571.
• 10: Didier Dubois , Hélène Fargier , Patrice Perny, Qualitative decision theory with preference relations and comparative uncertainty: an axiomatic approach, Artificial Intelligence, v.148 n.1-2, p.219-260, August 2003 [doi>10.1016/S0004-3702(03)00037-7]
• 11: Didier Dubois , Hélène Fargier , Henri Prade , Patrice Perny, Qualitative decision theory: from savage's axioms to nonmonotonic reasoning, Journal of the ACM (JACM), v.49 n.4, p.455-495, July 2002 [doi>10.1145/581771.581772]
• 12: Fitting, M. 1998. leantap revisited. J. Logic Comput. 8, 1, 33--47.
• 13: Plausibility measures and default reasoning, Journal of the ACM (JACM), v.48 n.4, p.648-685, July 2001 [doi>10.1145/502090.502092]
• 14: Nir Friedman , Joseph Y. Halpern , Daphne Koller, First-order conditional logic for default reasoning revisited, ACM Transactions on Computational Logic (TOCL), v.1 n.2, p.175-207, Oct. 2000 [doi>10.1145/359496.359500]
• 15: D. Gabbay, Theoretical foundations for non-monotonic reasoning in expert systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 16: Gardenförs, P. 1988. Knowledge in Flux. MIT Press.
• 17: Giordano, L., Gliozzi, V., Olivetti, N., and Pozzato, G. L. 2005a. Analytic tableaux for KLM preferential and cumulative logics. In Proceedings of the 12th Conference on Logic for Programming, Artificial Intelligence, and Reasoning, G. Sutcliffe and A. Voronkov, Eds. Lecture Notes in Artificial Intelligence, vol. 3835. Springer, 666--681.
• 18: Giordano, L., Gliozzi, V., Olivetti, N., and Pozzato, G. L. 2006. Analytic tableaux calculi for KLM rational logic R. In Proceedings of the 10th European Conference on Logics in Artificial Intelligence, M. Fisher et al., Eds. Lecture Notes in Artificial Intelligence, vol. 4160. Springer, 190--202.
• 19: Giordano, L., Gliozzi, V., Olivetti, N., and Pozzato, G. L. 2007a. Tableau calculi for klm logics: extended version. Tech. Rep. 102/07, Dipartimento di Informatica, Università degli Studi di Torino. http://www.di.unito.it/~argo/papers/RT_10207.pdf.
• 20: Giordano, L., Gliozzi, V., Olivetti, N., and Schwind, C. 2003. Tableau calculi for preference-based conditional logics. In Proceedings of the Conference on Automated Reasoning with Analytic Tableaux and Related Methods, M. Cialdea Meyer and F. Pirri, Eds. Lecture Notes in Artificial Intelligence, vol. 2796. Springer, 81--101.
• 21: Giordano, L., Gliozzi, V., Olivetti, N., and Schwind, C. 2005b. Extensions of tableau calculi for preference-based conditional logics. In Proceedings of the 4th International Workshop on Methods for Modalities (M4M-4), H. Schlingloff, Ed. Informatik-Bericht 194, Fraunhofer Institute FIRST, Berlin, 220--234.
• 22: Laura Giordano , Valentina Gliozzi , Gian Luca Pozzato, KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning, Proceedings of the 16th international conference on Automated Reasoning with Analytic Tableaux and Related Methods, July 03-06, 2007, Aix en Provence, France [doi>10.1007/978-3-540-73099-6_19]
• 23: Alain Heuerding , Michael Seyfried , Heinrich Zimmermann, Efficient Loop-Check for Backward Proof Search in Some Non-classical Propositional Logics, Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, p.210-225, May 15-17, 1996
• 24: Hughes, G. and Cresswell, M. 1984. A Companion to Modal Logic. Methuen.
• 25: Katsuno, H. and Sato, K. 1991. A unified view of consequence relation, belief revision and conditional logic. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI'91), 406--412.
• 26: Sarit Kraus , Daniel Lehmann , Menachem Magidor, Nonmonotonic reasoning, preferential models and cumulative logics, Artificial Intelligence, v.44 n.1-2, p.167-207, July 1990 [doi>10.1016/0004-3702(90)90101-5]
• 27: Daniel Lehmann , Menachem Magidor, What does a conditional knowledge base entail?, Artificial Intelligence, v.55 n.1, p.1-60, May 1992 [doi>10.1016/0004-3702(92)90041-U]
• 28: Makinson, D. 2003. Bridges between classical and nonmonotonic logic. Logic J. IGPL 11, 1, 69--96.
• 29: Makinson, D. 2005. Bridges from Classical to Nonmonotonic Logic. Series: Texts in Computing, vol 5. King's College Publications, London.
• 30: Olivetti, N. and Pozzato, G. L. 2005. KLMLean 1.0: A theorem prover for logics of default reasoning. In Proceedings of the 4th International Workshop on Methods for Modalities (M4M-4), H. Schlingloff, Ed. Informatik-Bericht 194, Fraunhofer Institute FIRST, Berlin, 235--245.
• 31: Judea Pearl, System Z: a natural ordering of defaults with tractable applications to nonmonotonic reasoning, Proceedings of the 3rd conference on Theoretical aspects of reasoning about knowledge, March 04-07, 1990, Pacific Grove, California
• 32: Pozzato, G. L. 2007. Proof methods for conditional and preferential logics. Ph.D. thesis, Dipartimento di Informatica, Università degli Studi di Torino. http://www.di.unito.it/~argo/papers/2007_PhDpozzato.pdf.
• 33: Shoham, Y. 1987. A semantical approach to nonmonotonic logics. In Proceedings of the Conference on Logics in Computer Science, 275--279.
• 34: Emil Weydert, System JLZ: rational default reasoning by minimal ranking constructions, Journal of Applied Logic, v.1 n.3-4, p.273-308, June 2003 [doi>10.1016/S1570-8683(03)00016-8]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Languages, Theory

Keywords:
Analytic tableaux calculi, nonmonotonic reasoning