| 研究課題/領域番号 |
13680422
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
新井 紀子 国立情報学研究所, 情報学基礎研究系, 助教授 (40264931)
|
|---|
| 研究期間 (年度) |
2001 – 2003
|
| 研究課題ステータス |
完了 (2003年度)
|
| 配分額 *注記 |
3,000千円 (直接経費: 3,000千円)
2003年度: 700千円 (直接経費: 700千円)
2002年度: 900千円 (直接経費: 900千円)
2001年度: 1,400千円 (直接経費: 1,400千円)
|
|---|
| キーワード | 証明の複雑さ / 計算の複雑さ / ロジック / 命題論理 / 複雑さ理論 / 数学基礎論 / 自動証明 / resolution / tableau / 証明論 / 計算の複雑さ理論 / 証明の複雑さ理論 / 遠隔教育 |
|---|
| 研究概要 |
コンピュータサイエンスにおいて、最も中心的な問いのひとつが、与えられた関数(グラフ)を計算するための最も効率のよいアルゴリズムは何か?と言う問題である。これは、ひとつには「P=?NP」問題に集約される。この課題に対して、ロジックからのアプローチとしては、次の2つが考えられる
1.与えられた命題論理の体系に対し、その体系では多項式サイズの証明が存在しないような定理群を発見する
2.与えられた2つの命題論理の体系が相対的にどちらの方が証明効率がよいか
本研究においては、タブロー法とレゾリューション法の証明の複雑さに関して研究を進めた。この2つの体系は、多くの自動証明機のエンジンとして採用されていることを追記しておく。その結果、1970年代から未解決であった、さまざまなタブロー法のバリエーション間の相対的証明効率の問題を完全解決した。まず、自動証明機のエンジンとして最も採用されているclausal tableauというタブローは一般的なタブローに比べて、superpolynomial-timeな遅延があることを発見した。また、resolution法はタブロー法に比べてexponentialのスピードアップがあると信じられてきたが、それは誤りであり、resolution法はタブロー法に比べて、擬似多項式時間分しかスピードアップしないことを論理的に証明した。
一方、本研究においては、clausal tableau法にシンメトリーという推論を付け加えることによって、新しい体系SCRを構築し、その証明力についてさまざまに考察した。結果、resolutionでは短く証明できない多くの組み合わせ論的な問題がSCRでは多項式サイズの証明があることがわかった。SCRはタブロー法をベースとしているため、自動証明に応用することができ、これをGodzillaという自動証明機として実現した。
|
