Automated Deduction - A Basis for Applications

Bernhard Beckert and Reiner Haehnle

Analytic Tableaux

The aim of this chapter is twofold: first, introducing the basic
concepts of analytic tableaux and, secondly, presenting state-of-the-art
techniques for using non-clausal tableaux in automated deduction.

An important point involves problems arising with implementing tableaux,
in particular with designing a deterministic proof procedure (although
no concrete implementation is presented). The most important
optimizations of analytic tableaux are discussed; but there are too many
to give a complete list here. Instead, we present examples for the
important types of optimizations, and describe the general techniques
for proving soundness and completeness of different tableau variants.