Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #513 | |
|---|---|
| Title: | The Use of Proof Plans for Normalization |
| Authors: | Bundy,A |
| Date: | Dec 1990 |
| Presented: | Submitted to the Festschrift in Honour of Woody Bledsoe |
| Keywords: | |
| 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. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}