A sequent calculus and a theorem prover for standard conditional logics

ABSTRACT

In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a theorem prover in Prolog for these calculi.

REFERENCES

• 1: Artosi, A., Governatori, G., and Rotolo, A. 2002. Labelled tableaux for nonmonotonic reasoning: Cumulative consequence relations. J. Logic Comput. 12, 6, 1027--1060.
• 2: Bernhard Beckert , Rajeev Goré, Free Variable Tableaux for Propositional Modal Logics, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.91-106, May 13-16, 1997
• 3: Beckert, B. and Posegga, J. 1995. leantap: Lean tableau-based deduction. J. Automat. Reason. 15, 3, 339--358.
• 4: John Bell, The logic of nonmonotonicity (research note), Artificial Intelligence, v.41 n.3, p.365-374, Jan. 1990 [doi>10.1016/0004-3702(90)90048-5]
• 5: 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]
• 6: Chellas, B. F. 1975. Basic conditional logics. J. Phil. Logic 4, 133--153.
• 7: Costello, T. and McCarthy, J. 1999. Useful counterfactuals. Electron. Trans. AI 3, Section A.
• 8: 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
• 9: Crocco, G., del Cerro, L. F., and Herzig, A. 1995. Conditionals: From philosophy to computer science. In Studies in Logic and Computation, Oxford University Press.
• 10: Crocco, G. and Lamarre, P. 1992. On the connection between nonmonotonic inference systems and conditional logics. In Proceedings of the 3rd International Conference on Principles of Knowledge. Representation and Reasoning, B. Nebel and E. Sandewall Ed., 565--571.
• 11: 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. Symb. Logic 48, 1, 1--20.
• 12: 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]
• 13: James R. Delgrande, An approach to default reasoning based on a first-order conditional logic: revised report, Artificial Intelligence, v.36 n.1, p.63-90, August 1988 [doi>10.1016/0004-3702(88)90079-3]
• 14: Delgrande, J. P. and Groeneboer, C. 1990. A general approach for determining the validity of commonsense assertions using conditional logics. Int. J. Intel. Syst. 5, 5, 505--520.
• 15: Fitting, M. 1998. Leantap revisited. J. Logic Computa. 8, 1, 33--47.
• 16: Friedman, N. and Halpern, J. 1994. On the complexity of conditional logics. In Proceedings of the 4th International Conference Principles of Knowledge Representation and Reasoning. 202--213.
• 17: Plausibility measures and default reasoning, Journal of the ACM (JACM), v.48 n.4, p.648-685, July 2001 [doi>10.1145/502090.502092]
• 18: Gabbay, D. M. 1996. Labelled Deductive Systems. Oxford Logic Guides, vol i. Oxford University Press.
• 19: Gabbay, D. M., Giordano, L., Martelli, A., Olivetti, N., and Sapino, M. L. 2000. Conditional reasoning in logic programming. J. Logic Program. 44, 1-3, 37--74.
• 20: Dov M. Gabbay , Nicola Olivetti, Goal-directed proof theory, Kluwer Academic Publishers, Norwell, MA, 2000
• 21: Peter Gärdenfors , Hans Rott, Belief revision, Handbook of logic in artificial intelligence and logic programming (Vol. 4): epistemic and temporal reasoning, Oxford University Press, Oxford, 1995
• 22: 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.
• 23: 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]
• 24: Giordano, L., Gliozzi, V., and Olivetti, N. 2002. Iterated belief revision and conditional logic. Studia Logica 70, 1, 23--47.
• 25: 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]
• 26: Giordano, L., Gliozzi, V., Olivetti, N., and Pozzato, G. L. 2005. Analytic tableaux for klm preferential and cumulative logics. In Proceedings of 12th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'05). Lecture Notes in Artificial Intelligence, vol. 3835, Springer-Verlag, 666--681.
• 27: Giordano, L., Gliozzi, V., Olivetti, N., and Schwind, C. 2003. Tableau calculi for preference-based conditional logics. In Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX' 03). Lecture Notes in Artificial Intelligence, vol. 2796, Springer, 81--101.
• 28: 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]
• 29: Grahne, G. 1998. Updates and counterfactuals. J. Logic Comput. 8, 1, 87--117.
• 30: Hudelmaier, J. 1993. An O(n log n)-space decision procedure for intuitionistic propositional logic. J. Logic Comput. 3, 1, 63--75.
• 31: 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]
• 32: Lamarre, P. 1992. Etude des raisonnements non-monotones: Apports des logiques des conditionnels et des logiques modales. PhD thesis, Université Paul Sabatier, Toulouse.
• 33: Lamarre, P. 1993. A tableaux prover for conditional logics. In Proceedings of the 4th International Conference Principles of Knowledge Representation and Reasoning, 572--580.
• 34: 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]
• 35: Lewis, D. 1973. Counterfactuals. Basil Blackwell Ltd.
• 36: Lindstrom, S. and Rabinowicz, W. 1992. Belief revision, epistemic conditionals and the ramsey test. Synthese 91, 195--237.
• 37: Joshua S. Hodas , Dale Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation, v.110 n.2, p.327-365, May 1, 1994
• 38: Miller, D., Nadathur, G., Pfenning, F., and Scedrov, A. 1991. Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51, 1-2, 125--157.
• 39: Negri, S. 2005. Proof analysis in modal logic. J. Philos. Logic, To Appear.
• 40: Nute, D. 1980. Topics in Conditional Logic. Reidel, Dordrecht.
• 41: N. Obeid, Model-Based Diagnosis and Conditional Logic, Applied Intelligence, v.14 n.2, p.213-230, March-April 2001 [doi>10.1023/A:1008322227554]
• 42: Olivetti, N. and Pozzato, G. L. 2003. Condlean: A theorem prover for conditional logics. In Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'03). Lecture Notes in Artificial Intelligence, vol. 2796, Springer, 264--270.
• 43: Olivetti, N. and Pozzato, G. L. 2005. Condlean 3.0: Improving condlean for stronger conditional logics. In Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods, (TABLEAUX'05). Lecture Notes in Artificeal Intelligence, vol. 3702, Springer-Verlag, 338--332.
• 44: Olivetti, N., Pozzato, G. L., and Schwind, C. B. 2005. A sequent calculus and a theorem prover for standard conditional logics: Extended version. Tech. rep. 87/05, Dip. di Informatica, Università degli Studi di Torino, http://www.di.unito.it/~argo/biblio/publications.php?author=Pozzato.
• 45: Olivetti, N. and Schwind, C. B. 2000. Analytic tableaux for conditional logics. Tech. rep., University of Torino.
• 46: Nicola Olivetti , Camilla Schwind, A Calculus and Complexity Bound for Minimal Conditional Logic, Proceedings of the 7th Italian Conference on Theoretical Computer Science, p.384-404, October 04-06, 2001
• 47: Pozzato, G. L. 2003. Deduzione automatica per logiche condizionali: Analisi e sviluppo di un theorem prover. Tesi di laurea, Informatica, Università di Torino. http://www.di.unito.it/~pozzato/tesiPozzato.html.
• 48: Pym, D. J. and Harland, J. 1994. A uniform proof-theoretic investigation of linear logic programming. J. Logic Comput. 4, 2, 175--207.
• 49: Schwind, C. B. 1999. Causality in action theories. Electr. Trans. AI 3, A, 27--50.
• 50: Stalnaker, R. 1968. A theory of conditionals. In N. Rescher, Ed., Studies in Logical Theory, American Philosophical Quarterly, Monograph Series no.2, Blackwell, Oxford, 98--112.
• 51: A. S. Troelstra , H. Schwichtenberg, Basic proof theory, Cambridge University Press, New York, NY, 1996
• 52: Viganò, L. 2000. Labelled Nonclassical Logics. Kluwer Academic Publishers, Dordrecht.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Logic and constraint programming; Computational logic

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based); Logic programming

General Terms:
Languages, Theory

Keywords:
Analytic sequent calculi, automated deduction, conditional logics, labeled deductive systems, logic programming, proof theory