RUI: Fixed-Point Logic in Finite Structures

RUI：有限结构中的定点逻辑

• 批准号: 9003356
• 负责人: Steven Lindell
• 金额: $ 5.07万
• 依托单位: Haverford College
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-08-01 至 1994-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9003356&HistoricalAwards=false
• 关键词: RUI; Fixed; Point; Logic; Finite

The study of algorithms involves two important aspects, correctness and complexity. This project addresses these two aspects from a machine independent viewpoint by using formulas of mathematical logic. Logic formulas can provide descriptions of solutions to problems which can then be analyzed for their correctness and complexity. Of particular interest is to develop a feasible set of logical formulas for P, the class of problems which are tractable, i.e., whose solutions require only a polynomial number of machine steps, and in addition, to provide a system for reasoning about the properties of these logical formulas. Finding a comprehensive description of such a set of formulas would exhibit a machine independent definition of P and have a significant impact on our understanding of the algorithms for this important complexity class. If successful, this system could provide a method by which one could demonstrate that a given formula is the correct solution to certain problem. As an alternative to program correctness, this may provide a deeper understanding of algorithmic correctness.

算法的研究涉及两个重要的方面，正确性和复杂性。 该项目通过使用数学逻辑公式从独立于机器的角度解决了这两方面问题。 逻辑公式可以提供问题解决方案的描述，然后可以分析其正确性和复杂性。 特别令人感兴趣的是为 P 开发一组可行的逻辑公式，这是一类易于处理的问题，即其解决方案仅需要多项式机器步骤，此外，还提供一个用于推理这些逻辑公式的属性的系统。 找到这样一组公式的全面描述将展示 P 的机器独立定义，并对我们对这一重要复杂性类别的算法的理解产生重大影响。 如果成功，该系统可以提供一种方法，通过该方法，人们可以证明给定的公式是特定问题的正确解决方案。 作为程序正确性的替代方案，这可以提供对算法正确性的更深入的理解。