通过反射自动化归纳
Automating Induction by Reflection
摘要：
尽管最近在全一阶理论的自动化定理证明方面取得了进展，归纳推理仍然对最先进的定理证明器提出了严峻的挑战。其原因是，在一阶逻辑中，归纳法需要无限数量的公理，这对于需要有限输入的计算机辅助定理证明器来说是不可行的。数学实践就是把这些无穷公理集指定为公理方案。不幸的是，这些图式定义不能在一阶逻辑中形式化，因此不支持作为一阶定理证明器的输入。在这项工作中，我们介绍了一种新的方法，启发真理的公理理论领域，允许表达示意归纳定义，在多排序的一阶逻辑的标准语法。此外，我们测试的实际可行性的方法与国家的最先进的定理证明，比较它的求解器的本地技术处理归纳。本文是LFMTP 21提交文件的扩展版本，具有相同的标题。
英文摘要：
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The reason for that is that in first-order logic induction requires an infinite number of axioms, which is not a feasible input to a computer-aided theorem prover requiring a finite input. Mathematical practice is to specify these infinite sets of axioms as axiom schemes. Unfortunately these schematic definitions cannot be formalized in first-order logic, and therefore not supported as inputs for first-order theorem provers. In this work we introduce a new method, inspired by the field of axiomatic theories of truth, that allows to express schematic inductive definitions, in the standard syntax of multi-sorted first-order logic. Further we test the practical feasibility of the method with state-of-the-art theorem provers, comparing it to solvers' native techniques for handling induction. This paper is an extended version of the LFMTP 21 submission with the same title.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
