search

totalperspective / oolon

Bloom implementation for Clojure/ClojureScript leaning on Datomic datalog
https://github.com/totalperspective/oolon
Eclipse Public License 1.0
10 stars 0 forks source link

Stratification #29

Closed bahulneel closed 8 years ago

bahulneel commented 8 years ago

In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists. Specifically, we say that a set of clauses of the form Q1 /\ ... /\ Qn /\ ¬Qn+1 /\ ... /\ ¬Qn+m -> P is stratified if and only if there is a stratification assignment S that fulfills the following conditions:

  1. 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 S(P) >= S(Q).
  2. 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 S(P) > S(Q).

Stratification

bahulneel commented 8 years ago

This also applies to non-monotonic rules as in https://github.com/bloom-lang/bud/blob/master/docs/operational.md#non-monotonicity-and-strata

The goal is to postpone evaluating non-monotonic operators until fixpoint is reached on their input collections.