Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

37

TPHOL
2005
IEEE

favoriteEmaildiscussreport

102views Automated Reasoning» more TPHOL 2005»

Shallow Lazy Proofs

14 years 4 months ago

Shallow Lazy Proofs

Download www.cl.cam.ac.uk

We show that delaying fully-expansive proof reconstruction for non-interactive decision procedures can result in a more eﬃcient workﬂow. In contrast with earlier work, our approach to postponed proof does not require making deep changes to the theorem prover.

Hasan Amjad

Real-time Traffic

Artificial Intelligence | Fully-expansive Proof Reconstruction | Non-interactive Decision Procedures | Theorem Prover | TPHOL 2005 |

claim paper

Related Content

» A SingleStep TermGraph Reduction System for Proof Assistants

» Theorem Proving Using Lazy Proof Explication

» Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

» Refinement verification of the lazy caching algorithm

» Proofs Programs Processes

» Proof Tool Support for Explicit Strictness

» Proving Properties of Lazy Functional Programs with Sparkle

» Strictness Properties of Lazy Algebraic Datatypes

» Induction and Coinduction in Sequent Calculus

Post Info
More Details (n/a)

Added	25 Jun 2010
Updated	25 Jun 2010
Type	Conference
Year	2005
Where	TPHOL
Authors	Hasan Amjad

Comments (0)