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

MSc Thesis #93127

Title:Implementing a Wave Rule Parser in Clam
Date: 1993
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.

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