振舞仕様記述法は，ソフトウェアモジュールをブラックボックスと見なし，その状態 の振舞，すなわち状態に観測操作をほどこしたとき状態からどのような出力が得られ るかということだけに注目して仕様記述する方法であり，振舞が同じ状態は等しいと 見なされる．振舞仕様は公理と呼ばれる等式（あるいは書換え規則）の集合であり， それを満たすすべてのソフトウェアモジュール上で成り立つ性質を振舞定理という． 振舞定理の自動証明はソフトウェアモジュールの信頼性向上のために重要である．振 舞定理の自動証明法としては，これまでに，観測操作の構造に関する帰納法，余帰納 法，テスト集合余帰納法などが研究されている．本研究では，帰納的定理の証明法と して従来から使われている潜在帰納法を振舞定理の証明に適用する．潜在帰納法は推 論規則の集合からなり，Knuth-Bendix手続きとして実現され，定理自動証明の有望な アプローチの一つとして認められている．帰納的定理の証明のための潜在帰納法の推 論規則集合としては，基本完備化システム，標準完備化システムがある．この２つの システムの方向付の推論規則を変更し，新たに基本振舞完備システムおよび標準振舞 完備システムを定めて，それらに基づくKnuth-Bendix手続きが健全であることを証明 する．