- 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 the 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.