The clause-linking theorem proving method was recently developed and tested on a wide variety of problems, including problems in set theory and temporal logic, and logic puzzles. This prover converts a first- order problem to the propositional calculus and then applies a propositional decision procedure similar to the Davis and Putnam method. This project will extend this theorem proving method to problems involving equality and term rewriting. This involves a combination of representations like Brand's modification method, with traditional term-rewriting techniques. A procedure to solve inequalities involving the lexicographic path ordering will be used to approximate specialized unification algorithms. This work will also incorporate meaningful semantics to guide the search; the semantics will be presented as a collection of procedures for computing the meanings of function and predicate symbols in a structure, as well as a procedure for deciding the satisfaction of existential sentences in the structure. Methods for generating plausible lemmas and using them to guide the search for a proof, will be developed. The prover will be applied to non-trivial mathematical theorems.
