Rodin Handbook


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 $x$ …”). Event-B 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 $1\div 0 = 1\div 0$ is not a tautology because $1\div 0$ does not represent a valid value.

  • Comprehension sets are supported.

  • Predicates can be evaluated to a Boolean value.