WOLTER Frank 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20272990)
KASHIMA Ryo School of Information Science, JAIST, Research Associate, 情報科学研究科, 助手 (10240756)
酒井 正彦 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597)
ISHIHARA Hajime School of Information Science, JAIST,Associate Professor, 情報科学研究科, 助教授 (10211046)
TOYAMA Yoshihito School of Information Science, JAIST,Professor, 情報科学研究科, 教授 (00251968)
AOTO Takahito School of Information Science, JAIST, Research Associate, 情報科学研究科, 助手 (00293390)
|Budget Amount *help
¥2,400,000 (Direct Cost : ¥2,400,000)
Fiscal Year 1997 : ¥1,300,000 (Direct Cost : ¥1,300,000)
Fiscal Year 1996 : ¥1,100,000 (Direct Cost : ¥1,100,000)
Main aim of this project is to study various logical problems appearing in computer science from both theoretical and practical point of view. In particular, we planned to bring the following subjects into focus, at the beginning.
1. linear logic and substructural logics, in general, as logic of action and logic of resources,
2. reasoning about knowledge, based on epistemic logic and cummulative reasoning,
3. descriptions of specifications of software based on temporal logics and their verifications,
4. reduction systems, in particular, term rewriting systems, and their applications to functional programming languages.
1. One is now developing a general theory of substructural logics without contraction rule, by using algebraic methods. The study shows that within the framework of logics without contraction rule, we can discuss various kinds of logics, including BCK logics, intuitionistic logic, Lukasiewicz's many-valued logics and even some of fuzzy logics in a uniform way. Ishihara and Kashima discussed various implicational logics and their connections with typed lambda calculi.
2. Some studies has been done by One in belief revision and its relation to reasoning of other types, like inductive reasoning and cummulative reasoning.
3. A very important theoretical study has been done by F.Wolter, who was a member of our project in 1996. Among others, he obtained strong results on the decision problems on temporal logics. This topics is related also to modal logic. Aoto and Ono have developed the study of the intuitionistic modal logics in collaboration with F.Wolter, M.Zakharyaschev and G.Bezhanishvili, who stayd at JAIST at least a half of the term of the present project.
4. Toyama and Aoto obtained interesting results on term rewriting systems, in particular on the termination, the confluence and the modularity of these systems, in collaboration with M.Sakai who was a member of our project in 1996.