Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #9824 | |
|---|---|
| Title: | Using Rippling for Equational Reasoning |
| Authors: | Metcalfe,PM |
| Date: | 1998 |
| Presented: | |
| Keywords: | |
| Abstract: | Rippling, a heuristic originally developed in the field of inductive theorem proving [Bundy et al. 93], is used here to guide equality proofs. Following Dieter Hutter's work in the area, common (syntactically identical) parts of two sides of an equation are found and brought together using rippling. Rewriting of these common parts is then restricted, pruning the search space and hopefully making progress in the proof. In order to find more common parts, difference reducing bridge lemmas are also applied, using (where necessary) rippling and further bridge lemmas to prepare the selected side of the equation. Bridge lemmas are chosen (in the current project) with the goal of equalising multisets of occurring function symbols.The strategy has been implemented in Sicstus PROLOG as part of the CLAM system [Bundy et al. 90] and tested on 80 theorems from a variety of mathematical fields (44 from the TPTP file [Suttner & Sutcliffe 97], proving 53 (18 from the TPTP file). |
| 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}