论文标题
基于模板的猜想，用于伊莎贝尔/hol自动诱导
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
论文作者
论文摘要
通过归纳证明在形式验证中起着核心作用。但是，其自动化仍然是计算机科学中的巨大挑战。为了解决归纳问题，人类工程师通常必须手动提供辅助引理。我们使用基于模板的猜想来使这一艰苦的过程自动化，这是一种新型的方法，可以产生辅助引理并使用它们来证明最终目标。我们的评估表明，我们的工作原型TBC实现了40个百分点的成功率提高了中级难度水平问题的成功率。
Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 40 percentage point improvement of success rates for problems at intermediate difficulty level.
