Automated Development of Fundamental Mathematical Theories
Arthur William Quaife, J. W. Addison · 1992
I provide an introduction to automated reasoning, and in particular to resolution theorem proving using the prover OTTER written by William McCune. I explain such concepts as clauses, substitutions, unification, binary resolution, hyperresolution, UR-resolution, paramodulation, demodulation, set-of-support strategy, subsumption, weighting, and lexical ordering. I present a new clausal version of von Neumann-Bernays-Godel set theory. A complete set of reductions for Boolean rings is given. I list over 400 theorems proved semi-automatically in elementary set theory, and supply the proofs of several of these, including Cantor's theorem. I present a semiautomated proof that the composition of homomorphisms is a homomorphism, thus solving a challenge problem from the literature. Using the clauses and heuristics presented, there is no apparent obstacle to the semiautomated development of set theory through considerably more difficult theorems. I develop Peano's Arithmetic, and give more than 1200 definitions and theorems in elementary number theory. I describe how I use a resolution theorem prover to prove theorems by induction. The definition principles I permit are described, including definition by primitive recursion. I present a schema by which metatheorems may be proved using resolution theorem prover. OTTER-generated proofs are presented of the Greek classics that the square root of any prime is irrational, and that there are infinitely many primes. I give part of the proof of the fundamental theorem of arithmetic (unique factorization), and part of the proof that justifies an algorithm for computing the greatest common divisor of two numbers from their factorizations. I give an OTTER-generated proof of Euler's generalization of Fermat's theorem. I develop Tarski's geometry, a complete first-order axiomatization of Euclidean plane geometry, within OTTER. I obtain proofs and supply performance statistics for most of the challenge problems appearing in the literature. Few of these problems have been previously solved by any clause-based reasoning system. I offer further challenges. I formalize the modal logic calculus K4, which represents important properties of the provability relation of Peano's Arithmetic, within OTTER. I obtain very high level automated proofs of Lob's theorem, and of Godel's two incompleteness theorems.