部分例示手法に基づいた定理自動証明手続き

• 山本, 雅人

• 大柳, 俊夫

• 大内, 東

書誌事項

タイトル別名

• A Theorem Proving Procedure based on the Partial In-stantion Technique

抄録

Jeroslow は関鍵記号を含まない論理式の充足可能性判定のための部分例示手法の理論的枠組みを提案している.部分例示手法は真理値の割当てを用いることによって節の増加を抑えようとするものである.しかしながら,Jeroslowの方法では関数記号を含む論理式は扱うことができない.本稿では,関数記号を含む論理式に対しての部分例示手法に基づいた定理自動証明手続きを提案する.この手続きは節形式の論理式を扱うが,そのことによって一般性を失うことはなく,むしろ Jeroslow の方法より効率的であることを示す.また,完全性が成り立つことの証明を与えている.さらに,導出原理に基づく方法との比較実験によって本手続きの有効性を示す.

収録刊行物

• 全国大会講演論文集

  全国大会講演論文集 第49回 (人工知能及び認知科学), 13-14, 1994-09-20

詳細情報

• CRID: 1050292572151774208
• NII論文ID: 110002885544
• NII書誌ID: AN00349328
• Web Site: http://id.nii.ac.jp/1001/00126619/
• 本文言語コード: ja
• 資料種別: conference paper
• データソース種別:
  • IRDB
  • CiNii Articles