?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Translation+from+Set-Theory+to+Predicate+Calculus&rft.creator=Konrad%2C+Matthias&rft.creator=Voisin%2C+Laurent&rft.subject=Provers&rft.description=The+mathematical+language+event-B+contains+powerful+syntactic+constructs+to+reason+about+functions%2C+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.%0D%0A%0D%0AThis+document+describes+a+translation+which%3A%0D%0A++%E2%80%A2+removes+most+set-theoretic+constructs+of+a+predicate.%0D%0A++%E2%80%A2+separates+arithmetic+and+set-theoretic+constructs+from+each+other.%0D%0A++%E2%80%A2+simplifies+predicates.&rft.publisher=ETH+Zurich&rft.type=Monograph&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F361%2F24%2FppTrans.pdf&rft.identifier=++Konrad%2C+Matthias+and+Voisin%2C+Laurent+++Translation+from+Set-Theory+to+Predicate+Calculus.++Technical+Report.+ETH+Zurich.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F361%2F