Deduction systems

by Rolf Socher-Ambrosius

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.