论文标题
Isabelle/HOL的智能感应（系统描述）
Smart Induction for Isabelle/HOL (System Description)
论文作者
论文摘要
证明助手提供策略以促进归纳证明。但是，仍然需要人类创造力来决定将哪些论点传递给这些归纳策略。为了自动化此过程，我们为isabelle/hol提供了smart_entuct。给定在任何问题域中的归纳问题，Smart_Induct列出了归纳策略的有希望的论点，而无需依赖搜索。我们的评估表明，Smart_Induct在问题域中提出了宝贵的建议。
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.
