Tutorial at TABLEAUX'99

Proof Confluent Tableau Calculi

Reiner Hähnle and Bernhard Beckert


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.


Additional Information

Maintainer: beckert@ira.uka.de
$Id: index.html,v 1.3 1999/05/31 15:07:26 beckert Exp $