Term Rewriting: Some Experimental Results,

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1987
Accession Number
ADA193644

Entities

People

  • David Plaisted
  • Richard Potter

Organizations

  • University of North Carolina at Chapel Hill

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Computer Science
  • Computers
  • Military Research
  • North Carolina
  • Plastic Explosives
  • Preprocessing
  • Set Theory
  • Standards
  • Theorems
  • Universities

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.