Automated Deduction in 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'').