構成的理論の推論構造の研究

1996 Fiscal Year Annual Research Report

• Project/Area Number: 07680364
• Research Category: Grant-in-Aid for Scientific Research (C)
• Research Institution: Kyushu University
• Principal Investigator: 廣川 佐千男 九州大学, 大学院・システム情報科学研究所, 教授 (40126785)
• Co-Investigator(Kenkyū-buntansha): 古森 雄一 千葉大学, 理学部, 教授 (10022302)
• Keywords: 構成的論理 / 型理論 / ラムダ計算 / 証明システム

Research Abstract

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

Research Products

• [Publications] Sachio Hirokawa: "The proof of a→a in P-W" Journal of Symbolic Logic. 61・1. 195-221 (1996)
• [Publications] Sachio Hirokawa: "A reduction rule for the Peirce formula" Studia Logica. 56・3. 419-426 (1996)
• [Publications] Masako Takahashi: "Normal Proofs and Their Grammars" Information and Computation. 125・2. 144-153 (1996)
• [Publications] 佐塚秀人: "分散する証明推論エンジンのWEB上での結合について" マルチメディアと分散処理ワークショップ論文集. 341-348 (1996)