Verification via Tableaux

We present a set of seminar notes on basic concepts and results on automated and semiautomated verification of correctness and validation of software systems (protocols) via the method of tableaux, often called semantic tableaux. Special emphasis is on comparison of various ways of formalization of the concept of a `proof ', on the example of the classical first-order logic. 1 Introduction Gentzen [5] proposed two distinct formalizations of deduction systems. Each of them in both classical and intuitionistic versions. Only one of them he called natural deduction. The second he called the logistic calculus. In this presentation we distinguish the second by calling it the sequent calculus. In a sense both formalizations are very close to each other. The tableaux [in English: tables] method is a version of the sequent calculus developed by Schutte [11] and [12], Beth [1], Hintikka [8], Smullyann [14], and others. Fundamental analogies and differences between these two proof mechanisms ar..