This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
Predicate Logic
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



2.2.3 Predicate Logic
In predicate logic, statements (which are called predicates) can be expressed with variables that can be quantified (e.g. “for all values of …”). EventB uses predicate logic with the following features:
Predicates and expressions are distinguished. All expressions have a data type, e.g. integer or set of integers. Quantification over variables, not predicates, is supported. This includes quantification over sets. A partial function semantics is included, e.g. the predicate is not a tautology because does not represent a valid value. Comprehension sets are supported. Predicates can be evaluated to a Boolean value.
