title: Translation from Set-Theory to Predicate Calculus
creator: Konrad, Matthias
creator: Voisin, Laurent
subject: Provers
description: 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
type: Monograph
type: NonPeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/361/24/ppTrans.pdf
identifier:   Konrad, Matthias and Voisin, Laurent   Translation from Set-Theory to Predicate Calculus.  Technical Report. ETH Zurich.    (Unpublished)  
relation: http://deploy-eprints.ecs.soton.ac.uk/361/