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