Learning-assisted theorem proving with millions of lemmas

DOI10.1016/j.jsc.2014.09.032zbMath1315.68220arXiv1402.3578OpenAlexW2127812195WikidataQ35829526 ScholiaQ35829526MaRDI QIDQ485842

Josef Urban, Cezary Kaliszyk

Publication date: 14 January 2015

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

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

zbMATH Keywords

artificial intelligencemachine learningFlyspecklemma mining

Mathematics Subject Classification ID

Related Items (7)

A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Proof mining with dependent types ⋮ Aligning concepts across proof assistant libraries ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammer for Coq: automation for dependent type theory ⋮ Lemmatization for Stronger Reasoning in Large Theories ⋮ Higher-Order Modal Logics: Automation and Applications

Uses Software

• Isabelle
• MPTP
• VAMPIRE
• MoMM
• Mizar
• Prover9
• HOL Light
• Mace4
• Sledgehammer
• MaLeCoP
• MaSh
• E Theorem Prover
• PRocH
• Flyspeck
• MaLARea
• HOLyHammer
• E-MaLeS
• BliStr
• SRASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• MPTP-motivation, implementation, first experiments
• Lightweight relevance filtering for machine-generated resolution problems
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• ATP and presentation service for Mizar formalizations
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• Recording and analysing knowledge-based distributed deduction processes
• Translating higher-order clauses to first-order clauses
• Automated Reasoning Service for HOL Light
• Lemma Mining over HOL Light
• Automated and Human Proofs in General Mathematics: An Initial Comparison
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• MaLeCoP Machine Learning Connection Prover
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• The Isabelle Framework
• SRASS - A Semantic Relevance Axiom Selection System
• Optimizing proof search in model elimination
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• PRocH: Proof Reconstruction for HOL Light
• E-MaLeS 1.1
• Extending Sledgehammer with SMT Solvers
• Sine Qua Non for Large Theory Reasoning
• MaSh: Machine Learning for Sledgehammer
• Scalable LCF-Style Proof Translation

This page was built for publication: Learning-assisted theorem proving with millions of lemmas