论文标题
迈向伊莎贝尔/hol自动归纳的联合推理
Towards United Reasoning for Automatic Induction in Isabelle/HOL
论文作者
论文摘要
归纳定理证明是计算机科学中重要的长期挑战。在这个扩展的摘要中，我们首先总结了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 reasoning, a novel approach to further automating inductive theorem proving. Upon success, united reasoning takes the best of three schools of reasoning: deductive reasoning, inductive reasoning, and inductive reasoning, to prove difficult inductive problems automatically.
