Term rewriting in logics of partial functions
OPEN ACCESS
Author / Producer
Date
2011
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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 preserv ing fashion. In the context of Rodin, we show that directed rewriting makes a significant 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.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
732
Pages / Article No.
Publisher
ETH Zurich, Department of Computer Science
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science