部分構造論理の研究

研究課題番号：10640103

1999年度 研究成果報告書概要

代表者

    • 古森 雄一
    • KOMORI, Yuichi
    • 研究者番号：10022302
    • 千葉大学・理学部・教授

研究課題基本情報

  • 研究期間

    1998年度〜1999年度

  • 研究分野

    数学一般(含確率論・統計数学)

  • 審査区分

    一般

  • 研究種目

    基盤研究(C)

  • 研究機関

    千葉大学

  • 配分額

    • 1998年度：2200千円 (直接経費：2200千円)
    • 1999年度：1600千円 (直接経費：1600千円)

研究分担者

    • 金沢 誠
    • 研究者番号：20261886
    • 千葉大学・文学部・助教授
    • 山本 光晴
    • 研究者番号：00291295
    • 千葉大学・理学部・助手
    • 桜井 貴文
    • 研究者番号：60183373
    • 千葉大学・理学部・助教授
    • 藤田 憲悦
    • 研究者番号：30228994
    • 九州工業大学・情報工学部・講師
    • 廣川 佐千男
    • 研究者番号：40126785
    • 九州大学・大型計算センター・教授

研究概要

1.近年ラムダ計算を介して,部分構造論理,直観主義論理,古典論理の研究が一体化しつつある。その中で鹿島(東京工大)と古典論理の自然演繹体系について研究した。鹿島は古典論理の新しい自然演繹体系を発見した。古森はそれを一部改良し体系CKを得た。体系CKは「ならば除去」,「割増」,「場合わけ」の3つの推論規則を持っている。この体系の発見はまったく新しいものであり,部分論理式特性を持つ古典論理の自然演繹体系の最初のもの(結論がいくつもあるのを認めるとParigotのものがある)である。体系CKについては更にChurch-Rosser性などを調べているところである。この結果は,数学で普通に使われている論理についての結果であるので,各方面から注目されている。

2.上記の結果は新しい計算方式を生んでいる。その計算方式については上で述べたChurch-Rosser性だけでなく,その意味なども調べている。

3.複数の結論を持つ自然演繹体系およびλμ計算とその周辺の研究は,藤田により活発に行なわれ本報告書の研究発表の欄にある二つの論文を生んでいる。

4.BB'IW論理の決定問題はrelevant論理最大の未解決問題であるので,研究代表者,分担者全員で解決にあたっているが,問題が難しくみるべく成果は得られていない。

5.金沢はカテゴリー文法について,それらの構文論的性質や意味論的性質をより明らかにするよう研究を進め成果を得ている。

6.桜井は,ラムダ計算のカテゴリーモデルについての研究を進め,構文論的な性質を証明するためのモデルの構成法について成果を得ている。

発表文献

  • 廣川佐千男: "A lambda proof of the P-W theorem"The Journal of Symbolic Logic. (発表予定).

  • 桜井貴文: "Categorical Model Construction for Proving Syntactic Properties"International J. F. Computer Science. (発表予定).

  • 金沢誠: "Lambek calculus : Recognizing power and complexity"Essays Dedicated to Johan van Benthem. (1999)

  • 藤田憲悦: "Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value"TLCA '99, LNCS 1581. 162-176 (1999)

  • 藤田憲悦: "Multiple-Conclusion System as Communication Calculus"Electronic Notes in Theoretical Computer Science. 31・1. 167-182 (2000)

  • Keiichi Mishima: "GUI for Geometric Inference Engine on Internet"Proceedings of Webnet'99. 1360-1361 (1999)

このページのURI

http://kaken.nii.ac.jp/ja/p/10640103/1999/6/ja