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 illustrated
the concepts discussed. Students will find this a readily accessible
introduction to the subject.
[BIO] | [HOME]
| [PUBLICATIONS] | [GRANTS]