Accession Number : AD0726649

Title :   Experiments with an Interactive Prover for Logic with Equality.

Descriptive Note : Interim rept.,

Corporate Author : CASE WESTERN RESERVE UNIV CLEVELAND OHIO SYSTEMS RESEARCH CENTER

Personal Author(s) : Huet,Gerard Pierre

Report Date : JUL 1971

Pagination or Media Count : 119

Abstract : A computer program has been developed to prove theorems in first order predicate calculus with equality. This program accepts as input the axioms, definitions and lemmata necessary for the proof, and the negation of the theorem to be proven. It attempts to find a contradiction in this set of clauses, and in case of a success it gives the proof of the theorem, i.e., the chain of deducations necessary to find the inconsistency. The results obtained so far show that the methods used by the program are well suited to the treatment of the equality relation, and that the interactive facilities provide the user with an effective mean of communication with the program in order to direct the proof search. (Author)

Descriptors :   (*MATHEMATICAL LOGIC, *COMPUTER PROGRAMMING), COMPUTER PROGRAMS, MATRICES(MATHEMATICS), NUMBER THEORY, STATISTICAL ANALYSIS, ARTIFICIAL INTELLIGENCE

Subject Categories : Statistics and Probability
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE