2008 Fiscal Year Annual Research Report
証明論と論理的意味論の二元論に対する論理哲学と認知科学による統合的研究
Project/Area Number |
07J06005
|
Research Institution | Keio University |
Principal Investigator |
竹村 亮 Keio University, 文学部, 特別研究員(PD)
|
Keywords | 証明論 / 線形論理 / Polarized linear logic / 図形推論 / オイラー図 / ヴェン図 |
Research Abstract |
本研究の目的は、証明論と論理的意味論の二元論的関係を多角的な観点から捉え直すことである。(1)証明論的観点からオイラー図を用いた推論の分析を行った。報告者は共同研究者と共に、オイラー図とヴェン図との考え方の違いが、論理学の観点からは含意結合子を基本とする直観主義論理自然演繹体系と選言標準形を基本とする古典論理の導出原理との間の違いとして特徴付けられることを指摘し、本質的に含意結合子に基づくオイラー図の表現システムを形式化した。また、それに基づくオイラー図の図的推論体系を形式化し、自然な集合論的意味論に対する完全性定理を示した。また共同研究者と共に、オイラー図が実際の三段論法推論において有効であることを実証する実験を行った。(2)線形論理の最小論理とも考えられ、証明探索の研究やゲーム意味論との対応で注目されているPolarized linear logicにおける様相演算子について分析した。命題論理部分のPolarized linear logicは通常のLinear logicの保守的な部分体系であることが知られているが、これが二階の量化子も含めた範囲に拡張できるかどうかは未解決問題であった。報告者は共同研究者と共に、これを肯定的に解決した。このことは、二階の線形論理の論理式に対する自然なpolarityの制限が、証明探索のための正規形の証明図を特徴付けることができるということを示しており、証明探索を基本とするLogic programmingにとっても有用な結果である。(3)報告者は共同研究者と共に、Ludicsにおけるアイデアを基に、証明論と意味論を統合した推論体系であると考えられるIndexed linear logicに対してpolarityを導入し、Indexed polarized linear logicを導入した。
|
Research Products
(7 results)