<学術雑誌論文>
証明探索と反例生成を同時に行なうアルゴリズムについて

作成者
本文言語
出版者
発行日
収録物名
開始ページ
終了ページ
出版タイプ
アクセス権
関連URI
概要 直観主義論理は, 型理論との対応や, 構成的プログラミングとの関連で重要性が広く認識されるようになってきた。自然推論の形での証明図を求める手法や証明図を全て求めるアルゴリズムなどが知られている。しかしその意味論の取扱は, 古典論理に比べて容易ではない。古典命題論理では真偽の2値の真理値表により, 恒真性が判定でき, これが証明可能性と一致している。従って, ある命題が古典論理で証明できないことを示...すには, その命題の真理値が偽となるような命題変数への割り当てを示せばよい。これに対し直観主義の意味論はクリプケ・モデルや擬プール代数によるもので, 古典論理におけるように単純なものではない。命題が証明できるかどうかを機械的に判定するアルゴリズムはいずれの論理についてもすでに古くから知られているが, 証明出来る場合に証明を返すだけでなく, 証明できない場合には反例を具体的に構成するのは容易ではない。我々は直観主義命題論理のシーゲント計算の形式化を用いて逆向きの証明探索を行い, その過程で証明不能と判断できる場合にはその情報を用いて反例のクリプゲ・モデルを生成するアルゴリズムを構成した。これまで辿ってきたシーケントを保存することにより, 証明探索の打ちきりと反例の構成を統一的に行うことが可能となった。小さな命題については, 人間が手で計算しても分かるくらい単純なものである。実働化はhttp:
whale.i.kyushu-u.ac.jp/prover.htmlに公開している。
続きを見る

本文情報を非表示

hirokawa_195 pdf 261 KB 130  

詳細

レコードID
査読有無
NCID
注記
登録日 2013.12.09
更新日 2015.11.19

この資料を見た人はこんな資料も見ています