---
abstract: "The mathematical language event-B contains powerful syntactic constructs to reason about functions, relations and some other sets. Automatic provers on the other side prefer to work on the smallest syntactic subset of the language that is still expressive.\r\n\r\nThis document describes a translation which:\r\n  • removes most set-theoretic constructs of a predicate.\r\n  • separates arithmetic and set-theoretic constructs from each other.\r\n  • simplifies predicates."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: laurent.voisin@systerel.fr
copyright_holders: []
corp_creators:
  - ETH Zurich
  - Systerel
creators_id:
  - ~
  - laurent.voisin@systerel.fr
creators_name:
  - family: Konrad
    given: Matthias
    honourific: ''
    lineage: ''
  - family: Voisin
    given: Laurent
    honourific: ''
    lineage: ''
data_type: ~
date: ~
date_type: ~
datestamp: 2011-12-16 11:29:54
department: ~
dir: disk0/00/00/03/61
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 361
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: application/pdf;http://deploy-eprints.ecs.soton.ac.uk/361/24/ppTrans.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: unpub
issn: ~
item_issues_comment: []
item_issues_count: ~
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: 2012-03-01 11:02:55
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: technical_report
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: ~
publisher: ETH Zurich
refereed: ~
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 47
series: ~
skill_areas: []
source: ~
status_changed: 2012-02-23 17:35:55
subjects:
  - Proof
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Translation from Set-Theory to Predicate Calculus
type: monograph
userid: 106
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>