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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amjad, H.: Programming a symbolic model checker in a fully expansive theorem prover. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 171–187. Springer, Heidelberg (2003)
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004)
Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)
Boulton, R.J.: Efficiency in a fully-expansive theorem prover. Technical report, University of Cambridge Computer Laboratory (1994)
Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5(2), 56–68 (1940)
de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438–455. Springer, Heidelberg (2002)
Gordon, M.J.C.: HolSatLib documentation (2002), http://www.cl.cam.ac.uk/users/mjcg/HolSatLib/HolSatLib.ps
Gordon, M.J.C.: Programming combinations of deduction and BDD-based symbolic calculation. LMS Journal of Computation and Mathematics 5, 56–76 (2002)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem-proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
Gordon, M.J.C., Milner, A.R.G., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)
Harrison, J.: Binary decision diagrams as a HOL derived rule. The Computer Journal 38(2), 162–170 (1995)
Harrison, J.: Private communication. See directory hol light/ Examples/holby.ml of the HOL Light distribution [14] (2005)
The HOL-4 Proof Tool. Tool URL (2003), http://hol.sf.net
The HOL Light Proof Tool. Tool URL (2005), http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)
Milner, A.R.G.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 348–375 (1978)
Milner, A.R.G., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML - Revised. MIT Press, Cambridge (May 1997)
Necula, G.C., Lee, P.: Proof generation in the Touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 25–44. Springer, Heidelberg (2000)
Sestoft, P.: Moscow ML (2003), http://www.dina.dk/~sestoft/mosml.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amjad, H. (2005). Shallow Lazy Proofs. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_3
Download citation
DOI: https://doi.org/10.1007/11541868_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)