Theorem proving for conditional logics: CondLean and GOALDUCK

References

• Artosi , A. , Governatori , G. and Rotolo , A. 2002 . Labelled Tableaux for Non-monotonic Reasoning: Cumulative Consequence Relations . Journal of Logic and Computation , 12 ( 6 ) : 1027 – 1060 .
   Web of Science ®Google Scholar
• Beckert , B. and Goré , R. Free Variable Tableaux for Propositional Modal Logics . Prooceedings of TABLEAUX 1997 (Automated Reasoning with Analytic Tableaux and Related Methods), vol. 1227 of LNAI . Edited by: Galmiche , D. May . pp. 91 – 106 . Pont-á-Mousson , , France : Springer-Verlag .
   Google Scholar
• Beckert , B. and Posegga , J. 1995 . leanTAP: Lean Tableau-based Deduction . Journal of Automated Reasoning , 15 ( 3 ) : 339 – 358 .
   Web of Science ®Google Scholar
• Chellas , B. F. 1975 . Basic Conditional logics . Journal of Philosophical Logic , 4 : 133 – 153 .
   Web of Science ®Google Scholar
• Costello , T. and McCarthy , J. 1999 . Useful Counterfactuals . ETAI (Electronic Transactions on Artificial Intelligence) , 3 : Section A
   Google Scholar
• Crocco , G. and del Cerro , L. F. 1995 . “ Structure, Consequence Relation and Logic ” . In What is a Logical System , Edited by: Gabbay , D. M. vol. 4 , 239 – 259 . Oxford University Press .
   Google Scholar
• Crocco , G. and Lamarre , P. On the Connection between Non-Monotonic Inference Systems and Conditional Logics . Proceedings of KR'92 (Principles of Knowledge Representation and Reasoning) . Edited by: Nebel , B. , Rich , C. and Swartout , W. R. October . pp. 565 – 571 . Cambridge , MA : Morgan Kaufmann .
   Google Scholar
• 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 . Journal of Symbolic Logic , 48 ( 1 ) : 1 – 20 .
   Web of Science ®Google Scholar
• Delgrande , J. P. 1987 . A First-order Conditional Logic for Prototypical Properties . Artificial Intelligence , 33 ( 1 ) : 105 – 130 .
   Web of Science ®Google Scholar
• Delgrande , J. P. and Groeneboer , C. 1990 . A General Approach for Determining the Validity of Commonsense Assertions Using Conditional Logics . International Journal of Intelligent Systems , 5 ( 5 ) : 505 – 520 .
   Web of Science ®Google Scholar
• Fitting , M. 1998 . leanTAP Revisited . Journal of Logic and Computation , 8 ( 1 ) : 33 – 47 .
   Web of Science ®Google Scholar
• Friedman , N. and Halpern , J. Y. 2001 . Plausibility measures and default reasoning . Journal of the ACM , 48 ( 4 ) : 648 – 685 .
   Web of Science ®Google Scholar
• Gabbay , D. M. 1996 . Labelled Deductive Systems (vol I) , Oxford University Press . Oxford Logic Guides
   Google Scholar
• Gabbay , D. M. , Giordano , L. , Martelli , A. , Olivetti , N. and Sapino , M. L. 2000a . Conditional Reasoning in Logic Programming . Journal of Logic Programming , 44 ( 1-3 ) : 37 – 74 .
   Google Scholar
• Gabbay , D. M. and Olivetti , N. 2000b . Goal-directed Proof Theory , Kluwer Academic Publishers .
   Google Scholar
• Gent , I. P. 1992 . A Sequent or Tableaux-style System for Lewis's Counterfactual Logic VC . Notre Dame Journal of Formal Logic , 33 ( 3 ) : 369 – 382 .
   Google Scholar
• Giordano , L. , Gliozzi , V. and Olivetti , N. 2002 . Iterated Belief Revision and Conditional Logic . Studia Logica , 70 ( 1 ) : 23 – 47 .
   Google Scholar
• Giordano , L. , Gliozzi , V. and Olivetti , N. 2005a . Weak AGM Postulates and Strong Ramsey Test: a logical formalization . Artificial Intelligence , 168 ( 1-2 ) : 1 – 37 .
   Web of Science ®Google Scholar
• Giordano , L. , Gliozzi , V. , Olivetti , N. and Pozzato , G. L. Analytic Tableaux for KLM Preferential and Cumulative Logics . Prooceedings of LPAR 2005 (12th Conference on Logic for Programming, Artificial Intelligence, and Reasoning), vol. 3835 of LNAI . Edited by: Sutcliffe , G. and Voronkov , A. December . pp. 666 – 6681 . Montego Bay , , Jamaica : Springer-Verlag .
   Google Scholar
