
Open access
Author
Date
2011Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
We devise a theoretical foundation of directed rewriting, a term rewriting strategy for logics of partial functions, inspired by term rewriting in the Rodin platform. We prove that directed rewriting is sound and show how to supply new rewrite rules in a soundness preserving fashion. In the context of Rodin, we show that directed rewriting makes a signicant number of conditional rewrite rules unconditional. Our work not only allows us to point out a number of concrete ways of improving directed rewriting in Rodin, but also has applications in other logics of partial functions. Additionally, we give a semantics for the logic of Event-B. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006750722Publication status
publishedPublisher
Eidgenössische Technische Hochschule Zürich, [Department of Computer Science]Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics