HOL(y)Hammer: online ATP service for HOL Light

DOI10.1007/s11786-014-0182-0zbMath1322.68177arXiv1309.4962OpenAlexW2113065066WikidataQ59425180 ScholiaQ59425180MaRDI QIDQ2018657

Josef Urban, Cezary Kaliszyk

Publication date: 25 March 2015

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1309.4962

zbMATH Keywords

machine learningautomated theorem provinginteractive theorem provingHOL Lightformal proof assistantslarge-theory automated reasoning

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence (68T35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Classification of alignments between concepts of formal mathematical systems, MizAR 40 for Mizar 40, JEFL: joint embedding of formal proof libraries, ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Mining the Archive of Formal Proofs, Formalizing Physics: Automation, Presentation and Foundation Issues, System Description: E.T. 0.1, Aligning concepts across proof assistant libraries, A learning-based fact selector for Isabelle/HOL, Hammer for Coq: automation for dependent type theory, Learning to Parse on Aligned Corpora (Rough Diamond), Making PVS accessible to generic services by interpretation in a universal format, Machine Learning for Inductive Theorem Proving, Solving modal logic problems by translation to higher-order logic, Random Forests for Premise Selection, Higher-Order Modal Logics: Automation and Applications, Unnamed Item, Learning-assisted theorem proving with millions of lemmas, Machine learning guidance for connection tableaux, Superposition with lambdas, Making higher-order superposition work, Making higher-order superposition work, Superposition with lambdas, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, A formally verified abstract account of Gödel's incompleteness theorems, Experiences from exporting major proof assistant libraries, Matching Concepts across HOL Libraries, Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description, Theorem proving as constraint solving with coherent logic

Uses Software

• MetiTarski
• ML
• VAMPIRE
• TPTP
• Metis_
• MoMM
• Mizar
• z3
• HOL
• HOL Light
• MaLeCoP
• E Theorem Prover
• PRocH
• Flyspeck
• MaLARea
• HOLyHammer
• BliStr

Cites Work

• Unnamed Item
• MizAR 40 for Mizar 40
• MetiTarski: An automatic theorem prover for real-valued special functions
• ATP and presentation service for Mizar formalizations
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• Translating higher-order clauses to first-order clauses
• Automated Reasoning Service for HOL Light
• Formal Mathematics on Display: A Wiki for Flyspeck
• Web Interfaces for Proof Assistants
• Lemma Mining over HOL Light
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• MaLeCoP Machine Learning Connection Prover
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
• Optimizing proof search in model elimination
• PRocH: Proof Reconstruction for HOL Light
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Sine Qua Non for Large Theory Reasoning
• Large Formal Wikis: Issues and Solutions
• Encoding Monomorphic and Polymorphic Types
• Scalable LCF-Style Proof Translation