Tutorial at TABLEAUX'99
Proof Confluent Tableau Calculi
Reiner Hähnle and Bernhard Beckert
Abstract
A tableau calculus is proof confluent if every partial tableau proof for
an unsatisfiable formula can be extended to a closed tableau. A rule
application may be redundant but it can never prevent the construction
of a proof; there are no "dead ends" in the proof search. Proof
confluence is a prerequisite of (a) backtracking-free proof search and
(b) the generation of counter examples to non-theorems.
In this tutorial we discuss the role and perspectives of proof
confluent calculi in tableau-based theorem proving. For the sake of
simplicity the discussion focuses on clause tableaux.
Slides
Additional Information
- A two page abstract of the tutorial (as it appears in the proceedings of TABLEAUX).
- More information on topics covered in the first part of the tutorial can be found in the overview article
Tableaux and Connections by Reiner Hähnle, which is to appear in the Handbook of Automated Reasoning (Kluwer Academic Publishers).
- More information on topics covered in the second part of the tutorial can be found in the paper
Depth-first Proof Search without Backtracking for Free Variable Semantic Tableaux by Bernhard Beckert.
- The Handbook of Tableau Methods.
Edited by Marcello D'Agostino, Dov M. Gabbay, Reiner Hähnle, and Joachim Posegga.
Kluwer Academic Publishers, 1999.
... the first complete reference work focusing on Tableau Systems for logical applications ...
Maintainer: beckert@kit.edu
$Id: index.html,v 1.3 1999/05/31 15:07:26 beckert Exp $