Logical Decision Procedures in Practice

The aim of these lectures is to give a clear and explicit overview of the most important decidable and undecidable problems in automated theorem proving. We put particular emphasis on practical algorithms that are useful in real{world problems, but we pay due attention to traditional theo-retical issues including the well{known limitative results (Godel's incompleteness theorem, Tarski's theorem on the undenability of truth etc.) Looking at the problem from both a theoretical and practical angle is quite instructive. It quite often happens that theoretical decision procedures have limited usefulness in practice (e.g. Tarski's original quantier elimination peocedure for real algebra), or conversely that apparently hopeless combinatorial explosions often fail to manifest themselves in many problems of real interest (e.g. in DPLL{based SAT checking). Towards the end of our lectures we will focus on a special topic that is of some interest to us: how can we implement decision methods so that they always produce proofs or certicates rather than merely a yes/no answer? Reading list For decidable subsets of pure rst{order logic, see Ackermann (1954) and Dreben and Goldfarb (1979). Decision procedures for particular theories, often based on quantier elimination, are give