The Use of Embeddings to provide a Clean Separation of Term and Annotation for Higher Order Rippling

Louise Abigail Dennis, Alan Smaill, Ian Green

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)57-105
Number of pages49
JournalJournal of Automated Reasoning
Volume47
Issue number1
DOIs
Publication statusPublished - 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.

Cite this