Experiments with an Interactive Prover for Logic with Equality.
CASE WESTERN RESERVE UNIV CLEVELAND OHIO SYSTEMS RESEARCH CENTER
Pagination or Media Count:
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
- Statistics and Probability
- Computer Programming and Software