Machine Learning for Inductive Theorem Proving

DOI10.1007/978-3-319-99957-9_6zbMath1515.68344MaRDI QIDQ6108816

Petros Papapanagiotou, Unnamed Author, 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

theorem provinginductionmachine learninglemma selection

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Lightweight relevance filtering for machine-generated resolution problems
• Isabelle/HOL. A proof assistant for higher-order logic
• Superposition with structural induction
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Proof-Pattern Recognition and Lemma Discovery in ACL2
• TacticToe: Learning to Reason with HOL4 Tactics
• Optimizing proof search in model elimination
• Automating Inductive Proofs Using Theory Exploration
• Hammering towards QED
• MaSh: Machine Learning for Sledgehammer

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