
Accession Number : ADA327449
Title : Experiments in Automatic Theorem Proving.
Descriptive Note : Technical rept.,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Bellin, Gianluigi ; Ketonen, Jussi
PDF Url : ADA327449
Report Date : DEC 1986
Pagination or Media Count : 283
Abstract : 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?
Descriptors : *SOFTWARE ENGINEERING, *COMPUTER PROGRAM VERIFICATION, COMPUTER LOGIC, MATHEMATICAL LOGIC, PERMUTATIONS.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE