归纳证明的规范变换方法

A Specification Transformation for Proof by Induction

给出了一般等式规范到有序类等式规范的变换方法，以及在有序类等式规范上的主要结论。在此基础上．又给出了有序类规范上的一个归纳证明方法。这一方法避免了Jouannaud-Kounalis方法中所谓归纳可归约性检查这一很费时的过程，且我们的合流性检查不依赖于终止性检查。

This paper intreduces a transformation of equational specification into ordcr-sorted equation al specification and the main conclusion of order-sorted equational specification. On this basis, a method of proof by induction is shown in order-sorted specification. With this method it is no necessary to use the so-called 'inductive reducibility test' which is the most expensive part of the Jouannaud-Kounalis algorithm, and makes termination independent of confluence.