A learning-based fact selector for Isabelle/HOL

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

zbMATH Keywords

machine learningproof assistantsautomatic theorem proversrelevance filtering

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05)

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

• Isabelle/HOL
• MPTP 0.2
• VAMPIRE
• Metis_
• Isar
• MoMM
• Mizar
• z3
• HOL Light
• CeTA
• Sledgehammer
• veriT
• MaSh
• CVC4
• E Theorem Prover
• Flyspeck
• MaLARea
• HOLyHammer
• Nominal Isabelle
• seL4
• BliStr
• kepler98
• Archive Formal Proofs
• AVATAR
• Jinja not Java

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