|
昨年度までの研究を踏まえて今年は証明探索との関連を通いてproofnetの特徴付け定理の意義を吟味した。線形論理ではparaproofと呼はれる証明より広い概念を用い、paraproofの中で特徴付け定理による条件を満たすものが証明であると評定される。また、プログラシング言語理論において重要な関数の性質である合流性を保証する論理学的な性質が特徴付け定理ということもできるのではないか。また証明に関する研究を論理体系(構文的)に対する分析的アプローチと一貫性空間(意味的)に対する大域主義的アプローチの観点から行い、証明探索における2大要素として、分解と分割を得るに到った。
今後線形論理を発展させたlocative logicに関する様様な研究がなされるであろうが少なくとも以下の観点は注目に値するであろう。
1.対話型証明探索はサーバクライコントモデルの理論となりうるか
2.論理学から"記憶機能"を提供できるか
3.論理はソフトウェア工学の基礎となりうるか
アブストラクション(描象)…オブジュクト指向
リプリゼンテーション(表現)…効率的なメモリ管理に適切な型(共用型)の理論
|
