zbMATH — the first resource for mathematics

First-order logic and automated theorem proving. (English) Zbl 0692.68002
Texts and Monographs in Computer Science. New York etc.: Springer-Verlag. XIII, 242 p. DM 68.00 (1990).
This book is a good introduction to the theoretical aspects of automatic theorem proving of classical first-order logic. The text is intended mainly for computer scientists. As weapons of automatic theorem proving semantic tableaux as well as resolution are treated. Their soundness and completeness theorems are presented uniformly for the propositional and first-order cases with and without equality. Other proof procedures such as natural deduction and sequent calculus are also touched upon.
Reviewer: H.Nishimura

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations