2014 Fiscal Year Research-status Report
| Project/Area Number |
24720016
|
|---|
| Research Institution | Nihon University |
|---|
Principal Investigator |
竹村 亮 日本大学, 商学部, 助教 (70583665)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | 論理学 / 証明論 / 図形推論 |
|---|
| Outline of Annual Research Achievements |
20世紀論理学は「文（記号）表現」に基づく「数学における演繹推論」を対象として発展してきた。しかし実際にわれわれが日常的に行う推論においては、図形表現が用いられたり、また演繹推論に限らないさまざまな論法が用いられたりする。本研究では、図形を用いた推論および非単調・非演繹的日常推論の数理モデルを構築することを目指し、本年度は以下の研究を行った。
1. 前年度に引き続き、表を用いた推論を形式化して、Heterogeneous Logic with Tables (HLT) を導入した。また、表を用いた場合の推論と、表を用いずに文表現（論理式）のみを用いた場合の推論とを、計算量および認知的な観点から比較し、表がもっとも有効に働くような推論の特徴づけを行った。（研究業績[2]）
2. さらに、対応表という個別の表現に依存しない、より抽象的なheterogeneous logicの形式化を目指して、HLTを既存の自然演繹の枠組みに自然に埋め込むための方法論の研究を行った。これにより、証明の正規化定理などの伝統的な証明論的手法を、直接heterogeneous logicの分析に応用することが可能になる。
3. 前年度に引き続き、反例モデル構成をオイラー図証明として形式化した。（研究業績[1]）さらに、集合論的モデルに対応するものとしてのオイラー図の伝統的なインフォーマルな利用を、厳密に形式化した。これにより、限られた言語（三段論法言語）では、オイラー図をモデル構成にも、また反例モデル構成にも用いることができることを示した。
4. 本研究で開発してきたオイラー図・ヴェン図システムを教育に応用するために、e-learningコンテンツの開発を行った。（研究業績[3]）
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
教育に対するエフォートの増大に合わせて修正した研究計画をもとに、前年度の研究計画のうちの以下の研究を遂行した。（1）Heterogeneous Logic with Tablesの計算量分析の拡張、（2）オイラー図システムの分析の深化、（3）オイラー図・ヴェン図システムを応用したe-learningコンテンツの開発。
前年度の研究計画のうち、以下の項目は研究途中であり、今年度も継続して研究を行う。（1）種々の図形表現と言語表現を組合せたheterogeneous logicの構築と分析、（2）帰納的推論や類推などの日常的な推論の分析。
|
| Strategy for Future Research Activity |
今後は、以下のような研究を行う。
1. 言語表現や対応表、オイラー図といった個別の表現に依存しない、より抽象的なheterogeneous logicの形式化を目指して、Heterogeneous Logic with Tables (HLT) の分析を進める。とくに、heterogeneous proofの正規化定理を確立する。
2. 本研究で開発してきたオイラー図・ヴェン図システム、対応表システムを、論理学・数学教育に応用し、e-learningコンテンツを含めた教材開発を行う。
3. オイラー図やヴェン図およびグラフ表現と言語表現を組み合わせたHeterogeneous Logicを構築するために、BarwiseのHyperproofを拡張する。また、それを状況意味論やチャンネル理論を基に線形論理の枠組みで分析し、一般的なheterogeneous reasoningを線形論理や多ソート論理などの表現力の豊かなシステムに基づいて形式化して証明論的な分析を行う。
4. 日常的な推論分析については、帰納的推論や類推などの、通常の論理学で扱われる演繹推論以外の推論方式について分析を進める。
|
