Experiments in Automatic Theorem Proving

[摘要] 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 compared. 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.

[学科分类] 计算机科学（综合）