MGTP : 並行論理型言語 KL1 によるモデル生成型定理証明系
スポンサーリンク
概要
- 論文の詳細を見る
一階述語論理のための定理証明系を,モデル生成法に基づき並行論理型言語KL1で効率良く実現する方法について述べる.モデル生成法においては,値域限定という条件を満たす節集合を対象とした場合,出現検査付き単一化が不要であり,照合操作で十分となる.その結果,入力節中の変数を直接KL1変数で表現することができ,入力節に対する単一化をKL1節の頭部単一化として実行できるなど,KL1言語処理系を活用した効率の良い実装が可能となった.しかしながら,モデル生成法で支配的な計算量を占める連言照合手続きを効率良く実現することはそれほど容易ではない.我々は,連言照合手続きに含まれる冗長計算を除くため,2つの方式を考案して比較検討した.両方式ともコーディング手法としてKL1に特化されたものであるが,一般的に前向き推論系の効率的実装技術としてKL1以外の実装言語を用いた場合にも有効な技術である.
- 1996-01-15
論文 | ランダム
- 自己血輸血-術前貯血を行ったにもかかわらず同種血輸血を必要とした症例の検討と反省-
- 多段階チルト時心拍変動性指標の加齢変化
- 女性医師の学会活動の現状
- 日本における女性医師の現況に関する調査研究-全女性医師(対象27,779名)に対するアンケート結果から-
- H-IIAロケットのシステムと開発計画について