| 研究分担者 |
金沢 誠 千葉大学, 文学部, 助教授 (20261886)
山本 光晴 千葉大学, 理学部, 助手 (00291295)
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
藤田 憲悦 九州工業大学, 情報工学部, 講師 (30228994)
廣川 佐千男 (廣川 左千男) 九州大学, 大型計算センター, 教授 (40126785)
|
|---|
| 研究概要 |
1.近年ラムダ計算を介して,部分構造論理,直観主義論理,古典論理の研究が一体化しつつある。その中で鹿島(東京工大)と古典論理の自然演繹体系について研究した。鹿島は古典論理の新しい自然演繹体系を発見した。古森はそれを一部改良し体系CKを得た。体系CKは「ならば除去」,「割増」,「場合わけ」の3つの推論規則を持っている。この体系の発見はまったく新しいものであり,部分論理式特性を持つ古典論理の自然演繹体系の最初のもの(結論がいくつもあるのを認めるとParigotのものがある)である。体系CKについては更にChurch-Rosser性などを調べているところである。この結果は,数学で普通に使われている論理についての結果であるので,各方面から注目されている。
2.上記の結果は新しい計算方式を生んでいる。その計算方式については上で述べたChurch-Rosser性だけでなく,その意味なども調べている。
3.複数の結論を持つ自然演繹体系およびλμ計算とその周辺の研究は,藤田により活発に行なわれ本報告書の研究発表の欄にある二つの論文を生んでいる。
4.BB'IW論理の決定問題はrelevant論理最大の未解決問題であるので,研究代表者,分担者全員で解決にあたっているが,問題が難しくみるべく成果は得られていない。
5.金沢はカテゴリー文法について,それらの構文論的性質や意味論的性質をより明らかにするよう研究を進め成果を得ている。
6.桜井は,ラムダ計算のカテゴリーモデルについての研究を進め,構文論的な性質を証明するためのモデルの構成法について成果を得ている。
|
