Abstract
Interactive proof assistants should verify the proofs they receive from automatic theorem provers. Normally this proof reconstruction takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: resolution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) examine it manually. Each step of a proof is justified by calling Hurd’s Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle’s axiomatic type classes.
This is a preview of subscription content, log in via an institution to check access.
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
Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (in press)
Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)
Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)
Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–321. Springer, Heidelberg (1999)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56–68 (September 2003)
Hurd, J.: Metis performance benchmarks (2004), http://gilith.com/software/metis/performance.html
Melham, T.F.: The HOL logic extended with quantification over type variables. Formal Methods in System Design 3(1-2), 7–24 (1994)
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) FLoC 2006 Workshop on Empirically Successful Computerized Reasoning. CEUR Workshop Proceedings, vol. 192, pp. 53–69 (2006)
Meng, J., Paulson, L.C.: Translating higher-order problems to first-order clauses. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) FLoC 2006 Workshop on Empirically Successful Computerized Reasoning. CEUR Workshop Proceedings, vol. 192, pp. 70–80 (2006)
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic (in press)
Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Information and Computation 204(10), 1575–1596 (2006)
Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 164–188. Cambridge University Press, Cambridge (1993)
Nipkow, T.: Structured Proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 259–278. Springer, Heidelberg (2003)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Norrish, M., Slind, K.: The HOL system description (2007), On the Internet at http://hol.sourceforge.net/
Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning 5(3), 363–397 (1989)
Paulson, L.C.: Organizing numerical theories using axiomatic type classes. Journal of Automated Reasoning 33(1), 29–49 (2004)
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2), 91–110 (2002)
Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004)
Sutcliffe, G., Schmidt, R., Schulz, S. (eds.): FLoC’06 Workshop on Empirically Successful Computerized Reasoning. CEUR Workshop Proceedings, vol. 192 (2006)
Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, vol. 112, pp. 201–215. IOS Press, Amsterdam (2004)
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: 16th AnnualSymposium on Principles of Programming Languages, pp. 60–76. ACM Press, New York (1989)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. ch. 27, vol. II, pp. 1965–2013. Elsevier Science, Amsterdam (2001)
Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paulson, L.C., Susanto, K.W. (2007). Source-Level Proof Reconstruction for Interactive Theorem Proving. In: Schneider, K., Brandt, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2007. Lecture Notes in Computer Science, vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-74591-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74590-7
Online ISBN: 978-3-540-74591-4
eBook Packages: Computer ScienceComputer Science (R0)