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):

• Potter, Richard
• Plaisted, David

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.

Descriptors:

• *MATHEMATICAL MODELS
• *WRITING
• *SET THEORY
• THEOREMS
• DISTRIBUTION THEORY
• INDEX TERMS
• MATHEMATICAL LOGIC

Subject Categories:

• Theoretical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE