Editing Stratification (mathematics) (section)

==In mathematical logic==

In [[mathematical logic]], '''stratification''' is any consistent assignment of numbers to [[Predicate (logic)|predicate]] symbols guaranteeing that a unique formal [[Interpretation (logic)|interpretation]] of a logical theory exists. Specifically, we say that a set of [[Clause (logic)|clauses]] of the form <math>Q_1 \wedge \dots \wedge Q_n \wedge \neg Q_{n+1} \wedge \dots \wedge \neg Q_{n+m} \rightarrow P</math> is stratified if and only if
there is a stratification assignment S that fulfills the following conditions:

# If a predicate P is positively derived from a predicate Q (i.e., P is the head of a rule, and Q occurs positively in the body of the same rule), then the stratification number of P must be greater than or equal to the stratification number of Q, in short <math>S(P) \geq S(Q)</math>.
# If a predicate P is derived from a negated predicate Q (i.e., P is the head of a rule, and Q occurs negatively in the body of the same rule), then the stratification number of P must be greater than the stratification number of Q, in short <math>S(P) > S(Q)</math>.

The notion of stratified negation leads to a very effective operational semantics for stratified programs in terms of the stratified least fixpoint, that is obtained by iteratively applying the fixpoint operator to each ''stratum'' of the program, from the lowest one up.
Stratification is not only useful for guaranteeing unique interpretation of [[Horn clause]]
theories.