Towards Machine Learning Induction
Yutaka Nagashima
TL;DR
This paper discusses advances in automating inductive theorem proving in Isabelle/HOL and introduces MeLoId, a new approach to identify promising induction applications without full proof searches.
Contribution
The paper presents MeLoId, a novel method for suggesting induction applications, enhancing automation in inductive theorem proving.
Findings
Progress in automating inductive theorem proving for Isabelle/HOL
Introduction of MeLoId for predicting promising induction applications
Potential to improve proof automation efficiency
Abstract
Induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle/HOL. Then, we present MeLoId, our approach to suggesting promising applications of induction without completing a proof search.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Parallel Computing and Optimization Techniques