×

zbMATH — the first resource for mathematics

HOL Light: an overview. (English) Zbl 1252.68255
Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 60-66 (2009).
Summary: HOL Light is an interactive proof assistant for classical higher-order logic, intended as a clean and simplified version of Mike Gordon’s original HOL system. Theorem provers in this family use a version of ML as both the implementation and interaction language; in HOL Light’s case this is Objective CAML (OCaml). Thanks to its adherence to the so-called ‘LCF approach’, the system can be extended with new inference rules without compromising soundness. While retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof tools and has been applied to some non-trivial tasks in the formalization of mathematics and industrial formal verification.
For the entire collection see [Zbl 1173.68002].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, London (1986) · Zbl 0617.03001
[2] Church, A.: A formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940) · Zbl 0023.28901 · doi:10.2307/2266170
[3] Diaconescu, R.: Axiom of choice and complementation. Proceedings of the American Mathematical Society 51, 176–178 (1975) · Zbl 0317.02077 · doi:10.1090/S0002-9939-1975-0373893-X
[4] Gordon, M.J.C.: Representing a logic in the LCF metalanguage. In: Néel, D. (ed.) Tools and notions for program construction: an advanced course, pp. 163–185. Cambridge University Press, Cambridge (1982)
[5] Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[6] Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979) · Zbl 0421.68039 · doi:10.1007/3-540-09724-4
[7] Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol. 05021. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2006)
[8] Hales, T.C.: The Jordan curve theorem, formally and informally. The American Mathematical Monthly 114, 882–894 (2007) · Zbl 1137.03305
[9] Harrison, J.: Proof style. In: Giménez, E., Paulin-Mohring, C. (eds.) TYPES 1996. LNCS, vol. 1512, pp. 154–172. Springer, Heidelberg (1998) · doi:10.1007/BFb0097791
[10] Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998); Revised version of author’s PhD thesis · doi:10.1007/978-1-4471-1591-5
[11] Harrison, J.: Floating-point verification using theorem proving. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol. 3965, pp. 211–242. Springer, Heidelberg (2006) · Zbl 1182.68120 · doi:10.1007/11757283_8
[12] Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102–118. Springer, Heidelberg (2007) · Zbl 1144.68357 · doi:10.1007/978-3-540-74591-4_9
[13] Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). Journal of Automated Reasoning (to appear, 2009) · Zbl 1185.68624 · doi:10.1007/s10817-009-9145-6
[14] Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge studies in advanced mathematics, vol. 7. Cambridge University Press, Cambridge (1986) · Zbl 0596.03002
[15] Loveland, D.W.: Mechanical theorem-proving by model elimination. Journal of the ACM 15, 236–251 (1968) · Zbl 0162.02804 · doi:10.1145/321450.321456
[16] Scott, D.: A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121, 411–440 (1993); Annotated version of a 1969 manuscript · Zbl 0942.68522 · doi:10.1016/0304-3975(93)90095-B
[17] Solovay, R.M., Arthan, R., Harrison, J.: Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904.3482 (2009); submitted to Annals of Pure and Applied Logic, http://arxiv.org/PS_cache/arxiv/pdf/0904/0904.3482v1.pdf · Zbl 1259.03020
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.