The algorithms for stratifying the rules of a logic program are implemented in discrete classes that implement the IRuleStratifier interface.

If an attempt is made to evaluate a logic program that can not be stratified then a ProgramNotStratifiedException is thrown.


We describe the following construct:

    p(X) :- q(X), not r(X)

as meaning, that the relation associated with predicate 'p' contains all those values from predicate 'q' that are not in predicate 'r'. In other words, the set difference of 'q' and 'r'.

Traditional forward chaining methods for evaluating logic programs involve simply using the values of tuples from predicates and applying them to the program's rules to generate more tuples.

Without negation such techniques are guaranteed to be monotone. However, in the presence of negation, rules that generate tuples for a predicate that is used in negated sub-goals of other rules, must be 'fully' evaluated before evaluation of the dependent rules begins.

Consider what would happen if we have the following:

    p(X) :- q(X), not r(X)	(1)
    r(X) :- t(X)	        (2)

If the known facts are applied to rule (1) first, the following new facts are generated:


Then applying the known facts to rule (2) produces the following:


However, the existence of fact r(a) should have precluded the deduction of fact p(a) in rule (1).

In order to ensure that rule evaluation is monotone, rules must be evaluated in a specific order.

For any general rule:

    p :- L1...Lm, N1...Np

where L1...Lm are positive literals and N1...Np are negative literals, monotone evaluation using forward chaining techniques can only be assured if the rule 'p' be allocated to a stratum that is at least as high as each of its positive literals and at least one higher than each of its negative literals.

Such a scheme would therefore require that rule (2) above is evaluated before rule(1).

However, this approach precludes the evaluation of any logic program containing a rule that has a negative dependency upon itself.

When all the rules in a knowledge base can be allocated to strata with no inconsistencies, the knowledge base is said to be stratified.

This (global) stratification algorithm can be found in class: org.deri.iris.rules.stratification.GlobalStratifier

Local Stratification

There are genuine reasoning activities that can lead to the creation of logic programs containing rules that do contain a negative dependency to themselves, but can still be evaluated in a meaningful way, because of the presence of constants in the rules that separate the domains of tuples used as input to the rule and tuples produced by the rule.


    p(a,X) :- q(X), not p(b,X)	(3)

This rule can produce tuples (a,?) for the relation associated with predicate 'p' from tuples (b,?) also associated with the relation for 'p'. However, no special treatment is required, because nothing produced by the rule can be used as input to the rule, because of the presence of constants 'a' and 'b'.

A more complicated scenario is as follows:

    p(a,X) :- r(X), not q(b,X)	(4)
    q(X,Y) :- p(X,Y)	        (5)

Here rule (5) can produce tuples for input to rule (4) and vice versa.

The technique used by IRIS to evaluate such logic programs involves adorning the rule heads with information that indicates what can and what can not be produced by the application of the rule.

The first step is to move as many constant values as possible in to the head with variable-variable and constant-variable substitutions, so as to indicate in as restrictive a manner as possible the extent of the domain over which the rule can produce new facts.

The following rule:

    p(Z,X) :- r(X), not q(b,X), Z=a,	(6)

would be re-written as:

    p(a,X) :- r(X), not q(b,X)	        (7)

being equivalent to (4) above. It is now clear that this rule can only produce tuples for predicate 'p' that have the constant value 'a' as their first term.

The second step is to adorn all the rule head predicates to show their 'domain of influence'. For each head predicate an adornment is added for each term that indicates if the term is either:

The significance of the third adornment type will be shown later.

The rules (4) and (5) above would thus be written:

    pa,?(a,X) :- r(X), not q(b,X)	(7)
    q?,?(X,Y) :- p(X,Y)	            (8)

Step 3 now involves iterating through the body literals of every rule. Whenever a negated literal is found that contains constant terms, a search is made for evry rule that can produce tuples that can fit this literal.

Rules that can feed a particular negated sub-goal are analysed to ascertain whether they:

  1. can not produce tuples to feed the negated sub-goal, i.e. no match
  2. can only produce tuples that feed the negated sub-goal, i.e. an exact match
  3. can produce tuples that might feed the negated sub-goal, i.e. superset

In cases 1. and 2. above, no work needs be done, because in case 1. there is no dependency and in case 2. there is an exact dependency which can not be further decomposed.

