HOL Light: A Tutorial Introduction

By J. Harrison. 1996

Subfields: Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Program Analysis & Verification

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, methodology): “This can be achieved using specialized programming languages that facilitate the simulation of logical and mathematical thinking using a computer, such as Coq [20], Isabelle [21], HOL4 [22], Lean [23], Metamath [24] and Mizar [25].”
Autoformalization with Large Language Models (2022, methodology): “These projects relied on interactive theorem provers, such as Isabelle [50], Coq [11], HOL Light [22], and Lean [12], which are essentially programming languages that enable users to enter their statements and proofs in a formal language, and which can then be checked automatically for correctness.”
DeepMath - Deep Sequence Models for Premise Selection (2016, background): “ITP systems include HOL (Light) [15], Isabelle [37], Mizar [13], Coq [7], and ACL2 [23].”
History of Interactive Theorem Proving (2014, methodology): “This started with the ‘Mizar mode for HOL’ [Harrison, 1996b] and was followed by several other declarative languages for other systems [Syme, 1997; Wenzel, 1999; Zammit, 1999].”
Learning to Reason in Large Theories without Imitation (2019, background): “Mnih et al. [2013]) and it was demonstrated later in Silver et al.”
Holophrasm: a neural Automated Theorem Prover for higher-order logic (2016, methodology): “Large datasets of formal proofs include Metamath [1], the Mizar Mathematical Library [2], Flyspeck [3], the Archive of Formal Proofs [4], the Coq standard library [5], and the HOL Light library [6].”
Language Modeling for Formal Mathematics (2020, methodology): “We start with the HOList dataset [Bansal et al., 2019], which spans a wide range of mathematical topics, including topology, multivariate calculus, real and complex analysis, geometric algebra, and measure theory, formalized in the HOL Light proof assistant [Harrison, 1996].”
Mathematical Reasoning via Self-supervised Skip-tree Training (2020, methodology): “We start with the HOList dataset [Bansal et al., 2019], which spans a wide range of mathematical topics, including topology, multivariate calculus, real and complex analysis, geometric algebra, and measure theory, formalized in the HOL Light proof assistant [Harrison, 1996].”
Monte Carlo Connection Prover (2016, background): “Furthermore, all provers below use the same proof format as the leanCoP tactic described in (Kaliszyk et al. 2015) to automatically find proofs for HOL Light, therefore adapting the HOL Light proof tactic to use our Monte Carlo system should be straightforward.”
Developing Bug-Free Machine Learning Systems With Formal Mathematics (2017, methodology): “Our approach makes use of a tool called an interactive proof assistant (Gordon, 1979; Gordon & Melham, 1993; Harrison, 1996; Nipkow et al., 2002; Owre et al., 1992; Coq Development Team, 2015-2016; de Moura et al., 2015), which consists of (a) a programming language, (b) a language to state…”
Mechanized Metatheory for the Masses: The PoplMark Challenge (2005, background): “However, despite much encouraging progress in recent years and the availability of several mature tools (ACL2 [26], Coq [3], HOL [18], HOL Light [21], Isabelle [35], Lego [28], NuPRL [7], PVS [40], Twelf [42], etc.”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, methodology): “We executed them with HOL Light [10] and INT assistant.”
Monte Carlo Tableau Proof Search (2016, methodology): “…versions of Vampire [4] and research on the InstGen calculus in iProver [16], but also more practical improvements, such as more efficient and precise term indexing techniques [24], efficient non-clausal tableau proof search [20], or the use of machine learning for problem size reduction [12].”
HyperTree Proof Search for Neural Theorem Proving (2022, background): “DeepHOL [20] focuses on the HOL-Light environment [21].”