定理証明器PTTPにおける対偶節生成の削減効果
スポンサーリンク
概要
- 論文の詳細を見る
PTTP(Prolog technology theorem prover)は、1階述語論理の完全な定理証明器となるようなPrologの拡張であり、推論システムを完全にするためにモデル消去法を用いている。このモデル消去法は、ノン・ホーン節を含む節集合の全ての節の対偶を取ることによって推論を行うため、効率を悪くしている。本研究では、対偶を必要に応じて取るようなアルゴリズムを作成し、推論の対象となる節の数を減らすことによって、PTTPの効率改善を図る。
- 一般社団法人情報処理学会の論文
- 1996-03-06
著者
関連論文
- 様相節変換に基づくボトムアップ型様相論理証明法
- 信念様相論理に対する様相節変換型証明器の実現
- 様相節変換に基づくMGTP上の様相論理証明器の効率的実現
- モデル生成型定理証明器を用いたアブダクションの計算における効率化手法
- モデル生成に基づく並列アブダクション
- モデル生成に基づく並列アブダクション
- 上昇型定理証明の探索効率を高めるノンホーン・マジックセット
- アクション言語Αのためのオートマトン理論
- 定理証明器PTTPにおける対偶節生成の削減効果
- アクション言語Aを表現するオートマトンモデル
- アブダクションを用いた逐次的な自然言語理解モデル