Tableau calculus for preference-based conditional logics: PCL and its extensions

ABSTRACT

We present a tableau calculus for some fundamental systems of propositional conditional logics. We consider the conditional logics that can be characterized by preferential semantics (i.e., possible world structures equipped with a family of preference relations). For these logics, we provide a uniform completeness proof of the axiomatization with respect to the semantics, and a uniform labeled tableau procedure.

REFERENCES

• 1: Artosi, A., Governatori, G., and Rotolo, A. 2002. Labelled tableaux for non-monotonic reasoning: Cumulative consequence relations. J. Logic Comput. 12, 6, 1027--1060.
• 2: 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]
• 3: Broda, K., Gabbay, D., Lamb, L., and Russo, A. 2002. Labelled natural deduction for conditional logic of normality. Logic J. IGPL 10, 2, 123--163.
• 4: Buchheit, M., Donini, F. M., and Schaerf, A. 1993. Decidable reasoning in terminological knowledge representation systems. J. Artif. Int. Res. (JAIR) 1, 109--138.
• 5: Burgess, J. P. 1981. Quick completeness proofs for logics of conditionals. Notre Dame J. Formal Logic 22, 1, 76--84.
• 6: G. Crocco , L. Fariñas del Cerro, Structure, consequence relation and logic, What is a logical system?, Oxford University Press, Inc., New York, NY, 1994
• 7: G. Crocco , L. Fariñas Del Cerro , A. Herzig, Conditionals: from philosophy to computer science, Oxford University Press, Oxford, 1996
• 8: de Swart, H. C. M. 1983. A Gentzen-or Beth-type system, a practical decision procedure and a constructive completeness proof for the counterfactual logics VC and VCS. J. Symbol. Logic 48, 1, 1--20.
• 9: James P. Delgrande, A first-order conditional logic for prototypical properties, Artificial Intelligence, v.33 n.1, p.105-130, Sept. 1987 [doi>10.1016/0004-3702(87)90053-1]
• 10: Delgrande, J. P. and Groeneboer, C. 1990. A general approach for determining the validity of commonsense assertions using conditional logics. Int. J. Intell. Syst. 5, 5, 505--520.
• 11: Fitting, M. 1983. Proof Methods for Modal and Intuitionistic Logics. Synthese Library. D. Reidel.
• 12: Friedman, N. and Halpern, J. 1994. On the complexity of conditional logics. In Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning, 202--213.
• 13: Galles, D. and Pearl, J. 1998. An axiomatic characterization of causal counterfactuals. Found. Sci. 3, 1, 151--182.
• 14: Gent, I. P. 1992. A sequent or tableaux-style system for Lewis's counterfactual logic vc. Notre Dame J. Formal Logic 33, 3, 369--382.
• 15: M I Ginsberg , M L Ginsberg, Counterfactuals, Artificial Intelligence, v.30 n.1, p.35-80, Oct. 1986 [doi>10.1016/0004-3702(86)90067-6]
• 16: Giordano, L., Gliozzi, V., and Olivetti, N. 2002. Iterated belief revision and conditional logic. Studia Logica 70, 1, 23--47.
• 17: Laura Giordano , Valentina Gliozzi , Nicola Olivetti, Weak AGM postulates and strong Ramsey Test: a logical formalization, Artificial Intelligence, v.168 n.1, p.1-37, October 2005 [doi>10.1016/j.artint.2005.06.004]
• 18: Giordano, L., Gliozzi, V., Olivetti, N., and Pozzato, G. L. 2005b. 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.
• 19: 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.
• 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. 2005c. 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., 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: Laura Giordano , Camilla Schwind, Conditional logic of actions and causation, Artificial Intelligence, v.157 n.1-2, p.239-279, August 2004 [doi>10.1016/j.artint.2004.04.009]
• 24: Goré, R. 1999. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, Kluwer Academic Publishers, 297--396.
• 25: Grahne, G. 1998. Updates and counterfactuals. J. Logic Comput. 8, 1, 87--117.
• 26: Groeneboer, C. and Delgrande, J. P. 1988. Tableau-Based theorem proving in normal conditional logics. In Proceedings of the National Conference on Artificial Intelligence (AAAI), 171--176.
• 27: Katsuno, H. and Satoh, 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.
• 28: 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]
• 29: Lamarre, P. 1992. Etude des raisonnements non-monotones: Apports des logiques des conditionnels et des logiques modales. PhD thesis, Université Paul Sabatier, Toulouse.
• 30: Lamarre, P. 1993. A tableaux prover for conditional logics. In Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning, 572--580.
• 31: Lewis, D. 1973a. Causation. J. Philosophy 70, 556--567.
• 32: Lewis, D. 1973b. Counterfactuals. Basil Blackwell Ltd.
• 33: Lewis, D. 2000. Causation as influence. J. Philosophy 97, 181--197.
• 34: Makinson, D. 1993. Five faces of minimality. Studia Logica 52, 3, 339--379.
• 35: Nejdl, W. 1991. The P-Systems: A systematic classification of logics of nonmonotonicity. In Proceedings of the National Conference on Artificial Intelligence, 366--372.
• 36: Nute, D. 1980. Topics in conditional logic. Reidel, Dordrecht.
• 37: Nicola Olivetti , Gian Luca Pozzato , Camilla B. Schwind, A sequent calculus and a theorem prover for standard conditional logics, ACM Transactions on Computational Logic (TOCL), v.8 n.4, p.22-es, August 2007 [doi>10.1145/1276920.1276924]
• 38: Sheremet, M., Tishkovsky, D., Wolter, F., and Zakharyaschev, M. 2005. Comparative similarity, tree automata, and diophantine equations. In Proceedings of the 12th Conference on Logic for Programming, Artificial Intelligence, and Reasoning. 651--655.
• 39: Shoenfield, J. R. 1967. Mathematical Logic. Addison-Wesley, MA.
• 40: Stalnaker, R. 1968. A theory of conditionals. In Studies in Logical Theory, American Philosophical Quarterly, Monograph Series no. 2. Blackwell, Oxford, 98--112.

INDEX TERMS

General Terms:
Theory

Keywords:
Tableaux calculi, conditional logics