MGTP : 並行論理型言語 KL1 によるモデル生成型定理証明系
スポンサーリンク
概要
- 論文の詳細を見る
一階述語論理のための定理証明系を,モデル生成法に基づき並行論理型言語KL1で効率良く実現する方法について述べる.モデル生成法においては,値域限定という条件を満たす節集合を対象とした場合,出現検査付き単一化が不要であり,照合操作で十分となる.その結果,入力節中の変数を直接KL1変数で表現することができ,入力節に対する単一化をKL1節の頭部単一化として実行できるなど,KL1言語処理系を活用した効率の良い実装が可能となった.しかしながら,モデル生成法で支配的な計算量を占める連言照合手続きを効率良く実現することはそれほど容易ではない.我々は,連言照合手続きに含まれる冗長計算を除くため,2つの方式を考案して比較検討した.両方式ともコーディング手法としてKL1に特化されたものであるが,一般的に前向き推論系の効率的実装技術としてKL1以外の実装言語を用いた場合にも有効な技術である.
- 1996-01-15
論文 | ランダム
- Observations on the sea coast of northern Shikoku.
- 義太夫節の音楽構造(II) : 文献・資料に表わされた息使いの記述
- 義太夫節の音楽構造(I) : 日本伝統音楽研究のためのある視点
- 近代日本音楽資料集(II) : 五世福原百之助著「黒美寿(くろみす)」について
- 近代日本音楽資料集(I) : 長唄歌曲審議会発行「長唄定本改訂歌詞集」について