zbMATH — the first resource for mathematics

First-order logic and automated theorem proving. 2nd ed. (English) Zbl 0848.68101
Graduate Texts in Computer Science. New York, NY: Springer-Verlag. xvii, 326 p. (1996).
The second edition of this book is an update and a revision of its first edition (1990; Zbl 0692.68002). The book treats propositional logic, first-order logic and first-order logic with equality. For each of these, resolution and semantic tableau systems are presented as (refutation-based) proof procedures; also, soundness and completeness results of the theorem provers considered are established. Based on Robinson’s unification algorithm, implementations of semantic tableaux in Prolog are given, and similar implementations of resolution procedures are outlined as projects. Additional proof procedures are specified, e.g., axiom systems (Hilbert systems), natural deduction, and Gentzen sequents. For each level of logic considered in this book, the necessary semantical background is considered: Boolean valuations in the propositional case, models in the first-order case, and normal models in the first-order case with equality. Additionally, various fundamental formal properties are derived, e.g., for first-order logic the replacement and skolemization Theorem, Herbrand’s Theorem, Gentzen’s Theorem, the cut elimination Theorem, Craig’s interpolation Theorem, Beth’s definability Theorem, and Lyndon’s homomorphism Theorem. Throughout the book, a system of uniform notation is used (following Smullyan).

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science
03B10 Classical first-order logic
03B35 Mechanization of proofs and logical operations