Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Cut elimination and automatic proof procedures
Zhang W. Theoretical Computer Science91 (2):265-284,1991.Type:Article
Date Reviewed: Apr 1 1993

The author discusses a simplified form of Gentzen’s sequential calculus as a basis for discussing proof procedures. He shows that the cut rule used in Gentzen’s approach, although redundant, can lead to much shorter proofs, or rather that eliminating the use of the cut rule from a proof results in an exponentially longer initial sequence.

He then goes on to point out that in resolution proofs, the cut rule appears in more than one guise. This can dramatically reduce the length of some proofs compared to the cut-free analysis trees in the Gentzen calculus. This reduction is not universal, however, especially if one applies refinement techniques (such as input resolution and linear resolution) to the general resolution method.

Zhang uses these results to discuss the efficiencies of mechanical proofs (using resolution or Bibel’s connection calculus) and those special proofs that are used by Prolog.

Reviewer:  Ranan Banerji Review #: CR116134
Bookmark and Share
 
Deduction And Theorem Proving (I.2.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Deduction And Theorem Proving": Date
Noninteractive zero-knowledge
Blum M., De Santis A., Micali S., Persiano G. SIAM Journal on Computing 20(6): 1084-1118, 1991. Type: Article
Jan 1 1993
A non-reified temporal logic
Bacchus F., Tenenberg J., Koomen J. Artificial Intelligence 52(1): 87-108, 1991. Type: Article
Oct 1 1992
Relative complexities of first order calculi
Eder E., Verlag Vieweg, Wiesbaden, Germany, 1992. Type: Book (9783528051228)
Oct 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