証明探索と反例生成を同時に行なうアルゴリズムについて
スポンサーリンク
概要
- 論文の詳細を見る
直観主義論理は, 型理論との対応や, 構成的プログラミングとの関連で重要性が広く認識されるようになってきた。自然推論の形での証明図を求める手法や証明図を全て求めるアルゴリズムなどが知られている。しかしその意味論の取扱は, 古典論理に比べて容易ではない。古典命題論理では真偽の2値の真理値表により, 恒真性が判定でき, これが証明可能性と一致している。従って, ある命題が古典論理で証明できないことを示すには, その命題の真理値が偽となるような命題変数への割り当てを示せばよい。これに対し直観主義の意味論はクリプケ・モデルや擬プール代数によるもので, 古典論理におけるように単純なものではない。命題が証明できるかどうかを機械的に判定するアルゴリズムはいずれの論理についてもすでに古くから知られているが, 証明出来る場合に証明を返すだけでなく, 証明できない場合には反例を具体的に構成するのは容易ではない。我々は直観主義命題論理のシーゲント計算の形式化を用いて逆向きの証明探索を行い, その過程で証明不能と判断できる場合にはその情報を用いて反例のクリプゲ・モデルを生成するアルゴリズムを構成した。これまで辿ってきたシーケントを保存することにより, 証明探索の打ちきりと反例の構成を統一的に行うことが可能となった。小さな命題については, 人間が手で計算しても分かるくらい単純なものである。実働化はhttp://whale.i.kyushu-u.ac.jp/prover.htmlに公開している。
- 1997-09-24
著者
-
廣川 佐千男
九州大学大学院システム情報科学研究科
-
佐塚 秀人
久留米工業大学
-
廣川 佐千男
九州大学
-
廣川 佐千男
九州大学 大型計算機センター
-
長野 大介
九州大学大学院
-
佐塚 秀人
九州大学大学院システム情報科学研究科
-
長野 大介
九大 大学院
関連論文
- 九州大学における一般情報処理教育支援システムについて
- 久留米高専のインターネットと久留米地区学術系NOCについて
- 証明探索と反例生成を同時に行なうアルゴリズムについて
- クリプケモデル生成とJavaアプレットとしての実現
- プログラミング教育のためのWEB上の動作表示システム
- Web データベースにおける入力フォーム情報の自動抽出
- 証明とモデルを生成するインターネットプルーバー
- ウェブデータウエアハウスと協働する業務報告書オーサリングシステム
- 協調作業におけるエージエシト間の相互作用のモデル化
- 初等幾何推論の多面的表示方式
- ZKネットワーク雑記帳
- 具体的な図を用いる初等幾何推論システム
- $\lambda_C$計算と$\lambda_P$計算との対応(計算理論とその応用)
- WWW上の幾何推論システム (「ネットワ-クとAI」小特集セッション)
- 分散する機能利用を支援するJavaを用いた対話環境
- リートネットワークによる併合法の実現
- CAI用パソコンLANにおけるファイル転送の性能評価
- 学生の教育履歴とプログラミング教育
- 初心者の冒すプログラム間違いの分析
- 複雑な知識モデルを利用した人間の学習プロセスシミュレーションの検討
- クロス集計による文献ファセット検索システムの提案
- ストリーミングビデオを用いた講義データベースシステム
- 二つの観点に基く検索結果の分析方法Double Rankについて(検索,第1回テキストマイニング・シンポジウム)
- 制約付きブートストラッピング法による特徴語抽出について(検索,第1回テキストマイニング・シンポジウム)
- 観光ブログからの地名抽出と曖昧性解消
- クロス集計による文献ファセット検索システムの提案 (情報処理学会第104回情報基礎とアクセス技術研究会(IFAT)発表論文)
- Crowdsourcing Systemを用いた略語の推定手法の提案 (言語理解とコミュニケーション)
- Crowdsourcing Systemを用いた略語の推定手法の提案 (音声)
- 日韓オノマトペの抽出とその感性評価利用
- 少数例による学習における属性選択の効果について