Stratification (logic)

In mathematical logic, stratification denotes an order of predicate symbols that guarantees that a clear formal interpretation of a logic program exists. In particular, a set of clauses of the form is called stratifiable if and only if there is a mapping S from the set of predicates into the natural numbers that satisfies the following conditions: ${\displaystyle Q_{1}\wedge \dots \wedge Q_{n}\wedge \neg Q_{n+1}\wedge \dots \wedge \neg Q_{n+m}\rightarrow P}$

(A) If a predicate is positively dependent on a predicate , i.e. if a rule occurs in the head in which positive occurs in the body, then it must have a greater or the same stratification number as , i.e. ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle S(P)\geq S(Q)}$

(B) If a predicate depends on a negated predicate, i.e. occurs in the head of a rule in which negative occurs in the body, then the stratification number of real must be greater than that of , i.e. ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle S(P)>S(Q)}$

Horn clauses are always stratifiable, since they do not allow negative literals in the fields of clauses and therefore only condition (A) has to be fulfilled, which is achieved by the trivial mapping that assigns the same natural number to all predicate symbols. ${\displaystyle S}$

The following prologue program is given as an example :

p(X) :- q(X).
q(X) :- not(r(X)), s(X,Z).

${\displaystyle S=\{p\mapsto 2,q\mapsto 2,r\mapsto 1,s\mapsto 1\}}$ is a possible stratification of this program.