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

1993 年度 実績報告書

• 研究課題/領域番号: 05680276
• 研究機関: 九州大学
• 研究代表者: 廣川 左千男 九州大学, 教養部, 助教授 (40126785)
• 研究分担者: 古森 雄一 静岡大学, 理学部, 助教授 (10022302)
• キーワード: 構成的論理 / 型理論 / 線形論理 / ラムダ計算 / 適切さの論理

研究概要

含意命題のBCK論理における正規形の証明図全体はその命題の極小論理式全体と1対1に対応するという知見を得た。これにより、正規形の証明が唯一となる必要十分条件も得られた。BB'IW論理に対応するラムダ項はlinear hereditary right-maximalな項として特徴づけることが出来るという知見を得てP-W問題をラムダの型の問題で表現できるようになった。古森はBB'を含む一連の論理について、カット除去ができるシーケント計算の形式化を行い、P-W問題の統語的解を得た。また、決定問題の計算の複雑さの解析は本質的には、証明図に現われる重複のないシーケントの列の最大長の解析に帰着できそうだという見通しが得られた。直観主義よりも強い構成的論理についてはなんらかの形でラムダ項を拡張する必要があることが分かった。文献調査により、そのような論理を特徴付けるような論理式は多く知られていないことが判明した。
BCK論理,BCI論理,適切さの論理などの直観主義論理の部分論理については、対応する証明図のパターンをラムダ項として特徴付けるという目的はほぼ達成できた。構成的論理の決定問題の解析については、単純な自然推論やラムダ項の探索でははなはだ困難であった。なんらかの構造を持つシーケント計算による形式化と特徴的な論理式の対応の解析が重要な問題である。
無限個証明がある命題のパターンを解析する過程で、古典論理を特徴付るパースの論理式と類似の論理式が得られた。また文献調査により、古典論理の証明から構成的要素を抽出する研究が数件あることが判明した。計画の当初は、直観主義より弱い構成的論理しか念頭になかったが、このことにより研究対象の論理を広げる必要性がでてきた。

研究成果

• [文献書誌] S.Hirokawa: "Principal types of BCK-lambda-terms" Theoretical Computer Science. 107. 253-276 (1993)
• [文献書誌] Y.Komori,S.Hirokawa: "The number of proofs for a BCK-formula" Jornal of Symbolic Logic. 58. 626-628 (1993)
• [文献書誌] S.Hirokawa: "The number of proofs for an implicational formulas" Journal of Symbolic Logic. 58. 1117- (1993)
• [文献書誌] S.Hirokawa: "The relevance graph of a BCK-formula" Journal of Logic and Computation. 3. 269-285 (1993)
• [文献書誌] M.Takahashi,Y.Akama S.Hirokawa: "Normal Proofs and Their Grammar" Lecture Notes in Computer Science. (発表予定).
• [文献書誌] S.Hirokawa: "The proofs of alpha->alpha in P-W" Journal of Symbolic Logic. (発表予定).
• [文献書誌] R.Kashima,Y.Komori: "The word problem for free BCI-algebras is decidable" Mathematica Japonica. 37. 1025-1029 (1992)
• [文献書誌] Y.Komori: "Syntactical Investigations into BI Logic and BB'I Logic" Studia Logica. (発表予定).