Inductive Decidability Using Implicit Induction
Inductive Decidability Using Implicit Induction
复制标题
使用隐式归纳法的归纳可判定性
DOI：
10.1007/11916277_4
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
D. Kapur
中科院分区：
文献类型：
--
作者：
Stephan Falke;D. Kapur
决策过程广泛用于自动推理工具中，以便对数据结构进行推理。在实际应用中，许多命题超出了决策过程所处理的理论范围。通常，需要对这些数据结构上的用户定义函数进行推理。为此，必须采用归纳推理。在这项工作中，类的功能定义和aesturtures确定的归纳有效性可以自动决定使用隐式归纳方法和决策程序的基础理论。本文所考虑的方程组大大扩展了Kapur & Subramaniam（CADE，2000）[15]的结果，这些结果是使用显式归纳法得到的。首先，可以自动确定非线性结构。其次，函数定义可以在其定义中使用其他已定义的函数，从而允许相互递归的函数和关于它们的可判定的构造。第三，命题可以有来自归纳位置的可判定理论的一般项。这些贡献对于成功地将归纳推理集成到决策过程中至关重要，从而使其能够在包括验证和程序分析在内的应用中以按钮模式使用。
Decision procedures are widely used in automated reasoning tools in order to reason about data structures. In applications, many conjectures fall outside the theory handled by a decision procedure. Often, reasoning about user-defined functions on those data structures is needed. For this, inductive reasoning has to be employed. In this work, classes of function definitions and conjectures are identified for which inductive validity can be automatically decided using implicit induction methods and decision procedures for an underlying theory. The class of equational conjectures considered in this paper significantly extends the results of Kapur & Subramaniam (CADE, 2000) [15], which were obtained using explicit induction schemes. Firstly, nonlinear conjectures can be decided automatically. Secondly, function definitions can use other defined functions in their definitions, thus allowing mutually recursive functions and decidable conjectures about them. Thirdly, conjectures can have general terms from the decidable theory on inductive positions. These contributions are crucial for successfully integrating inductive reasoning into decision procedures, thus enabling their use in push-button mode in applications including verification and program analysis.