- 著者
-
新井 紀子
- 出版者
- 国立情報学研究所
- 雑誌
- 基盤研究(C)
- 巻号頁・発行日
- 2001
コンピュータサイエンスにおいて、最も中心的な問いのひとつが、与えられた関数(グラフ)を計算するための最も効率のよいアルゴリズムは何か?と言う問題である。これは、ひとつには「P=?NP」問題に集約される。この課題に対して、ロジックからのアプローチとしては、次の2つが考えられる1.与えられた命題論理の体系に対し、その体系では多項式サイズの証明が存在しないような定理群を発見する2.与えられた2つの命題論理の体系が相対的にどちらの方が証明効率がよいか本研究においては、タブロー法とレゾリューション法の証明の複雑さに関して研究を進めた。この2つの体系は、多くの自動証明機のエンジンとして採用されていることを追記しておく。その結果、1970年代から未解決であった、さまざまなタブロー法のバリエーション間の相対的証明効率の問題を完全解決した。まず、自動証明機のエンジンとして最も採用されているclausal tableauというタブローは一般的なタブローに比べて、superpolynomial-timeな遅延があることを発見した。また、resolution法はタブロー法に比べてexponentialのスピードアップがあると信じられてきたが、それは誤りであり、resolution法はタブロー法に比べて、擬似多項式時間分しかスピードアップしないことを論理的に証明した。一方、本研究においては、clausal tableau法にシンメトリーという推論を付け加えることによって、新しい体系SCRを構築し、その証明力についてさまざまに考察した。結果、resolutionでは短く証明できない多くの組み合わせ論的な問題がSCRでは多項式サイズの証明があることがわかった。SCRはタブロー法をベースとしているため、自動証明に応用することができ、これをGodzillaという自動証明機として実現した。