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