一句话：建立理论模型分析自动归纳定理证明中归纳公理选取的困难，并厘清不同归纳性概念的关系。
本文研究自动归纳定理证明的逻辑基础。作者首先构建一个以“寻找足以证明目标的归纳公理之难度”为核心的理论模型，然后在该模型下分析证明形状的选择、归纳规则的选择以及归纳公式的语言。借助模型论技术，论文厘清了自动归纳定理证明文献中若干“归纳性”概念之间的关系。该工作为理解归纳定理证明中的核心逻辑问题提供了统一的概念框架和基础性观察。
In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving. This is a corrected version of the paper arXiv:1704.01930v5 published originally on Nov.~16, 2017.
@article{paperbot413,
title = {Some observations on the logical foundations of inductive theorem proving},
author = {Stefan Hetzl and Tin Lok Wong},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
number = {Automated deduction},
year = {2018},
doi = {10.23638/lmcs-13(4:10)2017}
}