2002 Fiscal Year Annual Research Report
| Project/Area Number |
13680422
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
新井 紀子 国立情報学研究所, 情報学基礎研究系, 助教授 (40264931)
|
|---|
| Keywords | 証明論 / 計算の複雑さ理論 / 証明の複雑さ理論 / 自動証明 / 遠隔教育 |
|---|
| Research Abstract |
平成11年度に提案した、simple combinatorial reasoningが類似の体系であるsymmetryつきのresolutionよりも体系として優れていることを証明した。すなわち、symmetryつきのresolutionはbackward searchができないという自動証明機向けの体系としての大きな欠点があるばかりでなく、simple combinatorial reasoningでは線形時間で解決可能であるような問題にたいして、指数時間かかることがあることを示した。このことで、simple combinatorial reasoningの優位性を証明したといえる。
また、平成13年度には、tree resolutionとanalytic tableauxのさまざまな形式化について、証明の複雑さを論じ、1975年にCookによって提出された定理「tree resolutionはanalytic tableauxに比べてexponentialなspeed-upを有する」という結果が誤りであり、正しくは「tree resolutionはanalytic tableauxに比べて、super-polynomialなspeed-upを有するが、analytic tableauxはtree resolutionを決定的チューリング機械によって、quasi-polynomial timeでsimulate可能である」ことをPittasiおよびUrquhartとともに示した。
平成14年度にはさらに自動証明および高精度保証ソフトウェア開発における論理学の応用について研究し、特に遠隔教育のプラットフォームの開発に応用した。
|
-
[Publications] Noriko H.Arai, Toniann Pittasi, Alasdair Urquhart: "The complexity of analytic tableaux"Proceedings of Symposium of Theory of Computing (STOC'01). 356-363 (2001)
-
[Publications] Noriko H.Arai, Toru Takahashi, Hideaki Takeda, Yasuhiro Katagiri: "E-Classroom ; how can we effectively use digital contents in a distance education system?"Proceedings of Logic in Real-World Interaction. (To appear). (2003)
