# 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@ira.uka.de*

$Id: index.html,v 1.3 1999/05/31 15:07:26 beckert Exp $