Automated Deduction in Mathematics

本研究解决了两个主要领域的问题：(1)定理证明：自动演绎被用于推导数学定理，这些定理的证明如果没有计算机的帮助是不可行的。本研究的两个方面是：搜索策略。这是改进现有定理证明技术的持续努力的一部分。具体研究包括：生成、模型生成和关联分辨率。1 b。特定的定理。正在寻找新的应用领域，并且正在研究涉及群的单一公理和罗宾斯代数问题的众所周知的开放问题。这两个方面是密切相关的。定理证明器技术的改进可以用来证明更好的定理。相反，证明新定理提供了一种展示技术力量的方法，而证明定理的失败尝试可以提出改进技术的方法。(2)验证：在这里，人们使用计算机程序来验证现有的数学定理。其中一个目标是开发足够远的验证系统，以便它们可以用作数学论文的审稿人。重点是：(a) Boyer-Moore证明。这适用于有限数学，可能是最著名的现有验证系统。目前的系统包括对序数epsilon_0的归纳。这个证明的扩展正在研究中，目的是允许在更大的序数上进行归纳。(b)集合论的证明者。在公理集理论（ZFC）中，人们可以发展所有的数学。设计了一个基于ZFC的验证系统。该系统将借鉴Boyer-Moore证明器和其他系统中已经使用的功能，但将解决主要的新问题。一个问题是如何对元规则进行编码，比如超限归纳的方案。另一个是如何允许用户通过添加类型声明来扩展系统（对应于非正式的数学语句，如“从现在开始，x,y，z将表示实数”）。

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'').