Shallow Lazy Proofs

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

• Type: Conference
• Year: 2005
• Where: TPHOL
• Authors: Hasan Amjad
• Keywords: Artificial Intelligence, Fully-expansive Proof Reconstruction, Non-interactive Decision Procedures, Theorem Prover, TPHOL 2005