Term rewriting: Some experimental results
David A. Plaisted, Richard C. Potter · Carolina Digital Repository (University of North Carolina at Chapel Hill) · 2021
We discuss term rewriting in conjunction with sprfn, a Prolog-based theorem prover. Two techniques for theorem proving that utilize term rewriting are presented. The first technique simulates the replacement of predicates by their definitions in a Skolemtzed setting. The second technique permits tautologies to be recognized quickly. We demonstrate their effectiveness by exhibiting the results of our experiments in proving some theorems of von Neumann-Bernays-Gödel set theory. We also show how the first technique can be used in any clausal theorem prover. Some outstanding problems associated with term rewriting are also addressed.