By Gianluca Pozzato
Università di Torino
Novembre 2009
Abstract
This volume is focused on proof methods and theorem proving for Conditional and Preferential logics. Conditional logics are extensions of classical logic by means of a conditional operator, usually denoted as ⇒. Conditional logics have a long history, and recently they have found application in several areas of AI, including belief revision and update, the representation of causal inferences in action planning, the formalization of hypothetical queries in deductive databases. Conditional logics have been also applied in order to formalize nonmonotonic reasoning. The study of the relations between conditional logics and nonmonotonic reasoning has lead to the seminal work by Kraus, Lehmann, and Magidor, who have introduced the so called KLM framework. According to this framework, a defeasible knowledge base is represented by a finite set of conditional assertions of the form A |~ B, whose intuitive reading is “typically (normally), the A’s are B’s” or “B is a plausible conclusion of A”. The operator |~ is nonmonotonic in the sense that A |~ B does not imply A ∧ C |~ B. The logics of the KLM frameworkalso known as Preferential logicsallow to infer new conditional assertion from a given knowledge base.
In spite of their significance, very few deductive mechanisms and theorem provers have been developed for Conditional and Preferential logics. In this work we try to (partially) fill the existing gap by introducing proof methods (sequent and tableau calculi) for these logics, as well as theorem provers obtained by implementing the proposed calculi.