研究概要 |
トロント大学情報科学部Alasdair Urquhart, Toniann Pittassi両教授とともに、一般的にtableauxシステムがresolutionシステムと比較してどのような証明の複雑さを持つかについて理論的に研究し、(1)tree resolutionはclausal tableauに対して、exponentialなspeed-upを持つことを証明した。 (2)binary tableauはclausal tableauに対して、super-polynomialなspeed-upを持つことを証明した。 (3)最も一般的な形をしているtableauであっても、tree resolutionと同等な証明効率は達成し得ない。Tree-resolutionは一般的にtableauに対して、super-polynomialなspeed-upを持つ。 (4)tableauはtree-resolutionをquasi-polynomial時間内で模倣することができる。つまり、(3)で得られた下界はタイトであることを証明した。 以上の結果により、1970年代より未解決であった、tree resolutionとtableauの証明効率の問題を完全に解決することができた。 また一方で、コンピュータの基礎理論を日本でより盛んにするため、中等高等教育の場で、コンピュータの基礎理論を学ぶための手法を開発中である。とくに、e-learningによってそれを実現するために現在準備中である。
|