In this work I present CondLean, a theorem prover for the conditional logic CK and three standard extensions of it, namely CK+ID, CK+MP, and CK+MP+ID. CondLean is a SICStus Prolog implementation of some labelled sequent calculi for the logics above, and it is inspired by the lean methodology. CondLean also comprises a graphical user interface written in Java.

   Slides presented at TABLEAUX 2003

In this work I present CondLean 2.0, an improved version of CondLean, implementing some refinements of the sequent calculus which is the base of the theorem prover.

   Slides presented at UNILOG 2005

In this work I present CondLean 3.0, an improved version of CondLean supporting other conditional logics. In detail, CondLean is a theorem prover for the basic conditional logic CK and extensions with the axioms ID, MP, CS, and CEM. CondLean 3.0 also includes all the combinations of the above systems, except those combining both MP and CEM.

   Slides presented at TABLEAUX 2005

In this work I present KLMLean 1.0, a theorem prover for some logics of default reasoning, namely Preferential logic P and Loop-Cumulative logic CL. These logics belong to the KLM framework, where KLM stands for Kraus, Lehmann, and Magidor. KLMLean 1.0 is a SICStus Prolog implementation of some analytic tableau calculi for P and CL recently introduced. It is inspired to the lean methodology and also comprises a graphical user interface written in Java.

   Slides presented at M4M - 4 (short version)
   Slides presented at M4M - 4 (long version)

In this work I present a tableau calculus for the rational logic R of default reasoning, introduced by Kraus, Lehmann and Magidor. Our calculus is obtained by introducing suitable modalities to interpret conditional assertions, it makes use of labels to represent possible worlds, and it can be used to provide a decision procedure for R.

   Poster presented at ECAI 2006

In this work I present a tableau calculus for the rational logic R of default reasoning, introduced by Kraus, Lehmann and Magidor. Our calculus is obtained by introducing suitable modalities to interpret conditional assertions, and makes use of labels to represent possible worlds. We also provide a decision procedure for R, and study its complexity.

   Slides presented at JELIA 2006

In this work I focus on proof methods for conditional logics. We present US', a goal-directed calculus for the basic normal conditional logic CK and its standard extensions ID, MP, and ID+MP. US' is derived from some labelled sequent calculi, called SeqS', and it is based on the notion of uniform proofs. We also introduce GoalDUCK, a simple implementation of US' written in SICStus Prolog.

   Slides presented at CILC 2007

We present proof methods for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We introduce tableaux calculi (called TST) for all KLM logics. We provide decision procedures for KLM logics based on these calculi, and we study their complexity. Finally, we describe KLMLean 2.0, a theorem prover implementing the calculi TST inspired by the "lean" methodology. KLMLean 2.0 is implemented in SICStus Prolog and it also comprises a graphical interface written in Java.

   Slides presented at CILC 2007

I present KLMLean 2.0, a theorem prover for propositional KLM logics of nonmonotonic reasoning. KLMLean 2.0 implements some analytic tableaux calculi for these logics recently introduced. KLMLean 2.0 is inspired by the lean methodology, it is implemented in SICStus Prolog and it also contains a graphical interface written in Java.

   Slides presented at TABLEAUX 2007

Conditional and Preferential Logics have been applied in order to formalize nonmonotonic reasoning. In spite of their significance, very few proof methods have been proposed for these logics. In my PhD thesis, whose content is summarized in this paper, I have tried to partially overwhelm this gap, by introducing sequent and tableau calculi for Conditional and Preferential Logics.

   Slides presented at CILC 2008

In this work I extend the Description Logic ALC with a “typicality” operator T that allows us to reason about the prototypical properties and inheritance with exceptions. The resulting logic is called ALC + T. The typicality operator is intended to select the “most normal” or “most typical” instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form “T(C) is subsumed by P”, expressing that typical C-members have the property P. The semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus- Lehmann-Magidor axioms of preferential logic P. We first show that T enjoys a simple semantics provided by ordinary structures equipped by a preference relation. This allows us to obtain a modal interpretation of the typicality operator. Using such a modal interpretation, we present a tableau calculus for deciding satisfiability of ALC + T knowledge bases. Our calculus gives a nondeterministic-exponential time decision procedure for satisfiability of ALC + T. We then extend ALC + T knowledge bases by a nonmonotonic completion that allows inferring defeasible properties of specific concept instances.

   Slides presented at CILC 2008

In this work I propose a nonmonotonic extension ALC + T_min of the Description Logic ALC for reasoning about prototypical properties and inheritance with exception. The logic ALC + T_min is built upon a previously introduced (monotonic) logic ALC + T, that is obtained by adding a typicality operator T to ALC. The operator T is intended to select the “most normal” or “most typical” instances of a concept, so that knowledge bases may contain subsumption relations of the form “T(C) is subsumed by P”, expressing that typical C-members have the property P. In order to perform nonmonotonic inferences, we define a “minimal model” semantics ALC + T_min for ALC + T. The intuition is that preferred, or minimal models are those that maximise typical instances of concepts. By means of ALC + T_min we are able to infer defeasible properties of (explicit or implicit) individuals. We also present a tableau calculus for deciding ALC + T_min entailment.

   Slides presented at JELIA 2008