Deduction systems
By: Rolf Socher-Ambrosius, Patricia Johann.
Contributors: Johann, Patricia.
Series: Graduate texts in computer science; Graduate texts in computer science (Springer-Verlag New York Inc.)
Publisher: Springer
Published: 1997
Place of publication: New York
Language: eng
Number of pages: 206
Subjects: Automatic theorem proving.
Description: This graduate-level text offers a theoretical treatment of the fundamental concepts and methods of automated deduction. In a presentation of first-order resolution theorem proving that also covers resolution in order-sorted first-order logic, this book provides a self-contained account suitable for students coming to the subject for the first time.

Both Gentzen-style sequent calculi and the refutation method known as resolution are treated in detail. Various strategies for pruning resolution search spaces - such as linear, hyper- and ordered resolution - are also covered. Numerous examples are presented to illustrate the concepts discussed. Students will find this a readily accessible introduction to the subject.
Notes: Includes bibliographical references (p. [199]-200) and index.