Translation from Set-Theory to Predicate Calculus

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.