However, for those rules in 3. above, the rule can be split in to two separate rules, one which is an exact match and one that does not match for the interesting negated sub-goal.

For a given negated sub-goal N1...Np), the 'perfect match' rule is created by taking a copy of the rule and replacing the variables in the head with the constants from the negated sub-goal and so on in to the rule body. Then the rule adornments are updated with the constant values from each position in the rule head.

To create the non-matching rule, in-equality literals are added to the rule body, one for each variable-constant pair, where the variables are from the rule head and the constants from N1...Np). For each in-equality literal added, the adornment for this position in the rule head is updated by adding '!'.

Following our example, the 'not q(b,X)' literal from (7) would therefore match with the head of rule (8).

However, the literal 'not q(b,X)' contains a constant, which enables the re-writing of rule (8) in to two separate rules: One that can produce tuples for 'not q(b,X)' and one that can not:

    qb,?(b,Y) :- p(b,Y)	            (9)
    q!b,?(X,Y) :- p(X,Y), X != b	    (10)

This process is repeated until no more rules can be found to 'split'. From our example, the resulting set of rules looks like this:

    pa,?(a,X) :- r(X), not q(b,X)	(11)
    qb,?(b,Y) :- p(b,Y)	            (12)
    q!b,?(X,Y) :- p(X,Y), X != b	    (13)

The standard stratification algorithm can now be applied, except that head predicate adornments as well as their names are now taken in to consideration.

From the above, it can be seen that negated literal 'not q(b,X)' from rule (11) can not have a dependency on rule (13) with head predicate 'q!b,?(X,Y)', since no tuples are generated from rule (13) with constant value 'b' in the first term.

However, the negated literal 'not q(b,X)' from rule (11) does have a dependency on rule (12) that only produces tuples with the constant value 'b' in the first term.

By inspection then, it can be seen that the order of evaluation of this logic program is as follows:

stratum 0: rule 12
stratum 1: rules 11 and 13

Once the stratum have been decided, the adornments can be removed and evaluation can progress as normal:

Stratum 0:
    q(b,Y) :- p(b,Y)
Stratum 1:
    p(a,X) :- r(X), not q(b,X)
    q(X,Y) :- p(X,Y), X != b

Consider the trivial program containing the single rule (3) above. The algorithm would cause this rule to be re-written as follows:

    pa,?(a,X) :- q(X), not p(b,X)	(14)

The negated sub-goal 'not p(b,X)' has no dependency on head predicate 'pa,?(a,X)', so no cyclic dependency exists.

The situation is more interesting with the addition of a second rule:

    p(X,Y) :- p(Y,X)	                        (15)

Following the negated sub-goal from (14) would lead us to re-write rule (15) to give the complete set of rules as:

    pa,?(a,X) :- q(X), not p(b,X)	(16)
    pb,?(b,Y) :- p(Y,b)	            (17)
    p!b,?(X,Y) :- p(Y,X), X != b	    (18)

The negated sub-goal 'not p(b,X)' from rule (16) requires that rule (16) exist in a higher stratum than (17), with no direct dependency on rule (18).

However, the literal 'p(Y,b)' from rule (17) matches with the head literal of every other rule, requiring that rule (17) exist in at least as high a stratum as the other two rules.

This program can not therefore be stratified.

More complicated cases can arise where a rule is split more than once, either on different terms or on the same term.

    p?,?,?(X,Y,Z) :- q(X,Y,Z)

could be split like this:

    pa,b,?(a,b,Z) :- q(a,b,Z)
    p!a,!b,?(X,Y,Z) :- q(X,Y,Z), X != a, Y != b

and then further like this:

    pa,b,?(a,b,Z) :- q(a,b,Z)	                            (19)
    p!a!c,!b,?(X,Y,Z) :- q(X,Y,Z), X != a, X != c, Y != b	(20)
    pc,!b,?(X,Y,Z) :- q(X,Y,Z), X =c, Y != b	                (21)

Here the adornments for rule (20) indicate that it produces tuple for predicate 'p', where the first term is neither 'a' nor 'c', the second term is not 'b' and the third term is not determined.

Summary of Algorithm

The local stratification algorithm can be found in class: org.deri.iris.rules.stratification.LocalStratifier