E単一化子の完全集合を求める推論規則
スポンサーリンク
概要
- 論文の詳細を見る
等式理論を法として単一化を行う拡張単一化のことをE単一化という.本稿では,E単一化を行う半決定手続きを与える.この手続きは,任意の等式理論に対して完全である.完全性の証明には証明順序法を用いる.また手続きは,Knuth-Bendix完備化手続きの拡張になっているので,E単一化の過程で等式理論に対応する完備な項書換え系を獲得することもある.この場合,本稿はHullotの結果の一般化でもある.
- 日本ソフトウェア科学会の論文
- 1991-05-15
著者
関連論文
- 代数的仕様を用いたソフトウェア開発支援環境 : Metis-AS
- Metis-AS における代数的仕様の検証手続き
- 等式論理の帰納的定理を証明する手続き
- E単一化子の完全集合を求める推論規則
- 項書換えシステム「Metis」の実装
- 不偏ゲームの平坦性についての考察(セッション(6) : 一般)
- Knuth-Bendixの完備化手続きとその応用
- 正規論理とそのmodelについて(計算機構に関する数学的基礎理論とその応用)
- 標数2のある体上の代数方程式の求解
- 「結合子による高階単一化」再考
- 特集「制約論理プログラミング」の編集にあたって (制約論理プログラミング)