Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Data compression for proof replay
Amjad H. Journal of Automated Reasoning41 (3-4):193-218,2008.Type:Article
Date Reviewed: Aug 20 2009

Interactive theorem provers suffer from a disadvantage implied by the name: in the proof of a nontrivial theorem, manual guidance by the user is often required. By contrast, Boolean satisfiability (SAT) solvers are powerful tools for propositional logic that do not need manual guidance. In the area of formal verification, one can often reduce the given problem to a SAT problem. Thus, an interactive theorem prover that could take advantage of a SAT solver could potentially be a significant improvement.

This paper proposes a technique for doing this that does not involve embedding a SAT solver in the theorem prover. The idea is for the theorem prover to verify a proof generated by the SAT solver, thus avoiding soundness bugs in the SAT solver, amongst other issues that would arise if the result from the SAT solver were simply asserted as a theorem. However, more is needed if this idea is to be truly effective. The heart of the paper concerns the complex details of the translation of the SAT solver’s result into a form in which the theorem prover can speed up its verification of the proof. The author describes with illustrative examples the process whereby partial results from the SAT solver can be memoized--for example, the SAT solver will, in the course of its reasoning, find and refind a number of conflicts that cannot be satisfied.

Amjad provides enough background to make the paper reasonably self-contained. The experimental results show that the speedups obtained are significant.

Reviewer:  J. P. E. Hodgson Review #: CR137217 (1004-0398)
Bookmark and Share
  Featured Reviewer  
 
Mechanical Theorem Proving (F.4.1 ... )
 
 
Proof Theory (F.4.1 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Mathematical Logic (F.4.1 )
 
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
Principles of automated theorem proving
Duffy D., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471927846)
Sep 1 1992
Resolution for some first-order modal systems
Cialdea M. Theoretical Computer Science 85(2): 213-229, 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