Industrial deployment of system engineering methods providing high dependability and productivity


Term Rewriting in Logics of Partial Functions

Schmalz, Matthias (2011) Term Rewriting in Logics of Partial Functions. Proceedings of ICFEM 2011 . (In Press)

Full text not available from this repository.


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 signi�cant 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.

Item Type:Article
Subjects:Event-B > Event-B Theory
ID Code:324
Deposited By:Matthias Schmalz
Deposited On:16 Aug 2011 10:03
Last Modified:16 Aug 2011 10:03

Repository Staff Only: item control page

Deploy-Project - All right reserved