---
abstract: "Abstract. We devise a theoretical foundation of directed rewriting, a\r\nterm rewriting strategy for logics of partial functions, inspired by term\r\nrewriting in the Rodin platform. We prove that directed rewriting is\r\nsound and show how to supply new rewrite rules in a soundness preserv-\r\ning fashion. In the context of Rodin, we show that directed rewriting\r\nmakes a signi�cant number of conditional rewrite rules unconditional.\r\nOur work not only allows us to point out a number of concrete ways of\r\nimproving directed rewriting in Rodin, but also has applications in other\r\nlogics of partial functions. Additionally, we give a semantics for the logic\r\nof Event-B."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - matthias.schmalz@inf.ethz.ch
creators_name:
  - family: Schmalz
    given: Matthias
    honourific: ''
    lineage: ''
data_type: ~
date: 2011
date_type: ~
datestamp: 2011-08-16 09:03:26
department: ~
dir: disk0/00/00/03/24
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 324
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: ''
full_text_status: none
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2011-08-16 09:03:26
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: Proceedings of ICFEM 2011
publisher: Springer
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 5
series: ~
skill_areas: []
source: ~
status_changed: 2011-08-16 09:03:26
subjects:
  - theory
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Term Rewriting in Logics of Partial Functions
type: article
userid: 208
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>