Machine Learning for Inductive Theorem Proving

DOI10.1007/978-3-319-99957-9_6MaRDI QIDQ6108816zbMATH OpenFDO

Authors Ya-Qing Jiang, Petros Papapanagiotou, Jacques D. Fleuriot

Publication date 30 June 2023

Published in Artificial Intelligence and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://www.research.ed.ac.uk/portal/en/publications/machine-learning-for-automated-inductive-theorem-proving(c8d4d86e-e71c-4e44-b121-a314097c4803).html

zbMATH Keywords

inductionlemma selectionmachine learningtheorem proving

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Machine learning for first-order theorem proving
• Theorem proving in large formal mathematics as an emerging AI field
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Learning-assisted theorem proving with millions of lemmas
• scientific article; zbMATH DE number 6528605

Cites work

• Automating Inductive Proofs Using Theory Exploration
• Conjecture synthesis for inductive theories
• Hammering towards QED
• HOL(y)Hammer: online ATP service for HOL Light
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Lightweight relevance filtering for machine-generated resolution problems
• MaSh: machine learning for Sledgehammer
• Optimizing proof search in model elimination
• Proof-pattern recognition and lemma discovery in ACL2
• Superposition with structural induction
• TacticToe: learning to reason with HOL4 tactics

Cited in

(16)

• Simple dataset for proof method recommendation in Isabelle/HOL
• Machine learning for first-order theorem proving
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Proof-pattern recognition and lemma discovery in ACL2
• MaLeCoP. Machine learning connection prover
• scientific article; zbMATH DE number 6528605 (Why is no real title available?)
• TacticToe: learning to reason with HOL4 tactics
• Learning domain knowledge to improve theorem proving
• Learning-assisted theorem proving with millions of lemmas
• Theorem proving in large formal mathematics as an emerging AI field
• scientific article; zbMATH DE number 6423829 (Why is no real title available?)
• Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
• Mining state-based models from proof corpora
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• Learning Proof Transformations and Its Applications in Interactive Theorem Proving
• Learning conjecturing from scratch

This page was built for publication: Machine Learning for Inductive Theorem Proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6108816)