Computer Understanding of Mathematical Proofs

Abstract

Mathematical proofs constitute a mixture of formulas with a subset of natural language. They can be represented as a sequence of lines expressible in the symbolism of predicate calculus. The transition from step to step may depend on a series of logical manipulations and/or on intricate mathematical knowledge associated with the domain of the proof. The organization of the proof may depend on different conventions adopted by mathematicians in communication with each other. This paper deals with problems involved in following the mathematical argument along those lines. Some of the ideas were implemented as a part of a system for teaching axiomatic set theory to college students. The most powerful and frequently used rules of inference utilize a resolution theorem prover. To the best of our knowledge this is the only resolution theorem prover, perhaps the only general purpose theorem prover used in actual production.