Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday
Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday
复制标题
系统设计原理 - 献给 Thomas A. Henzinger 60 岁生日的论文
DOI：
10.1007/978-3-031-22337-2_15
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Hajdu M
中科院分区：
文献类型：
--
作者：
Hajdu M
基于饱和的一阶定理证明中的归纳是归纳推理自动化中一个令人兴奋的新方向。在本文中，我们调查了将归纳法直接集成到一阶定理证明的基于饱和的证明搜索框架中的工作。我们描述了归纳推理规则，用归纳定义的数据类型和整数来证明属性。我们还提出了额外的推理启发法来加强归纳推理，以及使用归纳假设和递归函数定义来指导归纳。我们提供了详尽的实验结果，证明了我们在 Vampire 中实施的方法的实际影响。
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire.