Applications of Mathematical Logic in Theoretical Computer Science

这个项目的主要目的是从理论和实践的角度研究计算机科学中出现的各种逻辑问题。特别是，我们计划在一开始就把以下主题作为重点。线性逻辑和子结构逻辑，一般而言，作为行动逻辑和资源逻辑，2.基于认知逻辑和累积推理的知识推理，3.基于时态逻辑的软件规范及其验证的描述，4.约简系统，特别是术语重写系统，及其在函数式程序设计语言中的应用1.现在，人们正在用代数方法发展一个没有收缩规则的子结构逻辑的一般理论。研究表明，在无收缩规则逻辑的框架内，可以统一地讨论各种逻辑，包括BCK逻辑、直觉逻辑、卢卡西维茨的多值逻辑，甚至一些模糊逻辑。石原和鹿岛讨论了各种蕴含逻辑及其与类型化的Lambda演算的联系。已有学者对信念修正及其与其他类型推理的关系进行了研究，如归纳推理和累积推理。F.Wolter做了一项非常重要的理论研究，他是1996年我们项目的成员。其中，他在时序逻辑的决策问题上取得了很强的成果。这一主题也与模态逻辑有关。Aoto和Ono与F.Wolter、M.Zakharyaschev和G.Bezhanishvili合作开展了直觉主义模态逻辑的研究，他们在本项目的至少一半任期内一直在JAIST工作。富山和Aoto与M.Sakai合作，在术语重写系统方面取得了有趣的结果，特别是在这些系统的终止性、汇合性和模块化方面，M.Sakai是我们1996年项目的成员。

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.