Quantified Expressions in Daplex

Quantified expressions allow the user to specify how a predicate must be applied to the members of a set to determine the truth of the entire expression. For example, for a universally quantified expression to evaluate to true over a given set, the given predicate must evaluate to true for each member of that set, whereas an existentially quantified expression will succeed if there is at least one member of the set for which the predicate is true. The quantifiers provided are:

• all or each
  meaning ``succeed if the predicate is true for all set members'',

• some or any
  meaning ``succeed if there is a least one member of the set for which the predicate succeeds'',

• no
  meaning ``succeed if the predicate is true for none of the elements of the set'',

• at least <n>
  meaning ``succeed if the predicate is true for at least n members of the set'',

• at most <n>
  meaning ``succeed if the predicate is true for at most n members of the set'', and

• exactly <n>
  meaning ``succeed if exactly n members of the set satisfy the predicate''.

Example: print the names of all teachers who teach only fourth year courses.

    |: for each t in teacher such that all c in
    |:		has_course(has_lecturer_inv(t)) have level(c) = 4
    |: print(forename(t), surname(t));