Industrial deployment of system engineering methods providing high dependability and productivity


Translation from Set-Theory to Predicate Calculus

Konrad, Matthias and Voisin, Laurent Translation from Set-Theory to Predicate Calculus. Technical Report. ETH Zurich. (Unpublished)

PDF (ppTrans-2012-03-01) - Updated Version
Available under License Creative Commons Attribution Share Alike.



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.

Item Type:Monograph (Technical Report)
Subjects:Tool developments > Provers
ID Code:361
Deposited By: Laurent Voisin Laurent Voisin
Deposited On:16 Dec 2011 11:29
Last Modified:01 Mar 2012 11:02

Repository Staff Only: item control page

Deploy-Project - All right reserved