Mathematical Sciences: Applied Mathematical Logic

数学科学：应用数理逻辑

• 批准号: 9100665
• 负责人: Kenneth Kunen
• 金额: $ 19.26万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-06-01 至 1996-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9100665&HistoricalAwards=false
• 关键词: Mathematical; Sciences; Applied; Logic

In automated deduction, the project involves the computer verification of proofs of mathematical theorems. It addresses the problem of automatically generating proofs of individual lemmas, and also sets forth a general framework for verifying large fragments of mathematics through a development of axiomatic set theory. In logic programming, the project considers Prolog-style languages. These derive from logic, but there are serious questions about their semantics, and there are several divergent points of view on what a logic program "should" mean. The goal is to clean up the semantics, while still maintaining Prolog's efficiency as a programming language. In set theory and topology, three topics of research are planned. (1) Homogeneity properties of compact spaces. (2) Real-valued measurable cardinals; recent advances by Gitik and Shelah make it reasonable to reconsider some old questions in this area. (3) Martin's Axiom (MA) and uncountable cardinals below the continuum. Specifically, the investigator would like to find models where MA first fails at a singular cardinal of cofinality greater than omega-one and would like to discover consistent PFA-style axioms which allow the continuum to be greater than omega-two. This project thus involves several apparently unrelated areas, logic programming and proof verification on the one hand and set theoretic topology on the other hand. The former has a more obvious relation to practical problems of computer science, but the underlying connection is through the habits of mind cultivated by long study of mathematical logic.

在自动推论中，该项目涉及计算机验证数学定理证明。 它解决了自动生成各个引理证明的问题，并提出了一个通用框架，用于通过公理设置理论的发展来验证数学的大片段。 在逻辑编程中，该项目考虑了序言语言。 这些来自逻辑，但对其语义有严重的问题，并且关于逻辑程序“应该”的意思有几种不同的观点。 目的是清理语义，同时仍保持Prolog作为编程语言的效率。 在集合理论和拓扑中，计划了三个研究主题。 （1）紧凑空间的同质性特性。 （2）实用值可测量的红衣主教； Gitik和Shelah的最新进展使得在该领域重新考虑一些旧问题是合理的。 （3）Martin的公理（MA）和连续体下方的无数枢机主教。 具体而言，研究人员希望找到MA首次在唯一的辅助性基础上失败的模型，而辅助性大于欧米茄（Omega-One），并希望发现一致的PFA式公理，从而使连续体能够大于Omega-Two。 因此，该项目涉及几个显然无关的领域，一方面逻辑编程和证明验证，另一方面设置了理论拓扑。 前者与计算机科学的实际问题有更明显的关系，但是基本的联系是通过长期研究数学逻辑来培养的思想习惯。