Rights / licenseIn Copyright - Non-Commercial Use Permitted
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
PublisherEidgenössische Technische Hochschule Zürich, [Department of Computer Science]
Organisational unit02150 - Dep. Informatik / Dep. of Computer Science
NotesTechnical Reports D-INFK.
MoreShow all metadata