2001 Fiscal Year Annual Research Report
| Project/Area Number |
13680422
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
新井 紀子 国立情報学研究所, 情報学基礎研究系, 助教授 (40264931)
|
|---|
| Keywords | ロジック / 複雑さ理論 / 数学基礎論 / 自動証明 / resolution / tableau |
|---|
| Research Abstract |
トロント大学情報科学部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によってそれを実現するために現在準備中である。
|
-
[Publications] N.Arai, T.Pittassi, A.Urquhart: "The complexity of analytic tableaux"Proceedings of STOC2001 (Symposium of Theory of Computing). 356-363 (2001)
-
[Publications] N.Arai, R.Masukawa: "How to find symmetries hidden in combinatorial problems"Symbolic Computation and Automated Reasoning (eds. M.Karber, M Kohlhase), AK Peters. 18-32 (2001)
-
[Publications] Don Cohen, 新井 紀子: "アメリカ流7歳からの行列"講談社ブルーバックス. 196 (2001)
