Smart Induction for Isabelle/HOL (System Description)
Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct lists promising arguments for the induct tactic without relying on a search. Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains.
Code (0)
등록된 구현이 없습니다.
Tasks
IngenuitySimilar Papers 제목 키워드 기반
Towards United Reasoning for Automatic Induction in Isabelle/HOL
Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united…
Automated Theorem ProvingFaster Smarter Induction in Isabelle/HOL
Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed …
Towards Machine Learning Induction
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 ind…
Automated Theorem ProvingBIG-bench Machine LearningTowards Smart Proof Search for Isabelle
Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta…
PositionSimple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents imped…
Automated Theorem ProvingBIG-bench Machine LearningFormal Logic