creators_name: Schmalz, Matthias creators_id: matthias.schmalz@inf.ethz.ch type: article datestamp: 2011-08-16 09:03:26 lastmod: 2011-08-16 09:03:26 metadata_visibility: show title: Term Rewriting in Logics of Partial Functions ispublished: inpress subjects: theory full_text_status: none abstract: 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. date: 2011 publication: Proceedings of ICFEM 2011 publisher: Springer refereed: TRUE citation: Schmalz, Matthias (2011) Term Rewriting in Logics of Partial Functions. Proceedings of ICFEM 2011 . (In Press)