Mathematical Sciences: Applied Mathematical Logic

在自动演绎中，该项目涉及对数学定理证明的计算机验证。它解决了自动生成单个引理证明的问题，并通过公理集理论的发展提出了验证数学大块的一般框架。在逻辑编程中，该项目考虑了prolog风格的语言。它们来源于逻辑，但是它们的语义存在严重的问题，并且对于逻辑程序“应该”意味着什么存在几种不同的观点。目标是清理语义，同时仍然保持Prolog作为编程语言的效率。在集合论和拓扑学方面，规划了三个研究课题。(1)紧空间的齐次性。(2)实值可测基数；Gitik和Shelah的最新进展使我们有理由重新考虑这一领域的一些老问题。(3)马丁公理（MA）和连续统以下的不可数基数。具体地说，研究者希望找到模型，其中MA首先在大于ω - 1的共合性的单一基数上失败，并希望发现一致的pfa式公理，允许连续体大于ω - 2。因此，这个项目涉及几个看似不相关的领域，一方面是逻辑编程和证明验证，另一方面是集合论拓扑。前者与计算机科学的实际问题有更明显的关系，但其潜在的联系是通过长期研究数理逻辑所培养的思维习惯。

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.