|
本研究では、構成的論理の証明をラムダ項として研究を進めた。推論の構造、証明図の構造、証明の変換等をラムダ項の構造やラムダ項の変換として捕らえことができた。具体的な論理としては、適切さの論理と古典諭理について以下の成果を得た。
適切さの論理:適切さの論理P-Wに対する証明図をHereditary Right Maximal Linearなラムダ項として特徴づけることができた。これを用いて、α→αの証明は本質的に自明なものしかないという知見を得、適切さの論理における『P-W問題』を発展させた。
古典論理に対する計算規則:古典論理の命題を型としてもつような拡張されたラムダ項の定式化を与え、そのリダクション規則を調べた。具体的な方法として、古典論理を特徴づけるパースの論理式に対応する変形規則を求め、古典論理に対する結合子論理を定式化した。この変形規則は古典論理の証明から構成的証明を抽出する自然な変形である。この変形によれば、同じ論理式に対する証明はすべて同等となるという結果を得た。これは、古典論理でチャーチ・ロサ-の性質が成り立たない理由を、論理式と型との対応から説明するものである。
証明探索システム:与えられた含意論理式に対し直観主義論理における証明図全体は、ある種の文法で記述できるという結果を得た。更にこのような証明図全体が有限か無限かという問題の複雑さが多項式領域完全であるという知見を得た。高橋、赤間との共同研究では、さらにこのアイデアが高階の型の体系にも拡張できるこという知見を得た。証明の探索ならびに反例の生成を行うシステムを開発し、WEB上で公開した。
|
