Accession Number:

ADA193644

Title:

Term Rewriting: Some Experimental Results,

Descriptive Note:

Corporate Author:

NORTH CAROLINA UNIV AT CHAPEL HILL DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1987-10-01

Pagination or Media Count:

35.0

Abstract:

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.

Subject Categories:

  • Theoretical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE