A learning-based fact selector for Isabelle/HOL
From MaRDI portal
Publication:331617
DOI10.1007/s10817-016-9362-8zbMath1386.68149OpenAlexW2310495003WikidataQ108482139 ScholiaQ108482139MaRDI QIDQ331617
Jasmin Christian Blanchette, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban, David Greenaway
Publication date: 27 October 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://zenodo.org/record/1227195
Related Items
ENIGMA: efficient learning-based inference guiding machine, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Mining the Archive of Formal Proofs, Aligning concepts across proof assistant libraries, Hammer for Coq: automation for dependent type theory, CoProver: a recommender system for proof construction, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Hierarchical invention of theorem proving strategies, Hammering Mizar by Learning Clause Guidance (Short Paper)., A formal proof of the expressiveness of deep learning, TacticToe: learning to prove with tactics, Machine learning guidance for connection tableaux, A formal proof of the expressiveness of deep learning, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), Semantics of Mizar as an Isabelle object logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- MizAR 40 for Mizar 40
- Semi-intelligible Isar proofs from machine-generated proofs
- MPTP 0.2: Design, implementation, and initial experiments
- Lightweight relevance filtering for machine-generated resolution problems
- Isabelle/HOL. A proof assistant for higher-order logic
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Proof-Pattern Recognition and Lemma Discovery in ACL2
- System Description: E 1.8
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- Bridging the Gap: Automatic Verified Abstraction of C
- More SPASS with Isabelle
- AVATAR: The Architecture for First-Order Theorem Provers
- Three Chapters of Measure Theory in Isabelle/HOL
- Certification of Termination Proofs Using CeTA
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Sine Qua Non for Large Theory Reasoning
- Licensing the Mizar Mathematical Library
- Encoding Monomorphic and Polymorphic Types
- MaSh: Machine Learning for Sledgehammer
- Sledgehammer: Judgement Day
- General Bindings and Alpha-Equivalence in Nominal Isabelle
