Term Rewriting: Some Experimental Results,
NORTH CAROLINA UNIV AT CHAPEL HILL DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
We discuss term rewriting in conjunction with sprfn, a Prolog-based theorem prover. Two techniques for theorem proving that utilize term rewriting are presented. We demonstrate their effectiveness by exhibiting the results of our experiments in proving some theorems of von Neumann-Bernays-Godel set theory. Some outstanding problems associated with term rewriting are also addressed.
- Theoretical Mathematics