部分例示に基づく定理自動証明

• 山本, 雅人

• 大柳, 俊夫

• 大内, 東

書誌事項

タイトル別名

• Theorem Proving Based on the Partial Instantiation Technique
• ブブン レイジ ニ モトズク テイリ ジドウ ショウメイ

抄録

定理自動証明に対するこれまでの研究として,1965年にRobinsonによって提案された導出原理に基づくさまざまな方法,戦略などが提案されており,現在の定理証明システムの多くはこの導出原理に基づいている.これに対して,Jeroslowは1988年に部分例示手法を提案している.しかしながら,Jeroslowの提案した方法は関数記号を含まない論理式のみを対象としていること,また,節形式を前提としていないために効率が悪いことなどの欠点があった.筆者らはこのこのJeroslowの方法を改善して,関数記号を含まない節形式の論理式の充足可能性を判定する手続きを提案して,その有効性を示している.本論文では,この手続きを拡張した定理証明手続きを提案する.すなわち,関数記号を含む論理式を扱えるようにしている.また,本手続きが完全であることの証明を与える.更に,比較実験を行い本手続きの有効性について検討する.

収録刊行物

• 電子情報通信学会論文誌. A, 基礎・境界

  電子情報通信学会論文誌. A, 基礎・境界 78 (7), 864-871, 1995-07-25

  一般社団法人電子情報通信学会

キーワード

• 部分例示
• 充足可能性問題
• 定理自動証明
• 導出原理
• Davis-Putnamの方法

詳細情報

• CRID: 1050001339022802176
• NII論文ID: 110003312240
• NII書誌ID: AN10013345
• HANDLE: 2115/64575
• NDL書誌ID: 3621695
• ISSN: 09135707
• Web Site: http://id.ndl.go.jp/bib/3621695
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I3621695
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles