Shallow lazy proofs

Abstract

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