HOL(y)Hammer: online ATP service for HOL Light
From MaRDI portal
Publication:2018657
DOI10.1007/S11786-014-0182-0zbMATH Open1322.68177arXiv1309.4962OpenAlexW2113065066WikidataQ59425180 ScholiaQ59425180MaRDI QIDQ2018657FDOQ2018657
Publication date: 25 March 2015
Published in: Mathematics in Computer Science (Search for Journal in Brave)
Abstract: HOL(y)Hammer is an online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system. The service allows its users to upload and automatically process an arbitrary formal development (project) based on HOL Light, and to attack arbitrary conjectures that use the concepts defined in some of the uploaded projects. For that, the service uses several automated reasoning systems combined with several premise selection methods trained on all the project proofs. The projects that are readily available on the server for such query answering include the recent versions of the Flyspeck, Multivariate Analysis and Complex Analysis libraries. The service runs on a 48-CPU server, currently employing in parallel for each task 7 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also available for local installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise and their solutions are discussed, and an initial account of using the system is given.
Full work available at URL: https://arxiv.org/abs/1309.4962
Recommendations
machine learningautomated theorem provinginteractive theorem provingHOL Lightformal proof assistantslarge-theory automated reasoning
Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence (68T35)
Cites Work
- MizAR 40 for Mizar 40
- MaLeCoP Machine Learning Connection Prover
- Title not available (Why is that?)
- PRocH: Proof Reconstruction for HOL Light
- 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
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- 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
- Sine Qua Non for Large Theory Reasoning
- Encoding Monomorphic and Polymorphic Types
- MetiTarski: An automatic theorem prover for real-valued special functions
- Lemma Mining over HOL Light
- Optimizing proof search in model elimination
- Scalable LCF-Style Proof Translation
- Large Formal Wikis: Issues and Solutions
- Formal Mathematics on Display: A Wiki for Flyspeck
- Using the TPTP Language for Writing Derivations and Finite Interpretations
- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Web interfaces for proof assistants
Cited In (31)
- Learning to Parse on Aligned Corpora (Rough Diamond)
- Solving modal logic problems by translation to higher-order logic
- Superposition with lambdas
- JEFL: joint embedding of formal proof libraries
- Formalizing Physics: Automation, Presentation and Foundation Issues
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
- Aligning concepts across proof assistant libraries
- Mining the Archive of Formal Proofs
- Making higher-order superposition work
- Superposition with lambdas
- Machine learning guidance for connection tableaux
- Title not available (Why is that?)
- Classification of alignments between concepts of formal mathematical systems
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- A formally verified abstract account of Gödel's incompleteness theorems
- Random Forests for Premise Selection
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Making higher-order superposition work
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Learning-assisted theorem proving with millions of lemmas
- Experiences from exporting major proof assistant libraries
- Hammering Floating-Point Arithmetic
- Making PVS accessible to generic services by interpretation in a universal format
- Machine Learning for Inductive Theorem Proving
- Theorem proving as constraint solving with coherent logic
- Higher-Order Modal Logics: Automation and Applications
- Hammer for Coq: automation for dependent type theory
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- System Description: E.T. 0.1
- Matching Concepts across HOL Libraries
Uses Software
This page was built for publication: HOL(y)Hammer: online ATP service for HOL Light
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2018657)
