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)
q(a)
q(b)
t(a)

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

p(a)
p(b)

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

r(a)

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 :- L_{1}...L_{m}, N_{1}...N_{p}

where L_{1}...L_{m} are positive literals and N_{1}...N_{p} 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`

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.

Consider:

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:

- free, i.e. it is a variable and is represented with '?'
- a constant, which is represented by the constant value itself
- not a specific constant, which is indicated by '!' followed by the constant value

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

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

p^{a,?}(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:

- can not produce tuples to feed the negated sub-goal, i.e. no match
- can only produce tuples that feed the negated sub-goal, i.e. an exact match
- 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 `N`

,
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.
_{1}...N_{p})

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 `N`

.
For each in-equality literal added, the adornment for this position in the rule head is updated
by adding '!'_{1}...N_{p})

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:

q^{b,?}(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:

p^{a,?}(a,X) :- r(X), not q(b,X) (11)
q^{b,?}(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:

p^{a,?}(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:

p^{a,?}(a,X) :- q(X), not p(b,X) (16)
p^{b,?}(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:

p^{a,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:

p^{a,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)
p^{c,!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

- Move as many constants as possible in to rule heads.
- Adorn rule heads
- Follow every negated sub-goal containing constants and split any matching rules in to those that can 'feed' the negated sub-goal and those that can not
- When no more modifications to rules can be made, attempt the normal stratification process, but take adornments as well as predicate names in to account when detecting dependencies.

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