Quantifiers and Omniform Rules

The Implications ==> and ~~>

The if-then implications are often used in Ergo both in rule heads and bodies in conjunction with quantifiers (and without them). The details can be found ErgoAI Reasoner User's Manual, sections "General Formulas in Rule Bodies" and "General Formulas in Rule Heads."  Here we will just highlight the main points.

Ergo has the following implications:

• p~~>q  and  q<~~p  --  both equivalent to  q \or \naf p

• p==>q  and  q<==p  --  both equivalent to  q \or \neg p

• p<~~>q  --  equivalent to  p<~~q \and p~~>q

• p<==>q  --  equivalent to  p<==q \and p==>q

These implications are different from each other and from :-.   The :- connective is the one that separates rule heads from rule bodies, while the above implications do not -- they appear as subgoals in rule heads or bodies. More precisely:

• ~~>, <~~, <~~> can appear only in rule bodies, i.e., to the right of :-.

• ==>, <==, <==>  can appear both in rule heads and bodies.

  • However, usually they appear in rule heads only; their use in rule bodies is for experts who are well-versed in various types of negation used in Ergo and understand the semantics well.

Note: it is tempting to think of statements like this

p(?X) <== q(?X,?Y),r(?Y).

as having a head p(?X) and a body q(?X,?Y),r(?Y), but in Ergo-speak this is not the case. A head is something that occurs to the left of the :- connective and a body is something that occurs to the right.  At best, the above statement can be considered as occurring entirely in the head of a rule that has an empty body.  In section "Omniform Rules," we  will see that such a statement is a shortcut for several ordinary rules (having a :- connective). 

Quantifiers: forall/exist

Logical quantifiers are very important in knowledge representation, especially in translating sentences from natural language to logic. For instance, a query such as ``find all students that have taken every course offered by some professor in some year,''  when translated into logic, requires three quantified variables: Course, Professor, and Year: the first being quantified universally and the second and third existentially.  The variable Student is the one whose values we want as an answer --- it is a free variable. Most logic languages for knowledge representation support only existential quantification, making queries such as above extremely cumbersome to express. 

Ergo supports both the universal quantifier, forall (synonyms: all, each), and the existential quantifier, which can be written as  exist,  exists, or some. The general syntax is this:

• forall(?Var1,...,?VarN)^(body) -- body must be true for all possible bindings of the listed variables.

• exist(?Var1,...,?VarN)^(body)  -- body must be true for some binding of each of the listed variables.

• exists(?Var)^(body)  -- alternative form of exist; normally used with one variable, but this is not enforced and any number of variables can appear.

Here body  can be any formula that is allowed in rule bodies and all the variables in the quantifier's list of variables must occur inside body. If  body  has the form of a frame or a single predicate (or of another quantified formula) then the surrounding parentheses are optional.

The following examples illustrate quantification in rule body and rule head.

• Example of the use of quantifiers in rule body:

?P[completed_core_requirements->?Stu]  :-

?P:CollegeProgram,

?Stu:Student,

forall(?Course)^exists(?Semester)^(

         ?P[core_course->?Course] ~~> transcript(?Stu,?Course,?Semester,?_Grade)

).

This rule defines a property of college programs, called completed_core_requirements, which returns all the students who, according to their transcript, have completed all the courses that are designated as core courses for the given program.  In slightly more explicit, technical terms, the above rule defines a set of ?P -- ?Stu pairs such that:

1. ?P is a program and ?Stu is a student;

2. For every ?Course there is ?Semester such that:

   1. • If ?Course is a core course of the program ?P 

      • then there is a transcript record that attests that student ?Stu took course ?Course in semester ?Semester.

Pay attention to the suggested style of writing long rules that involve multiple subgoals in rule bodies, including the subgoals that involve quantifiers.

• • Example of the use of quantifiers in rule head: Every state has two senators.

forall(?St)^exist(?Sn1,?Sn2)^(senator(?St,{?Sn1,?Sn2}) <== state(?St)).

This body-less statement says that every state (?St) has two senators (?Sn1 and ?Sn2).  More technically, for every ?St there are ?Sn1, ?Sn2 such that if ?St is a state then both ?Sn1 and ?Sn2 are senators of that state.   Another way to express similar information is

exist(?Sn1,?Sn2)^(senator(?St,{?Sn1,?Sn2}))  :-  state(?St).

which has both a body and a head. Unlike in the first statement, here ?St is quantified implicitly  --  with a universal quantifier placed outside of the rule.  You can imagine the previous rule to mean to be something like this:

