Automated Deduction in Mathematics

数学自动演绎

• 批准号: 9503445
• 负责人: Kenneth Kunen
• 金额: $ 12万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-09-01 至 1997-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9503445&HistoricalAwards=false
• 关键词: Automated; Deduction; Mathematics

This research addresses problems in in two major areas: (1) Theorem Proving: Automated deduction is being used to derive mathematical theorems whose proofs would not be feasible without computer assistance. Two facets of this research are: 1a. Search Strategies. This is part of a continuing effort to improve current theorem proving technology. Specific investigations involve: generation, model generation, and linked resolution. 1b. Specific Theorems. New areas of application are being sought out, and well- known open problems involving single axioms for groups and the Robbins algebra problem are being studied. These two facets are closely related. Improvements in theorem prover technology can be applied to proving better theorems. Conversely, proving new theorems gives a way of demonstrating the power of the technology, and failed attempts to prove a theorem can suggest ways in which the technology can be improved. (2) Verification: Here, one uses a computer program to verify existing mathematical theorems. One goal is to develop verification systems far enough so that they could be used as referees for mathematical papers. Concentration is on: (a) The Boyer-Moore prover. This works finitistic mathematics, and is probably the best known existing verification system. The current system includes the ability to do induction on the ordinal epsilon_0. Extensions of this prover are being examined, with an eye to allowing induction on larger ordinals. (b) A prover for set theory. Within axiomatic set theory (ZFC), one can develop all of mathematics. A verification system based on ZFC is being designed. This system will borrow features already used in the Boyer-Moore prover and other systems, but major new problems will be addressed. One problem is how to encode meta-rules, such as the scheme for transfinite induction. Another is how to allow the user to extend the system by adding type declarations (corresponding to informal mathematical statements such as ``from now on, x,y,z will represent real numbers'').

这项研究涉及两个主要领域的问题： (1)定理证明：自动演绎被用于推导数学定理 如果没有计算机的帮助，他们的证明是不可行的。这其中的两个方面 研究：1A。 搜索策略。 这是持续努力的一部分， 改进现有定理证明技术。 具体调查涉及： 生成、模型生成和链接解析。 1b. 具体定理。 新的应用领域正在寻找，著名的开放性问题，涉及单一公理的群体和罗宾斯代数 问题正在研究中。 这两个方面密切相关。 改进 在定理证明器中，技术可以用来证明更好的定理。 相反，证明新的定理提供了一种展示 技术，以及证明定理的失败尝试可以表明， 技术可以改进。 (2)验证：在这里，一个使用计算机 程序来验证现有的数学定理。 一个目标是发展 验证系统足够远，以便他们可以用作裁判， 数学论文 重点是：（a）Boyer-Moore证明器。 这工程 有限数学，可能是最著名的 现有核查制度。 目前的系统包括以下能力： 关于序数ε_0的归纳法。这个证明器的扩展正在研究中，目的是允许在更大的序数上进行归纳。 (b)一 集合论的证明者。 在公理集合论（ZFC）中，人们可以开发 所有的数学。 设计了一个基于ZFC的验证系统。 这 系统将借用已经在Boyer-Moore证明器和其他 系统，但主要的新问题将得到解决。 一个问题是如何编码 元规则，例如超限归纳法。另一个是如何 允许用户通过添加类型声明（相应的 到非正式的数学陈述，如“从现在开始，x，y，z将 表示真实的数字“）。