Monotonicity
Consider a rule containing an atom referencing a predicate p:
r(X, Y, Z) :- ..., p(X, Y), ...We call the rule monotone in p if a larger p gives us a larger r.
A program is monotone if all recursive rules are monotone in all recursive predicates.
Knaster-Tarski Theorem: Each monotone program has a least fixed point.
Kleene Fixed-Point Theorem: For monotone programs in pure Datalog, naive evaluation terminates with the least fixed point.