DIPARTIMENTO DI
INFORMATICA
Università di Torino | |

Gian Luca Pozzato
In this page you will find the slides I have presented at Conferences and Workshops
CondLean 2.0: a Theorem Prover for Standard Conditional Logics (UNILOG 2005) CondLean 3.0: Improving CondLean for Stronger Conditional Logics (TABLEAUX 2005) KLMLean 1.0: a Theorem Prover for Logics of Default Reasoning (M4M - 4) Automated Deduction for Logics of Default Reasoning (ECAI 2006) Analytic Tableau Calculi for KLM Rational Logic R (JELIA 2006) A Goal-Directed Calculus for Standard Conditional Logics (CILC 2007) KLM Logics of Nonmonotonic Reasoning: Calculi and Implementations (CILC 2007) KLMLean 2.0: a Theorem Prover for KLM Logics of Nonmonotonic Reasoning (TABLEAUX 2007) Proof Methods for Conditional and Preferential Logics of Nonmonotonic Reasoning (CILC 2008) ALC+T: Reasoning About Typicality in Description Logics (CILC 2008) Reasoning about typicality in preferential description logics (JELIA 2008)
presented at the
12th International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods (TABLEAUX 2003)Roma, Italy, 9-12 September 2003
In this work I present
Slides presented at TABLEAUX 2003
presented at the
1st World Conference and School on Universal Logic (UNILOG 2005)Montreux, Switzerland, March 26th-April 3rd 2005
In this work I present
Slides presented at UNILOG 2005
presented at the
14th International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods (TABLEAUX 2005)Koblenz, Germany, 14-17 September 2005
In this work I present
Slides presented at TABLEAUX 2005
presented at the
4th International Workshop on Methods for Modalities (M4M - 4)Fraunhofer Institute of Computer Architacture and Software Technology, Berlin - Adlershof, Germany, December 1-2 2005
In this work I present
Slides presented at M4M - 4 (short version) Slides presented at M4M - 4 (long version)
presented at the
17th European Conference on Artificial Intelligence
(ECAI 2006)Riva del Garda, Italy, August 28th - September 1st 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, 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
presented at the
10th European Conference on Logics in Artificial Intelligence (JELIA 2006)University of Liverpool, England, 13-15 September 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
presented at
22o Convegno Italiano di Logica Computazionale (CILC 2007)University of Messina, Italy, 21-22 June 2007. 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
presented at
22o Convegno Italiano di Logica Computazionale (CILC 2007)University of Messina, Italy, 21-22 June 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
presented at the
16th International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods (TABLEAUX 2007)Aix En Provence, France, 3-6 July 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
presented at
23o Convegno Italiano di Logica Computazionale (CILC 2008)University of Perugia, Italy, 10-12 July 2008. 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
presented at
23o Convegno Italiano di Logica Computazionale (CILC 2008)University of Perugia, Italy, 10-12 July 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
presented at the
11th European Conference on Logics in Artificial Intelligence (JELIA 2008)University of Dresden, Germany, 28 September-1 October 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 Back to Gian Luca Pozzato's home page |