Projects per year
Abstract / Description of output
Rippling is a proof search guidance technique with particular application to proof by mathematical induction. It is based on a concept of annotating the differences between two terms. In its original formulation this annotation was only appropriate to first-order formulae. We use a notion of embedding to adapt these annotations appropriately for higher-order syntax. This representation simplifies the theory of annotated terms, no longer requiring special substitution and unification theorems. A key feature of the representation is that it provides a clean separation of the term and the annotation. We illustrate this with selected examples using our implementation of these ideas in λClam.
Original language | English |
---|---|
Pages (from-to) | 57-105 |
Number of pages | 49 |
Journal | Journal of Automated Reasoning |
Volume | 47 |
Issue number | 1 |
DOIs | |
Publication status | Published - Jun 2011 |
Fingerprint
Dive into the research topics of 'The Use of Embeddings to provide a Clean Separation of Term and Annotation for Higher Order Rippling'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Integration and Interaction of multiple mathematical reasoning processes
Bundy, A., Colton, S., Aspinall, D., Dennis, L., Fleuriot, J., Georgieva, L., Ireland, A., Jackson, P. & Smaill, A.
1/04/07 → 31/03/11
Project: Research