Quantifiers

Flora has two quantifiers: forall and exists. We have already seen the latter used in Negation. In fact, the use of exists together with \naf is the only use for exists that we know of. We will now discuss forall here.

In Prolog, if we want to check that some condition is true for all values that fulfill a criterion, we would typically collect all the values into a list, and then recursively go through the list. We can do this similarly in Flora. For example, to make sure that all people are either male or female [1], we can use the following:

maleOrFemale([]).
maleOrFemale([?P|?Ps]) :-
  (?P : Male ; ?P : Female), maleOrFemale(?Ps).
@!{MaleOrFemaleValidationQuery} !-
  ?persons = setof{?x | ?x : Person},
  maleOrFemale(?persons).

This style requires us to introduce two new rules, and it is rather difficult to quickly see the meaning of these rules. By using forall in Flora, this can be done more elegantly as:

@!{MaleOrFemaleValidationQuery_Forall} !-
  forall(?p)^(?p : Person ~~> (?p : Male ; ?p : Female)).

The intuitive meaning is familiar to those who know first-order logic, but it is worthwhile to know that there are several layers of “syntactic sugar” at work here. In particular, several implicit \nafs including:

• a ~~> b is shorthand for \naf a \or b (it is also possible to use ==>, which is shorthand for \neg a \or b).
• forall(?x)^p(?x) is shorthand for \naf exists(?x)^(\naf p(?x)).

Thus, the expression

forall(?p)^(?p : Person ~~> (?p : Male ; ?p : Female)).

is shorthand for

\naf exists(?p)^(\naf(\naf ?p : Person \or (?p : Male ; ?p : Female))).

The operational semantics of such an expression is difficult to figure out. If something goes wrong in the forall expression, it can also be daunting to debug.

Note that, as in Prolog, unquantified variables in a Flora fact or rule are implicitly and universally quantified on the outside of the entire fact or rule. This is why we don’t need to add exists and forall in front of all variable occurrences.

Quantifiers may not occur in rule heads or facts, because of their implicit reliance on \naf, which cannot occur in rule heads or facts. See Skolems if you feel the need for existentially quantified variables in facts.

For more on the quantifiers, see section “Arbitrary First-order Formulas in Rule Bodies” in the Flora-2 Manual [2].

[1]	This could be a validation query to make sure our KB is consistent. In most object-oriented languages like Java, we could achieve this by declaring the common super-class, Person, to be abstract. Flora does not have a notion of abstract classes.

[2]	Kifer, Michael, Guizhen Yang, Wan Hui, and Chang Zhao. 2014. Flora-2: User’s Manual. 1.0. Stony Brook University, Stony Brook: Department of Computer Science.