Analytic Tableaux

Abstract

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 tableau calculi, 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.