Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Principles of automated theorem proving
Duffy D., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471927846)
Date Reviewed: Sep 1 1992
The aim of this book is to serve both as an introduction to automated theorem proving (ATP) in first-order logic, and as a guide to current work on particular aspects of ATP. The intention is to give full details of the principles involved, whilst keeping the non-specialist in mind.…

There are two main themes in the book. The first concerns general techniques for performing proofs automatically, whilst the second concerns particular implemented systems to apply these techniques for specific purposes. With regard to the first theme the major approaches--natural deduction, sequentzen [sequent-calculi], resolution and the connection calculi--are discussed in detail.…Throughout this discussion an attempt is made to bring out the underlying relationships between these diverse approaches to proof. With regard to the second, three systems are described: Prolog, the Knuth-Bendix completion procedure and the Boyer-Moore theorem prover.…Prolog is related both to resolution and (cut-free) sequent calculi, whilst the distinct approaches to proof by induction applied by the Knuth-Bendix procedure and the Boyer-Moore system are shown to have fundamental connections.

--From the Preface

The author meets the aims set out in his preface. The brief introduction to first-order formal systems is sufficient to give the knowledgeable reader an idea of the notation used, while references to other texts serve to assist novices. The author’s practicality is characteristic of the text as a whole; he compares different forms of logical systems for their efficiency and ease of use. It is also instructive for the reader to see three ostensibly different systems compared and to have their similarities pointed out. The bibliography is up to date and comprehensive, and a number of illustrative exercises (some of which have solutions outlined) add to its usefulness. Perhaps all that is lacking is some discussion of material on computer-assisted proof as distinct from the automatically generated proof that is provided by the various logic for continuous functionals (LCF) systems, for instance. This area has wider applicability (and possibly wider utility) than ATP, and it would have been interesting to see the author’s views on this issue. Nonetheless, the book serves a useful purpose in combining a number of different systems in a single clear and unified exposition.

Reviewer:  Simon Thompson Review #: CR115808
Bookmark and Share
  Featured Reviewer  
 
Mechanical Theorem Proving (F.4.1 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Mechanical Theorem Proving": Date
Unification in primal algebras, their powers and their varieties
Nipkow T. (ed) Journal of the ACM 31(4): 742-776, 1984. Type: Article
Dec 1 1991
Resolution for some first-order modal systems
Cialdea M. Theoretical Computer Science 85(2): 213-229, 1991. Type: Article
Jul 1 1992
Proving refutational completeness of theorem-proving strategies
Hsiang J. (ed), Rusinowitch M. Journal of the ACM 38(3): 558-586, 1991. Type: Article
Jul 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy