Report Number: CS-TR-87-1155
Institution: Stanford University, Department of Computer Science
Title: Experiments in Automatic Theorem Proving
Author: Bellin, G.
Author: Ketonen, J.
Date: December 1986
Abstract: The experiments described in this report are proofs in EKL of
properties of different LISP programs operating different
representations of the same mathematical structures -- finite
permutations. EKL is an interactive proof checker based upon
the language of higher order logic, higher order unification
and a decision procedure for a fragment of first order logic.
The following questions are asked: What representations of
mathematical structure and facts are better suited for
formalization and also applicable to several interesting
situations? What methods and strategies will make it possible
to prove automatically an extensive body of mathematical
knowledge? Can higher order logic be conveniently applied in
the proof of elementary facts?
The fact (*) that finite permutations form a group is proved
from the axioms of arithmetic and elementary set theory, via
the "Pigeon Hole Principle" (PHP). Permutations are
represented (1) as association lists and (2) as lists of
numbers. In representation (2) operations on permutations are
represented (2.1) using predicates (2.2) using functions.
Proofs of (*) using the different representations are
The results and conclusions include the following. Methods to
control the rewriting process and to replace logic inference
by high order rewriting are presented. PHP is formulated as a
second order statement which is then easily applied to (1)
and (2). This demonstrates the value of abstract, higher
order formulation of facts for application in different
contexts. A case is given in which representation of
properties of programs by predicates may be more convenient
than by functions. Evidence is given that convenient
organization of proofs into lemmata is essential for large
scale computer aided theorem proving.