Tableaux Systems

Andreas Herzig

Logic, Interaction, Language, and Computation Group - IRIT - France

University Paul Sabatier

Tableaux systems are together with resolution procedures and sequent systems the main methods for automation of reasoning. They can be used both to construct proofs and to build models. Given a formula or a set thereof, a tableaux system uses a set of rules in order to build trees (or more generally graphs). Closure being defined as inconsistency in some node, a formula is inconsistent if all possible tablaux are closed.

For many logics there have been designed strategies which combine the rules in a way such that termination is guaranteed. For these logics construction of tableaux can be used as a decision procedure. Recently tableaux have found wide application as optimal decision procedures for description logics.

The course will treat the following topics:

- tableaux for classical propositional logic
- tableaux for first-order logic
- tableaux for modal logics and description logics
- tableaux for other nonclassical logics: intuitionistic, paraconsistent,
relevant logics
- combinations of tableaux and other reasoning methods
- implemented tableaux theorem provers: LWB, LoTREC, TWB