
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