| Collation |
xii, 206 pages : illustrations ; 25 cm. |
|
text txt rdacontent |
|
unmediated n rdamedia |
|
volume nc rdacarrier |
| Series |
Graduate texts in computer science |
|
Graduate texts in computer science (Springer-Verlag New York Inc.)
|
| Bibliog. |
Includes bibliographical references (pages 199-200) and index. |
| Contents |
1. Introduction -- 2. Mathematical Preliminaries -- 3. Syntax of First-order Languages -- 4. Semantics of First-order Languages -- 5. The Gentzen Calculus G -- 6. Normal Forms and Herbrand's Theorem -- 7. Resolution and Unification -- 8. Improving Deduction Efficiency -- 9. Resolution in Sorted Logic. |
| Summary |
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. |
| Note |
Gift of Dr. Gary Jason. |
| Subject |
Automatic theorem proving.
|
| Alt Author |
Johann, Patricia.
|
| ISBN |
0387948473 (acid-free paper) |
|
9780387948478 (acid-free paper) |
|
