Deduction Systems /

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...

Full description

Bibliographic Details
Main Author: Socher-Ambrosius, Rolf
Corporate Author: SpringerLink (Online service)
Other Authors: Johann, Patricia
Format: eBook
Language:English
Published: New York, NY : Springer New York, 1997.
Series:Graduate texts in computer science.
Subjects:
Online Access:Connect to the full text of this electronic book
Description
Summary: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.
Item Description:Electronic resource.
Physical Description:1 online resource (xii, 206 pages 34 illustrations)
ISBN:9781461222668 (electronic bk.)
1461222664 (electronic bk.)
ISSN:1868-0941