Experiments with an Interactive Prover for Logic with Equality.
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1971
- Accession Number
- AD0726649
Entities
People
- Gerard Pierre Huet
Organizations
- Case Western Reserve University