(別紙様式 14)

ABASTRACTS OF RESEARCH PROJECT GRANT-IN-AID FOR SCIENTIFIC RESEARCH (1999)

1. RESEARCH INSTITUTION NUMBER: 12501

2. RESEARCH INSTITUTION: Chiba University

3. CATEGORY: Grant-in-Aid for Scientific Research (C)(2)

4. TERM OF PROJECT: (1998 ∼ 1999)

5. PROJECT NUMBER: 10640103

6. TITLE OF PROJECT: A Study of Substractural Logics

7. HEAD INVESTIGATOR

10022302 Komori, Yuichi Chiba University Faculty of Science Professor

8. INVESTIGATORS

(1) 60183373 Sakurai, Takafumi  Chiba University  Faculty of Science  Assistant Professor
(2) 00291295 Yamamoto, Mitsuharu Chiba University  Faculty of Science  Research Associate
(3) 20261886 Kanazawa, Makoto  Chiba University  Faculty of Letters  Assistant Professor
(4) 40126785 Hirokawa, Sachio  Kyushu University  Computer Center  Professor

(5)

30228994 Fujita, Ken-etsu Kyushu Institute of Technology Faculty of Informatic Technology

Lecturer

9. SUMMARY OF RESEARCH RESULTS

1. Recently lambda calculus unites studies of substructural logics, the intutionistic logic and the classical logic. In this context, Kashima has posed a Natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. Komori has noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system T A_{μ} from Kashima’s system by replacing the introduction of implication by the weakening. While the type assignment system T A_{λ} gives a natural deduction for implicational intuitionistic logic, the type assignment system T A_{μ} gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in T A_{μ} enjoying the subformula property. Still more λ–calculus can be simulated in μ–calculus.

2. A new system of calculus comes out of the above result. We are investigating the meaning of the new calculus.

3. Fujita has actively studied on multiple-conclusion natural deduction system and λμ-calculus, and then has written many papers.

4. The problem on the decidablity of BB’IW logic is one of the most difficult mathematical problem. We are wrestling with the problem.

5. Kanazawa has investigated Categorial Grammars and has gotten excellent results.

6. Sakurai has investigated Categorical model of lambda-calculus and has written two good papers.

10. KEY WORDS

(1) Substructural Logic  (2) Classical Logic  (3) Intuitionistic Logic
(4) BCK Logic  (5) Lambda Calculus  (6) Type Theory

(CONTINUE TO NEXT PAGE)

11. REFERENCES Sachio Hirokawa, A lambda proof of the P − W theorem, The Journal of Symbolic Logic, To appear. Takafumi Sakurai, Categorical Model Construction for Proving Syntactic Properties, Int. Journal of Foundations of Computer Science, To appear. Makoto Kanazawa, Lambek calculus: Recognizing power and complexity, In Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday, (cf. http://turing.wins.uva.nl/ j50/cdrom/) 1999. Ken-etsu Fujita, Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value, Typed Lambda Calculi and Applications (TLCA ’99), LNCS 1581, pages 162–176, 1999. Ken-etsu Fujita, Multiple-Conclusion System as Communication Calculus, Electronic Notes in Theoretical Computer Science (Elsevier Science), Vol. 31, No. 1, pages 167–182, 2000. Keiichi Mishima, GUI for Geometric Inference Engine on Internet, Proceedings of Webnet’99, pages 187– 206, 1999.