研究課題
基盤研究(C)
条件付き項書き換えシステムは，ホーン節理論に対応する書き換えシステムの拡張であり，より広範な代数構造を対象とするばかりでなく，関数型プログラムのより直接的な翻訳を実現できるため，応用上も重要な拡張である．条件付き項書き換えシステムの合流性検証では，従来の書き換え理論の様々な応用を用いた合流性検証ツールと第一階述語論理の定理自動証明ツールを用いるアプローチに基づく合流性検証ツールが拮抗している．本研究では，2 つのアプローチをどのように融合できるか，また，それによって，より強力な条件付き項書き換えシステムの強力な検証法を実現できるかを検討する．
