creators_name: Konrad, Matthias
creators_name: Voisin, Laurent
creators_id: laurent.voisin@systerel.fr
type: monograph
datestamp: 2011-12-16 11:29:54
lastmod: 2012-03-01 11:02:55
metadata_visibility: show
corp_creators: ETH Zurich
corp_creators: Systerel
title: Translation from Set-Theory to Predicate Calculus
ispublished: unpub
subjects: Proof
full_text_status: public
monograph_type: technical_report
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.

This document describes a translation which:
  • removes most set-theoretic constructs of a predicate.
  • separates arithmetic and set-theoretic constructs from each other.
  • simplifies predicates.
publisher: ETH Zurich
citation:   Konrad, Matthias and Voisin, Laurent   Translation from Set-Theory to Predicate Calculus.  Technical Report. ETH Zurich.    (Unpublished)  
document_url: http://deploy-eprints.ecs.soton.ac.uk/361/24/ppTrans.pdf