forall(?St)^( exist(?Sn1,?Sn2)^(senator(?St,{?Sn1,?Sn2}))  :-  state(?St) ).

but the bold part above is implicit -- the syntax of Ergo does not permit any kind of quantifiers to be applied to an entire rule that has an :- in them (quantifiers may appear only in the heads and bodies of rules).  Observe that in the first of the above three statements, forall is applied to the head of the rule (that rule has no body and thus no `:-').  The second rule above does have a :-, but the exist quantifier is  applied to the head only and so is permitted.

We will discuss the difference between the first two of the above rules in the next section.

Omniform Rules

Explicit quantification in rule heads, illustrated above, is one of the features that are collectively called omniformity. The other features under that rubric include disjunction (the \or-operator) and the ==>-style implication in rule heads. The previous subsection illustrates the importance of these features, especially for expressing natural language sentences in logic.  Omniformity is an advanced feature that requires a very good understanding of the meaning of such formulas, so omniform rules are not enabled by default: the user must request omniformity explicitly via the compiler directive

:- compiler_options{omni=on}.

see the ErgoAI Reasoner User's Manual for more details.

Omniformity implies one more important feature that makes Ergo rules behave a bit more like first-order rules: contrapositive assertions. To explain, recall that in first-order logic,

rains -> wet 

means not only that if it rains then it is wet, but also that if it is not wet then it does not rain:

¬wet -> ¬rains 

In contrast,

wet :- rains. 

does not imply the contrapositive, so given \neg wet one cannot derive \neg rains.   Similarly, in first-order logic, given

rains ∨ shines 

¬ rains 

one derives shines. In most logic programming languages one cannot even write something like this in rule heads or facts:

rains \or shines. 

Omniformity changes all that for the  connectives ==>, <==, and \or, but leaves the traditional interpretation for the :- connective (because it is fundamentally non-first order).  Namely, due to omniformity, the Ergo statement

rains ==> wet 

stands for the following pair or rules

wet :- rains. 

\neg rains :- \neg wet. 

Thus, given \neg wet, Ergo would derive  \neg rains.  Similarly,

rains \or shines. 

stands for

rains :- \neg shines. 

shines :- \neg rains. 

and, therefore, given  \neg rains,  Ergo would derive  shines.

Next, let us come back to the statements discussed in the previous sections. For

p(?X) <== q(?X,?Y), r(?Y). 

the Ergo interpretation includes all of its contrapositives:

p(?X) :- q(?X,?Y), r(?Y). 

\neg q(?X,?Y) :- r(?X), \neg p(?X). 

\neg r(?Y) :- q(?X,?Y), \neg p(?X). 

Important: omniformity applies only to rule heads.  So, if we had

(p(?X) <== q(?X,?Y), r(?Y)) :- body(?X,?Y). 

then the full enchilada, including the contrapositives, will consist of

p(?X) :- body(?X,?Y), q(?X,?Y), r(?Y).

\neg q(?X,?Y) :- body(?X,?Y), r(?X), \neg p(?X).

\neg r(?Y) :- body(?X,?Y), q(?X,?Y), \neg p(?X).

Now, let us discuss the difference between seemingly similar statements from the previous section:

forall(?St)^exist(?Sn1,?Sn2)^(senator(?St,{?Sn1,?Sn2}) <== state(?St)).

and

exist(?Sn1,?Sn2)^(senator(?St,{?Sn1,?Sn2}))  :-  state(?St).

The difference here is that the first rule uses <== and so is subject to "contrapositivisation" while the second statement is not. Both statements will undergo quantifier elimination as follows:

• The outermost forall in sentence 1 is eliminated, since universal quantification of the entire rule is implicit anyway, as observed earlier.

• In both cases, the existential variables ?Sn1 and ?Sn2 will be replaced by so called Skolem functions -- the functions with completely new names that don't occur elsewhere in the knowledge base. 

  • In both cases, these functions will depend only on the universally quantified variable ?St.

  • The replacement of ?Sn1 and ?Sn2 will occur only when the exist quantifier occurs in the head of a contrapositive derivative.

Without further ado, we spill the beans and reveal that the first rule above is translated into

senator(?St,{sen1(?St),sen2(?St)}) :- state(?St).

\neg state(?St) :- \neg exist(?Sn1,?Sn2)^(senator(?St,{?Sn1,?Sn2})).

In contrast, the second rule above will only undergo quantifier replacement, which will yield only this rule:

senator(?St,{sen1(?St),sen2(?St)}) :- state(?St).

Thus, the first form, which uses ==>, would imply that if something has no senators then this is not a state, while the second form won't support such a conclusion.