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.

This book contains a revised and updated version of my Ph.D. dissertation, which has been awarded by the Italian Association for Logic Programming (GULP) with the “Marco Cadoli” prize, as one of the distinguished dissertations focused on computational logic discussed between 2007 and 2009. First of all, I want to express my gratitude to the members of GULP, in particular to Gianfranco Rossi, Alberto Pettorossi and Paolo Torroni, who have made this publication possible. I would also like to thank the board of trustees of the “Marco Cadoli” award: Agostino Dovier, Andrea Formisano, Enrico Pontelli and Giorgio Delzanno. Moreover, I am very grateful to the referees of my thesis: Rajeev Goré, Guido Governatori, Daniel Lehmann and Dale Miller, for their helpful comments and interesting suggestions, which have helped me a lot in improving the final version of this work.

I would like to thank all the members of the “Logic Programming and Automated Reasoning Group” of the Department of Computer Science of the University of Turin: Alberto Martelli, Maria Luisa Sapino, Matteo Baldoni, Cristina Baroglio, Elisa Marengo, Viviana Patti, and Claudio Schifanella. I want also to express my gratitude to Pietro Torasso, our Ph.D. Coordinator, for the time he has spent for me, especially during the last months of my Ph.D. program. I would also like to thank my friend Roberto Micalizio: he's a great researcher, and he is the best person I've ever met.

I can't find the right words to thank Laura Giordano and Nicola Olivetti for supporting me through the years of my Ph.D. program, and for dedicating me time and patience. Their enthusiasm and their constant encouragement have been fundamental for the realization of my thesis. I will always be in debt with Laura and Nicola: they are two wonderful persons, and I am so lucky to work with them. I want also to express my gratitude to Valentina Gliozzi for her essential suggestions, for sharing her knowledge with me, and moreover for her patience in tolerating my bad temper when we have worked together.

Finally, I would like to thank my parents, for helping and supporting me since I was born, and my wife Eleonora, for sharing with me every second of her life. And I would like to thank my sweet son Lorenzo, for asking me to play with him, for breaking my heart every time I have to leave home, for making me feel his hero.

November 2009

Gian Luca Pozzato