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风格 语言 这些都是从逻辑上推导出来的，但也有严重的 关于它们的语义，有几个不同的问题， 逻辑程序“应该”是什么意思。 目标 是清理语义，同时仍然保持Prolog的 作为编程语言的效率。 在集合论和拓扑学中，三个研究主题是 计划好了 (1)紧空间的齐性性质。（二） 实值可测基数; Gitik和 希拉使重新考虑一些老问题变得合理， 这方面(3)Martin公理（MA）和不可数基数 在连续体之下。 具体来说，调查员希望 找到MA首先在以下奇异基数处失败的模型： 共尾性大于ω 1，并希望发现 一致的PFA式公理，允许连续统是 大于Ω 2 因此，该项目涉及几个显然无关的 一方面，逻辑编程和证明验证 另一方面是集合论拓扑。 前者的 与计算机科学的实际问题有更明显的联系， 但潜在的联系是通过思维习惯 通过长期学习数理逻辑而培养出来的。