自然演繹の体系と古典論理の計算機構

点击翻译按钮获取中文摘要

研究実行計画にしたがって、下記のような結果を得た。証明論の方法論としてのinfinite version of generalized Konig's lemmaとgeneralized bar inductionの数学的同値性の証明の概要。自然演繹の新しい体系NDKの再定式化およびその2階論理への拡張。NDKの正規証明からNKの(自然な)証明への変換アルゴリズムの構成。NDKの計算機構を表現する項体系NDTRMの定義。NDKとNDTRMの相互写像などいくつかの詳細は今後の課題として残ったが、方法論は明確なので、実行に問題はないと予想される。これらの研究において、形式的体系と計算性の問題、計算機使用の援助などに関して、本学の辻井、中神、藤井、鷲原の各教授にも協力を依頼した。大学院生の笠さんは、NDKの最初の協力者であったが、さらにそのグラフィックな表現および論理的複雑度のスケールの研究を担当した。また、プログラミングにおいては学部生の協力も得た。研究費は、研究連絡および研究会出席などの旅費、知識・技術提供の謝金、文房具、ソフトウエアなどの消耗品などに使用した。設備備品としては書籍以外に、プリンタを購入した。通信費およびコピー代を大学の研究費内でまかなうことができたので、その分を手持ちのパソコンにつなぐプリンタにまわした。実験的な入力を即カラーで見ることができて、大変便利になった。科学基礎論学会、数理解析研究所短期共同研究集会、超準解析研究会、などで関連テーマの講演を行った。また、関連分野の談話会およびインフォーマルなセミナー講師として、R. Pollack, J-P. jouannaud, MaLi, 小川重義の諸氏を招いた。