MGTP : 並行論理型言語 KL1 によるモデル生成型定理証明系
スポンサーリンク
概要
- 論文の詳細を見る
一階述語論理のための定理証明系を,モデル生成法に基づき並行論理型言語KL1で効率良く実現する方法について述べる.モデル生成法においては,値域限定という条件を満たす節集合を対象とした場合,出現検査付き単一化が不要であり,照合操作で十分となる.その結果,入力節中の変数を直接KL1変数で表現することができ,入力節に対する単一化をKL1節の頭部単一化として実行できるなど,KL1言語処理系を活用した効率の良い実装が可能となった.しかしながら,モデル生成法で支配的な計算量を占める連言照合手続きを効率良く実現することはそれほど容易ではない.我々は,連言照合手続きに含まれる冗長計算を除くため,2つの方式を考案して比較検討した.両方式ともコーディング手法としてKL1に特化されたものであるが,一般的に前向き推論系の効率的実装技術としてKL1以外の実装言語を用いた場合にも有効な技術である.
- 1996-01-15
論文 | ランダム
- CMテストとリフティングによる安全な楕円暗号系の構成法の実現と解析
- ARDS;septic ARDSを含めて (特集 急性呼吸不全に対する呼吸管理ベストプラクティス) -- (救急患者にみられる急性呼吸不全の病態と治療)
- 第1回 生研産学共同研究の歴史を振り返る懇談会 : （生研アーカイバル懇談会）
- びまん性汎細気管支炎--経気管支肺生検による診断 (閉塞性肺疾患)
- 腎障害に伴う高血圧患者に対するアロチノロ-ル(Arotinolol)の降圧効果と腎機能に及ぼす影響についての検討