Experiments in Automatic Theorem Proving.
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The experiments described in this report are proofs in EKL of properties of different LISP programs operating on 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 simultaneously applicable to many different contexts What methods and strategies will make it possible to prove automatically an extensive body of mathematical knowledge Can higher order logic be conveniently applied to proofs of elementary facts
- Computer Programming and Software