A COMPUTATIONAL APPROACH TO CLASSICAL LOGICS AND CIRCUITS

The purpose of this book is to present the logical foundations of computer science: classical logics and logic circuits. Fundamental concepts and results of classical logics are introduced in a formal style and in an explicitly computational way. Applications to automated theorem proving in propositional logic and first-order logic are presented. The studied proof methods are: the resolution method, the semantic tableaux method and the sequent/anti-sequent calculi.