权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Applications of Mathematical Logic in Theoretical Computer Science

数理逻辑在理论计算机科学中的应用

基本信息

批准号：
08680356
负责人：
ONO Hiroakira
金额：
$ 1.54万
依托单位：
Japan Advanced Institute of Science and Technology, Hokuriku
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1996
资助国家：
日本
起止时间：
1996 至 1997
项目状态：
已结题

项目摘要

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.

该项目的主要目的是从理论和实践的角度研究计算机科学中出现的各种逻辑问题。特别是，我们计划在会议上重点讨论以下问题。线性逻辑和子结构逻辑，一般来说，作为行动逻辑和资源逻辑，2。基于认知逻辑和累积推理的知识推理;基于时序逻辑的软件规格说明及其验证; 4.约简系统，特别是项重写系统，以及它们在函数式编程语言中的应用。目前，人们正在用代数方法发展一种不需要压缩规则的子结构逻辑的一般理论。研究表明，在没有压缩规则的逻辑框架内，我们可以统一地讨论各种逻辑，包括BCK逻辑、直觉逻辑、Lukasiewicz的多值逻辑，甚至某些模糊逻辑。石原和鹿岛讨论了各种蕴涵逻辑及其与类型lambda演算的联系。One对信念修正及其与其他类型推理（如归纳推理和累积推理）的关系做了一些研究. 1996年我们项目的成员F.Wolter做了一个非常重要的理论研究。除其他外，他获得了强有力的结果的决定问题的时间逻辑。这个主题也与模态逻辑有关。Aoto和Ono与F.Wolter、M.Zakharyaschev和G.Bezhanishvili合作开展了直觉模态逻辑的研究，他们在JAIST至少呆了本项目的一半时间。富山和Aoto获得了有趣的结果，长期重写系统，特别是对终止，汇合和这些系统的模块化，在合作与酒井先生谁是我们的项目的成员在1996年。