|
構成的理論における証明の構造パターンをラムダ項で解析する研究を進めた。適切さの論理について、その証明をラムダ項として特徴付けることができ、それを用いて、適切さの論理におけるP-W問題に対し統語的で簡単な新しい証明を与えた。直観主義論理については、与えられた論理式に対しその正規形の証明図全体が、無限個の記号を持つ文脈自由文法として記述できるという知見を得た。証明の簡単化に対する新しい計算概念を探すことも本研究の重要なテーマであった。古典論理における証明の簡単化の新しい方式を発見し、その性質を明らかにした。これは、圈論におけるブール圈とも関連することが分かった。Parigot、de-Groote、Felleisenらの古典論理に対応する計算との関連は、今後の研究で明らかにしなければならない。これまで作成して来た型付けシステムと定理証明システムを、インターネットから直接利用できるようなシステムに改訂し、http://whale.i.kyushu-u.ac-jp/prover.htmlに公開した。複数のシステムを結合できる枠組を与えることができたので、他の定理証明システムを組み込むことが今後の課題となる。
|
