基于重写归纳的推理技术及应用

In this paper we briefly analyze the background for the NSFC-supported project Reasoning Techniques and Applications Based on Rewriting Induction. The new approach, which combines theorem proving and model checking methods, is described. Finally, we present the obtained results on the principles, algorithms, and applications of inductive reasoning.

研究基于重写归纳的高效推理技术。结合测试集途径和显示归纳法，提出基于构造集的归纳证明原理，将归纳过程分解为公理化描述和相容性检查两个步骤，考虑归纳假设使用、归纳规则生成、归纳变量选择、归纳定理推广等方面的优化方案，使重写归纳推理具有灵活性，达到速度更快、能力更强。研究成果应用于程序综合，促进软件的自动化开发与验证。