论文部分内容阅读
该文在系统分析归纳法推理基本理论的基础上,深入研究了归纳法推理策略,取得了以下成果:该文提出了递归函数终止性的自动证明方法,在分析与证明过程中应用任意测度函数,改进了传统的终止性证明方法;提出了一种新的推理策略--标记重写策略,对其建立了严格的形式化系统;给出了一般意义上推理策略的分类方法.在归纳法推理的实际研究中,该文提出mJVM的形式化模型,用来模拟实际Java虚拟机系统.