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.
Shonda Terrill
Sky Bluethorne
Indie authors send us advance copies. We match them to readers by genre. You get the book free, the author gets an honest review.
