Deduction Systems
By: by Rolf Socher-Ambrosius, Patricia Johann
Contributors: Johann, Patricia
Series: Graduate Texts in Computer Science; Graduate texts in computer science
Publisher: Springer New York
Published: 1997
Place of publication: New York, NY
Language: eng
Format: [electronic resource] /
Number of pages: 206
ISBN-13: 9781461274797; 9781461222668
Subjects: Information theory; Computer science
Description: This graduate-level text offers a theoretical treatment of the fundamental concepts and methods of automated deduction. By presenting an account which covers resolution theorem-proving in order-sorted first-order logic it 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 covered. Numerous examples are presented to illustrate the examples discussed. As a result students will find this a readily accessible introduction to this subject.
Notes: Online full text is restricted to subscribers.

Also available in print.

Mode of access: World Wide Web.
Table of contents: title: Contents: Mathematical Preliminaries; title: Syntax of first-order languages; title: Semantics of first-order languages; title: The Gentzen calculus G. Normal Forms and Herbrand's Theorem; title: Resolution and unification; title: Improved Deduction efficiency; title: Resolution in sorted logic.