A Program for Generating and Analyzing Term Rewriting Systems

This thesis presents new results in the use of term rewriting systems for automatic theorem proving. The design and implementation of REVE 2, a computer program that incorporates these results, is described. In addition, an introduction to the basic theory, procedures, and algorithms of term rewri...

Full description

Bibliographic Details
Main Author: Forgaard, Randy
Other Authors: Guttag, John V.
Published: 2023
Online Access:https://hdl.handle.net/1721.1/149613
Description
Summary:This thesis presents new results in the use of term rewriting systems for automatic theorem proving. The design and implementation of REVE 2, a computer program that incorporates these results, is described. In addition, an introduction to the basic theory, procedures, and algorithms of term rewriting is provided, in a manner suitable for non-specialists.