Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #93127 | |
|---|---|
| Title: | Implementing a Wave Rule Parser in Clam |
| Authors: | Narine,G |
| Date: | 1993 |
| Presented: | |
| Keywords: | |
| Abstract: | Rippling, a heuristic used to reduce search space in inductive proofs, uses a special class of rewrite rules known as wave-rules. Attempts have been made to formally describe what constitutes a valid wave-rule by specifying general wave-rule formats. Recently, interest has grown in alternative ways of describing wave-rules, based on meta-level properties of rewrite rules. This project outlines the implementation of a prototype wave-rule parser based on these new ideas. The performance of the parser is compared with that of existing CLAM parser by testing them on a range of examples. it is shown that the prototype parser extracts all the wave-rules that the existing CLAM parser does within the constraints of the implementation, and more besides. |
| Download: | NO ONLINE 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}