Logic and Computability

逻辑和可计算性

• 批准号: 0100035
• 负责人: Richard Shore
• 金额: $ 30万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-06-01 至 2007-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0100035&HistoricalAwards=false
• 关键词: Logic; Computability

The proposed project includes research into a broad range of topics in computability theory (recursion theory) and logic both theoretical and applied to other areas of mathematics and computer science. Included in the first area are investigations of the structures of sets and functions ordered by relative complexity of computation. Particular emphasis will be placed on the issue of definability in the complexity structures of all sets and those which are effectively enumerable. Included in this area is the analysis of the relations between difficulty of computing functions and other issues such as rates of growth, complexity of their definitions in arithmetic and the strength of axiom systems needed to prove their existence. Applications of the methods of pure computability theory will be made in the areas of computable algebra and model theory. General methods will be developed for transferring results from arbitrary structures to ones in specific classes of interest such as lattices, groups and rings. Another area where issues of computability and complexity are to be studied is that of modal and intuitionistic logics and their model theory. These logics are now used to model issues in program verification and computer security. The second area includes the study of structures representable by finite automata, decision procedures, the analysis and development of nonmonotonic logic, concurrent programming models, and applications of linear programming ideas and algorithms to data structures and logic programming. A primary focus here will be the logical and mathematical foundations of hybrid (continuous and discrete) control theory as well as the practical implementation of algorithms for these subjects based on the theoretical work being done. An important tool to be developed in this area is that of infinitary automata.The research proposed is of two types. The first is directed at a better understanding of the fundamental notions of computability and relative difficulty of computation for different tasks. The theoretical work deals both with the abstract notion of computability as well as with applications to specific branches of, and questions in, other areas of mathematics. One important application (within mathematics) concerns the general question of what starting information is needed to be able to compute various aspects of many important classes of mathematical structures. In practical terms, the results at times indicate that there are no algorithms for certain important tasks or that more information than might have been expected is needed to write programs calculating the desired results. Another aspect of this work stresses the impact that the specific concrete choice of representation of an abstract mathematical structure has on one's ability to compute specific functions and relations. The second type deals more directly with developing the mathematical (and especially logical) tools needed for the crucial areas of program verification, data management and automated control of real-world complex systems. Commercial applications are expected for some of this work and there has already been a spin off to a start-up company developing several applications including data compression and network management algorithms. Other applications of these techniques to be investigated include multimedia applications and distributed continuous systems.

拟议的项目包括对计算理论（递归理论）的广泛主题的研究，以及理论上的逻辑，并应用于数学和计算机科学的其他领域。在第一个领域包括对计算相对复杂性的集合和功能结构的研究。在所有集合的复杂性结构以及有效枚举的复杂性结构中的确定性问题上，将特别强调。该领域中包括的是对计算功能难度与其他问题之间的关系的分析，例如增长率，其定义的复杂性以及证明其存在所需的公理系统的强度。纯计算性理论方法的应用将在可计算的代数和模型理论的领域中进行。将开发一般方法，以将结果从任意结构转移到特定类别的兴趣类别（例如晶格，组和环）中。要研究计算性和复杂性问题的另一个领域是模态和直觉逻辑及其模型理论。这些逻辑现在用于建模程序验证和计算机安全性问题。第二个领域包括对有限自动机代表的结构，决策程序，非单调逻辑的分析和开发，并发编程模型以及线性编程思想和算法在数据结构和逻辑编程中的应用。这里的主要重点将是混合（连续和离散）控制理论的逻辑和数学基础，以及基于所做的理论工作的这些主题的算法的实际实施。在该领域要开发的一个重要工具是无限自动机。提出的研究是两种类型。第一个针对不同任务的计算性和相对难度的基本概念有了更好的理解。理论工作既涉及可计算性的抽象概念，也涉及到其他数学领域的特定分支和问题的应用。一个重要的应用（在数学中）涉及一个总体问题，即能够计算许多重要类数学结构的各个方面需要什么起始信息。实际上，有时的结果表明，对于某些重要任务没有算法，或者编写程序计算所需结果所需的信息比预期的要比预期的要多。这项工作的另一个方面强调了特定的混凝土对抽象数学结构的表示对计算特定功能和关系的能力的影响。第二种类型更直接地涉及开发计划验证，数据管理和对现实世界复杂系统自动化控制的至关重要领域所需的数学（尤其是逻辑）工具。预计某些工作的商业应用程序已经有了一家开发多个应用程序的初创公司，包括数据压缩和网络管理算法。这些技术的其他应用包括多媒体应用和分布式连续系统。