(別紙様式 13) 平成１１年度科学研究費補助金成果報告概要

1. 機関番号 2. 研究機関名

3. 研究種目名 4. 研究期間

平成年度〜平成年度

5. 課題番号

6. 研究課題名

7. 研究代表者

研究者番号研究代表者名所属部局名職名

フリガナ

8. 研究分担者(所属機関名は，研究代表者の所属機関と異なる場合に記入すること。 )

研究者番号研究分担者名所属機関名・所属部局名職名

フリガナ

フリガナ

フリガナ

フリガナ

フリガナ

9. 研究成果の概要 (当該研究期間のまとめ， 6 0 0 字〜 8 0 0 字で記入。図，グラフ等は記載しないこと。 )

10. キーワード

(1)  (2)  (3)
(4)  (5)  (6)

(7) (8)

(裏面に続く)

千葉大学

基盤研究 (C)(2)

部分構造論理の研究

10  11

{1 2 5 0 1 \atop 1 0 6 4 0 1 0 3}

1 0 0 2 2 3 0 2  古森,  雄一^{コモリ ユウイチ}理学部教授

6 0 1 8 3 3 7 3  桜井,  貴文^{サクライ タカフミ}理学部助教授
0 0 2 9 1 2 9 5  山本,  光晴^{ヤマモト ミツハル}理学部助手
2 0 2 6 1 8 8 6  金沢,  誠^{カナザワ マコト}文学部助教授
4 0 1 2 6 7 8 5  廣川,  佐千男^{ヒロカワ サチオ}九州大学・大型計算機センター教授
3 0 2 2 8 9 9 4  藤田,  憲悦^{フジタ ケンエツ}九州工業大学・情報工学部講師

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

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

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

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

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

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

部分構造論理古典論理直観主義論理 BCK 論理ラムダ計算型理論 11. 研究発表 (印刷中も含む。)

［雑誌論文］

著者名発行年

論文標題

雑誌名巻・号ページ著者名

発行年

論文標題

雑誌名巻・号ページ著者名

発行年

論文標題

雑誌名巻・号ページ著者名

発行年

論文標題

雑誌名巻・号ページ著者名

発行年

論文標題

雑誌名巻・号ページ著者名

発行年

論文標題

雑誌名巻・号ページ

［図 書］

著者名発行年

出版者

書名総ページ数著者名

発行年

出版者

書名総ページ数

廣川佐千男  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  1 9 9 9
藤田憲悦  Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value
TLCA ’99, LNCS 1581 1 9 9 9 162 176
藤田憲悦  Multiple-Conclusion System as Communication Calculus
Electronic Notes in Theoretical Computer Science 31 ・ 1 2 0 0 0 167 182
Keiichi Mishima  GUI for Geometric Inference Engine on Internet
Proceedings of Webnet’99  1 9 9 9 1360  1361