Knuth-Bendix完备化过程的实现及其有效性

本文讨论了 Knuth-Bendix 完备化过程的一些理论问题和实现技术,同时,分析完备化过程终止的成功率,进而讨论完备化过程在教学科研中应用的可行性.

Knuth－Bendix过程的发散现象的研究

Ｋｎｕｔｈ－Ｂｅｎｄｉｘ完备过程不终止的起因研究得很少．本文研究引起不终止的重写规则的结构性质，提出了相容交叉规则对的概念，推广了文献［６］的结论，并提出了为构造系统检验该过程是否不终止的方法．

重写系统中的显式归纳方法

提出了重写系统中的显式归纳方法，设计了一个新的归纳定理证明系统。实例表明，显式归纳方法要比无归纳的归纳方法来得简单直观。