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. This is an extended version of a Principles of Systems Design 2022 paper with the same title and the same authors.

翻译：在基于饱和的一阶定理证明中引入归纳推理，是自动化归纳推理领域一个令人振奋的新方向。本文综述了我们关于将归纳法直接集成到一阶定理证明的饱和搜索框架中的研究工作。我们描述了用于证明归纳定义数据类型与整数性质的归纳推理规则，同时提出了强化归纳推理、利用归纳假设及递归函数定义引导归纳过程的附加推理启发式方法。通过Vampire系统实现的实验结果表明，该方法具有显著的实际应用价值。本文是2022年《系统设计原理》会议同名论文（作者相同）的扩展版本。