A Brief Overview of HOL4
By Konrad Slind, Michael Norrish. International Conference on Theorem Proving in Higher Order Logics, 2008
355 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/402eef6a118dfe6c59e59decffd7964094faee93
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Jia Deng
- Markus Norman Rabe
- Christian Szegedy
- Mingzhe Wang
- Kshitij Bansal
- Sarah M. Loos
- Ilya Sutskever
- Cezary Kaliszyk
In Computational Theory and Mathematics
- Jia Deng
- Markus Norman Rabe
- Christian Szegedy
- Mingzhe Wang
- Kshitij Bansal
- Sarah M. Loos
- The mathlib Community
- Cezary Kaliszyk
Citations in the corpus
- Monte Carlo Connection Prover (2016, background): “In particular, the recent hammer integration of automated theorem provers (ATPs) such as E (Schulz 2013), Vampire (Kovács and Voronkov 2013), CVC4 (Barrett et al. 2011), leanCoP (Otten 2008), and interactive theorem provers (ITPs) such as Isabelle (Wenzel et al. 2008), HOL4 (Slind and Norrish 2008),”
- Learning to Prove Theorems by Learning to Generate Theorems (2020, background): “TacticToe (Gauthier et al., 2018), DeepHOL (Bansal et al., 2019a) and ASTactic (Yang & Deng, 2019) are learning-based theorem provers for the higher-order logic based on various interactive theorem provers, including HOL4 (Slind & Norrish, 2008), HOL Light (HOLLight, 2019) and Coq (Bertot & Cast ´ e”
- 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].”
- The lean mathematical library (2019, methodology): “A number of contemporary proof systems implement versions of simple type theory , among them HOL4 [55], HOL Light [35], and Isabelle/HOL [49].”
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “We are not aware of a comprehensive coverage of fundamental mathematics in Isabelle, HOL4, or Lean.”