• Giordano , L. , Gliozzi , V. , Olivetti , N. and Pozzato , G. L. Analytic Tableaux Calculi for KLM Rational Logic R . Proceedings of JELIA 2006 (10th European Conference on Logics in Artificial Intelligence), vol. 4160 of LNAI . Edited by: Fisher , M. , van der Hoek , W. , Konev , B. and Lisitsa , A. September . pp. 190 – 202 . Liverpool , , England : Springer-Verlag .
   Google Scholar
• Giordano , L. , Gliozzi , V. , Olivetti , N. and Schwind , C. Tableau Calculi for Preference-Based Conditional Logics . Proceedings of TABLEAUX 2003 (Automated Reasoning with Analytic Tableaux and Related Methods), vol. 2796 of LNAI . Edited by: Meyer , C. , Marta and Pirri , F. September . pp. 81 – 101 . Roma , , Italy : Springer .
   Google Scholar
• Giordano , L. , Gliozzi , V. , Olivetti , N. and Schwind , C. Extensions of Tableau Calculi for Preferencebased Conditional Logics . Proceedings of the 4th InternationalWorkshop on Methods for Modalities (M4M-4) . Edited by: Schlingloff , H. December . pp. 220 – 234 . Berlin , , Germany : Informatik-Bericht 194, Fraunhofer Institute FIRST .
   Google Scholar
• Giordano , L. and Schwind , C. 2004 . Conditional Logic of Actions and Causation . Artificial Intelligence , 157 ( 1-2 ) : 239 – 279 .
   Web of Science ®Google Scholar
• Grahne , G. 1998 . Updates and Counterfactuals . Journal of Logic and Computation , 8 ( 1 ) : 87 – 117 .
   Web of Science ®Google Scholar
• Kraus , S. , Lehmann , D. and Magidor , M. 1990 . Nonmonotonic Reasoning, Preferential Models and Cumulative Logics . Artificial Intelligence , 44 ( 1-2 ) : 167 – 207 .
   Web of Science ®Google Scholar
• Lamarre , P. A Tableaux Prover for Conditional Logics . Proceedings of KR'93 (Principles of Knowledge Representation and Reasoning) . pp. 572 – 580 .
   Google Scholar
• Lewis , D. 1973 . Counterfactuals , Basil Blackwell Ltd .
   Google Scholar
• Miller , D. , Nadathur , G. , Pfenning , F. and Scedrov , A. 1991 . Uniform Proofs as a Foundation for Logic Programming . In Annals of Pure and Applied Logic , 51 ( 1-2 ) : 125 – 157 .
   Web of Science ®Google Scholar
• Nute , D. 1980 . Topics in Conditional Logic , Dordrecht : Reidel .
   Google Scholar
• Olivetti , N. and Pozzato , G. L. CondLean: A Theorem Prover for Conditional Logics . Proceedings of TABLEAUX 2003 (Automated Reasoning with Analytic Tableaux and Related Methods), vol. 2796 of LNAI . Edited by: Cialdea Meyer , M. and Pirri , F. September . pp. 264 – 270 . Roma , , Italy : Springer .
   Google Scholar
• Olivetti , N. and Pozzato , G. L. CondLean 3.0: Improving CondLean for Stronger Conditional Logics . Proceedings of TABLEAUX 2005 (Automated Reasoning with Analytic Tableaux and Related Methods), vol. 3702 of LNAI . Edited by: Beckert , B. September . pp. 328 – 332 . Koblenz , , Germany : Springer-Verlag .
   Google Scholar
• Olivetti , N. and Pozzato , G. L. KLMLean 1.0: a Theorem Prover for Logics of Default Reasoning . Proceedings of the 4th International Workshop on Methods for Modalities (M4M-4) . Edited by: Schlingloff , H. December . pp. 235 – 245 . Berlin , , Germany : Informatik-Bericht 194, Fraunhofer Institute FIRST .
   Google Scholar
• Olivetti , N. , Pozzato , G. L. and Schwind , C. B. 2007 . A Sequent Calculus and a Theorem Prover for Standard Conditional Logics . ACM Transactions on Computational Logics (TOCL) ,
   Google Scholar
• Schwind , C. B. 1999 . Causality in Action Theories . Electronic Transactions on Artificial Intelligence (ETAI) , 3 : 27 – 50 .
   Google Scholar
• Smullyan , R. 1968 . First-Order Logic , Berlin : Springer-Verlag .
   Google Scholar
• Stalnaker , R. 1968 . “ A Theory of Conditionals ” . In Studies in Logical Theory, vol. 2 of Monograph Series, American Philosophical Quarterly , Edited by: Rescher , N. 98 – 112 . Oxford : Blackwell .
   Google Scholar
• Viganò , L. 2000 . Labelled Non-classical Logics , Dordrecht : Kluwer Academic Publishers .
   Google Scholar