ソフトウェアモジュールの二つのデータを比較する場合、内部構造を比較するのでは
なく、それらのデータに対してあらゆる操作を適用して観測した結果が等しい時、振
舞等価であるという。データを表現する二つの式からなる等式は、式が表すデータ同
士が振舞等価である時、振舞定理であるという。振舞定理を証明する手法としては、
観測操作の構造に関する帰納法、余帰納法、潜在帰納法がある。本研究では、
Knuth-Bendix完備化手続きを改変した潜在帰納法に基づく振舞定理証明系をプログラ
ミング言語MLを用いて実現する。
この実現は２つの部分からなる。一つは、改変
されたKnuth-Bendix手続きを実現する。他方は、改変Knuth-Bendix手続きが必要とす
る、式の間の半順序関係を与えるための関数記号間の全順序関係を自動生成する部分
である。この二つにより、振舞定理の自動証明ができることをいくつかの例で確認し
た。効率の改善、適用範囲の拡大は今後の課題である。