TY  - UNPB
ID  - deploy361
UR  - http://deploy-eprints.ecs.soton.ac.uk/361/
A1  - Konrad, Matthias
A1  - Voisin, Laurent
N2  - 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.
PB  - ETH Zurich
TI  - Translation from Set-Theory to Predicate Calculus
M1  - technical_report
AV  - public
ER  -

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>