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.