ITR: Integrating Induction Schemes into Decision Procedures

基于决策过程的验证工具，包括基于OBDD的工具和模型检查器，已经有效地应用于硬件验证、协议分析与验证、代码的静态分析与类型检查、字节码验证、移动代码分析和携带证明的代码等许多应用领域。然而，这些工具无法处理使用大状态空间（包括无限状态空间）建模的计算，部分原因是它们不支持归纳推理。基于归纳法的定理证明虽然非常强大，但缺乏自动化，需要大量的用户指导。提出了一种新颖而激进的方法，将决策过程、重写和归纳方案以一种有限的方式结合起来，从而不失去自动化。利用这种方法，递归定义作为终止重写规则在可判定理论（如Presburger算法）之上给出。归纳方案是从这些终止定义生成的。通过对递归定义施加结构，可以自动确定需要归纳推理的一大类猜想。建议扩展和推广这种方法，以考虑一大类递归定义的函数，它们之间的相互作用，以及关于这些函数的一大类猜想，这些猜想可以自动决定（不需要任何用户指导）。

Verification tools based on decision procedures including OBDD based tools and model-checkers have been effectively used in many application areas including hardware verification, protocol analysis and verification, static analysis and type-checking of code, byte-code verification, analysis of mobile code and proof-carrying code. These tools are however unable to deal with computations modeled using large state space (including infinite state space), partly because they do not support inductive reasoning. Induction based theorem provers, while quite powerful, lack automation and require tremendous user guidance. A novel and radical approach is proposed to combine decision procedures, rewriting and induction schemes in a restricted way so as not to lose automation. Using this approach, recursive definitions are given as terminating rewrite rules on top of decidable theories, such as Presburger arithmetic. Induction schemes are generated from these terminating definitions. By imposing structure on recursive definitions, it becomes possible to automatically decide a large class of conjectures requiring inductive reasoning. It is proposed to extend and generalize this approach to consider a large class of recursively defined functions, their interactions with each other, as well as a large class of conjectures about these functions, that can be automatically decided (without any need for user guidance).