The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #513

Title:The Use of Proof Plans for Normalization
Date:Dec 1990
Presented:Submitted to the Festschrift in Honour of Woody Bledsoe
Abstract:We propose using proof plans to implement expression normalizers in automatic theorem proving. We outline some general-purpose proof plans and show how these can be combined in various ways to yield some standard normalizers. We claim that using proof plans facilitates the flexible application of these normalizers so that they can interact with the theorem provers in which they are embedded. We intend to extend this technique to decision procedures.

[Search These Pages] [DAI Home Page] [Comment]