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.