平成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年度にはさらに自動証明および高精度保証ソフトウェア開発における論理学の応用について研究し、特に遠隔教育のプラットフォームの開発に応用した。
|