A rule is a sentex — same structure (sentence + context), different indexing. Its sentence is an implication:
(implies (and <antecedent> ...) <consequent>) ; single antecedent needs no and
Antecedents and consequent are sentence patterns that may contain variables. Rules are indexed by their antecedent/consequent predicates (see the index store) so forward chaining finds candidate rules without scanning, and — being ordinary sentexes — they get handles, TMS support, and retraction for free.
Rules must be range-restricted: every consequent variable appears in some
antecedent, so a fired consequent is ground. The one exemption is a head
existential — a consequent variable explicitly marked (exists ?y C), which
forward firing skolemizes to a deterministic constant (docs/skolem.md); range
restriction permits only the marked variable and still rejects any accidentally
unbound one. The same closure is required of an exceptWhen exception, which is a
query rather than a conclusion but must be ground for the same reason (checked at the
assert layer via sentex/check-exception-closed).
A rule *is* a sentex — same structure (sentence + context), different indexing. Its sentence is an implication: (implies (and <antecedent> ...) <consequent>) ; single antecedent needs no `and` Antecedents and consequent are sentence patterns that may contain variables. Rules are indexed by their antecedent/consequent predicates (see the index store) so forward chaining finds candidate rules without scanning, and — being ordinary sentexes — they get handles, TMS support, and retraction for free. Rules must be range-restricted: every consequent variable appears in some antecedent, so a fired consequent is ground. The one exemption is a **head existential** — a consequent variable explicitly marked `(exists ?y C)`, which forward firing skolemizes to a deterministic constant (docs/skolem.md); range restriction permits only the marked variable and still rejects any *accidentally* unbound one. The same closure is required of an `exceptWhen` exception, which is a query rather than a conclusion but must be ground for the same reason (checked at the assert layer via `sentex/check-exception-closed`).
(aggregate-antecedents sentex)The aggregate antecedent literals of a stored rule.
The aggregate antecedent literals of a stored rule.
(aggregate-antecedents-of rule-sentence)The aggregate antecedent literals of a raw rule sentence — for the checks that run before a rule is stored as a sentex (stratification).
The aggregate antecedent literals of a raw rule *sentence* — for the checks that run before a rule is stored as a sentex (stratification).
(aggregate-predicates sentex)The predicates a stored rule's aggregate bodies mention.
The predicates a stored rule's aggregate bodies mention.
(aggregate-predicates-of rule-sentence)The predicates a raw rule sentence's aggregate bodies mention — the negative-edge keys the stratification graph reads, and the re-check keys the index posts under.
The predicates a raw rule *sentence*'s aggregate bodies mention — the negative-edge keys the stratification graph reads, and the re-check keys the index posts under.
(aggregate-queries sentex)The body queries of a rule's aggregate antecedents, so the settle-time firing filter can shape them against a trigger exactly as it shapes an exception's conjuncts. Each mentions the reduction variable by construction, so none of them is ground and every one falls through to 'keep' — an aggregate's firings are never narrowed away, which is the safe direction.
The body queries of a rule's aggregate antecedents, so the settle-time firing filter can shape them against a trigger exactly as it shapes an exception's conjuncts. Each mentions the reduction variable by construction, so none of them is ground and every one falls through to 'keep' — an aggregate's firings are never narrowed away, which is the safe direction.
(antecedent-predicates sentence)(antecedents sentence)The antecedent patterns of a rule sentence (unwrapping a leading and).
The antecedent patterns of a rule sentence (unwrapping a leading `and`).
(assumption? sentex)Is this stored rule sentex a set/assumptionRule — a choice rule whose head a solve
decides rather than the chainer deriving? Read straight off the record's
:assumption field, like :defeasible (docs/solving.md).
Is this stored rule sentex a `set/assumptionRule` — a choice rule whose head a solve decides rather than the chainer deriving? Read straight off the record's `:assumption` field, like `:defeasible` (docs/solving.md).
(backward-sentex? sentex)Does this stored rule sentex backward-chain? An assumptionRule / constraint rule
does not (see forward-sentex?).
Does this stored rule sentex backward-chain? An `assumptionRule` / constraint rule does not (see `forward-sentex?`).
(backward? direction)(check-range-restricted antecedents consequent)Throw :type :not-range-restricted unless every consequent variable is bound by
some antecedent (and the consequent is a well-formed conclusion).
Uses ex-info, not clojure.core/assert: an elidable check under *assert* false
would store the junk rule silently — the exact failure check-ground exists to
prevent — and an AssertionError carries no :type for callers to discriminate
on.
Throw `:type :not-range-restricted` unless every consequent variable is bound by some antecedent (and the consequent is a well-formed conclusion). Uses `ex-info`, not `clojure.core/assert`: an elidable check under `*assert*` false would store the junk rule *silently* — the exact failure `check-ground` exists to prevent — and an `AssertionError` carries no `:type` for callers to discriminate on.
(consequent sentence)(consequent-predicate sentence)The predicate a rule concludes. A consequent of the form (ist Ctx S) (place S
into context Ctx) is indexed by S's predicate, not by ist.
The predicate a rule concludes. A consequent of the form `(ist Ctx S)` (place S into context Ctx) is indexed by S's predicate, not by ist.
(constraint-of sentex)The constraint class of this stored rule sentex — :hard / :soft from its
set/hardConstraint / set/softConstraint wrapper, or nil for an ordinary rule.
Read straight off the record's :constraint field (docs/solving.md).
The constraint class of this stored rule sentex — `:hard` / `:soft` from its `set/hardConstraint` / `set/softConstraint` wrapper, or nil for an ordinary rule. Read straight off the record's `:constraint` field (docs/solving.md).
(constraint? sentex)Is this stored rule sentex a set/hardConstraint / set/softConstraint — a
contradiction rule whose conjunctive body a solve grounds into a nogood?
Is this stored rule sentex a `set/hardConstraint` / `set/softConstraint` — a contradiction rule whose conjunctive body a solve grounds into a nogood?
(expand-consequent sentence)Polycanonicalize a rule that concludes a conjunction into one rule per conjunct,
preserving any virtual wrapper (default / forward / backward / inert / assumptionRule).
A rule (implies A (and C1 C2)) becomes [(implies A C1) (implies A C2)]; anything
else (a non-rule, or a rule with a single consequent) returns [sentence] unchanged.
Runs on a rule whose exceptWhen has already been split off (split-exceptWhen), so
the exception is re-attached once per conjunct by the caller, against each conjunct's
own handle.
Polycanonicalize a rule that concludes a conjunction into one rule per conjunct, preserving any virtual wrapper (default / forward / backward / inert / assumptionRule). A rule `(implies A (and C1 C2))` becomes `[(implies A C1) (implies A C2)]`; anything else (a non-rule, or a rule with a single consequent) returns `[sentence]` unchanged. Runs on a rule whose exceptWhen has already been split off (`split-exceptWhen`), so the exception is re-attached once per conjunct by the caller, against each conjunct's own handle.
(forward-sentex? sentex)Does this stored rule sentex forward-chain? Read off the record, which carries
the direction its set/*Rule wrapper set. An assumptionRule (a choice head) and a
hard/softConstraint (a contradiction marker) never chain — their heads are decided
or forbidden by a solve, not derived — so they are inference-inert in both directions
regardless of the direction they were written with.
Does this stored rule sentex forward-chain? Read off the record, which carries the direction its `set/*Rule` wrapper set. An `assumptionRule` (a choice head) and a `hard`/`softConstraint` (a contradiction marker) never chain — their heads are decided or forbidden by a solve, not derived — so they are inference-inert in both directions regardless of the direction they were written with.
(forward? direction)(has-aggregate? sentex)Does this rule carry any aggregate antecedent?
Does this rule carry any aggregate antecedent?
(has-naf? sentex)Does this rule carry any unknown antecedent?
Does this rule carry any `unknown` antecedent?
(inner-rule sentence)The bare (implies …) inside any virtual rule wrappers (set/*Rule and
exceptWhen, which may nest in any order — a defeasible forward rule with an
exception). The direction / default / assumption wrappers become record fields and
the exceptWhen becomes a meta-sentex, so the checks and the stored sentence both work
on this.
The bare `(implies …)` inside any virtual rule wrappers (`set/*Rule` and `exceptWhen`, which may nest in any order — a defeasible forward rule with an exception). The direction / default / assumption wrappers become record fields and the exceptWhen becomes a meta-sentex, so the checks and the stored sentence both work on this.
(naf-antecedents sentex)The (unknown S) antecedent literals of a stored rule — its negation-as-failure
conditions.
The `(unknown S)` antecedent literals of a stored rule — its negation-as-failure conditions.
(naf-antecedents-of rule-sentence)The (unknown S) antecedent literals of a raw rule sentence — for the checks
that run before a rule is stored as a sentex (stratification).
The `(unknown S)` antecedent literals of a raw rule *sentence* — for the checks that run before a rule is stored as a sentex (stratification).
(naf-predicates sentex)The predicates a rule's unknown antecedents mention — the keys the re-check index
posts the rule under, so a fact arriving or leaving on one re-evaluates the NAF
condition. The exception analogue is exception-predicates; both feed the same
[:exception-index …] index.
The predicates a rule's `unknown` antecedents mention — the keys the re-check index posts the rule under, so a fact arriving or leaving on one re-evaluates the NAF condition. The exception analogue is `exception-predicates`; both feed the same `[:exception-index …]` index.
(naf-predicates-of rule-sentence)The predicates a raw rule sentence's unknown antecedents mention — for the
stratification check on a rule not yet stored (the mirror of the exception's
negative dependence).
The predicates a raw rule *sentence*'s `unknown` antecedents mention — for the stratification check on a rule not yet stored (the mirror of the exception's negative dependence).
(naf-queries sentex)The inner query literals of a rule's unknown antecedents (each unwrapped past a
thereExists), so the settle-time firing filter can shape them against a trigger
exactly as it shapes an exception's conjuncts — the ground ones narrow, the
existential ones fall through to 'keep' like any non-flat conjunct.
The inner query literals of a rule's `unknown` antecedents (each unwrapped past a `thereExists`), so the settle-time firing filter can shape them against a trigger exactly as it shapes an exception's conjuncts — the ground ones narrow, the existential ones fall through to 'keep' like any non-flat conjunct.
(parse sentence)(post-join-antecedents sentex)post-join-literals over a stored rule's antecedents.
`post-join-literals` over a stored rule's antecedents.
(post-join-literals antes)The antecedent literals evaluated after the join: every aggregate, plus every
deferred literal reading a variable an aggregate produces — or that one of those
produces in turn, so an (evaluate ?d (+ ?n 1)) carries a later (lessThan ?d 9)
along with it.
In written order, which is the order they run in, because a computed literal
reads what is written before it. That is not a rule aggregates introduce: an
evaluate chain has always had to be written downhill, since canonical order holds a
deferred literal in the author's position and every chainer runs it there. Making an
aggregate an exception — reordering the phase so a comparison could be written above
its own count — is what a forward chainer could do and a backward one could not, so
it would buy convenience at the price of the two disagreeing about one rule.
sentex/check-naf-closed refuses the uphill writing instead.
unknown is deliberately not here: it binds nothing, so it never needs the ordering,
and it is already evaluated per placement as :naf.
Asked on every join, so the gate is a short-circuiting some that allocates
nothing: no aggregate, no post-join phase, and the overwhelming majority of rules
have none.
The antecedent literals evaluated **after** the join: every aggregate, plus every deferred literal reading a variable an aggregate produces — or that one of *those* produces in turn, so an `(evaluate ?d (+ ?n 1))` carries a later `(lessThan ?d 9)` along with it. **In written order**, which is the order they run in, because a computed literal reads what is written before it. That is not a rule aggregates introduce: an `evaluate` chain has always had to be written downhill, since canonical order holds a deferred literal in the author's position and every chainer runs it there. Making an aggregate an exception — reordering the phase so a comparison could be written above its own count — is what a *forward* chainer could do and a backward one could not, so it would buy convenience at the price of the two disagreeing about one rule. `sentex/check-naf-closed` refuses the uphill writing instead. `unknown` is deliberately not here: it binds nothing, so it never needs the ordering, and it is already evaluated per placement as `:naf`. Asked on **every** join, so the gate is a short-circuiting `some` that allocates nothing: no aggregate, no post-join phase, and the overwhelming majority of rules have none.
(range-problems antecedents consequent)Why antecedents => consequent is not range-restricted, as a seq of problem
strings — empty when the rule is fine. The value form, like the wff arms:
a caller that refuses wraps it in a throw, and a fixpoint that must not abort
can record it instead.
A head existential (exists ?y C) exempts only its marked variable(s): the
check runs over the inner C, and every consequent variable that is neither
antecedent-bound nor existentially marked is still a problem — so an accidental
typo is caught while a deliberate ∃ is allowed (docs/skolem.md).
Why `antecedents => consequent` is not range-restricted, as a seq of problem strings — empty when the rule is fine. The value form, like the wff arms: a caller that refuses wraps it in a throw, and a fixpoint that must not abort can record it instead. A head existential `(exists ?y C)` exempts **only** its marked variable(s): the check runs over the inner `C`, and every consequent variable that is neither antecedent-bound nor existentially marked is still a problem — so an accidental typo is caught while a deliberate `∃` is allowed (docs/skolem.md).
(recheck-predicates sentex)The predicates whose change must re-check this rule for its own re-check
conditions — the predicates its unknown antecedents and its aggregate bodies
mention. (An exceptWhen exception is a separate meta-sentex, registered under its
rule by the meta-sentex's own indexing; it is not read off the rule.) The key set
the [:exception-index …] index posts a rule under when it is indexed.
The two kinds are one key set because they are one problem: both read what the KB believes at firing time rather than a fact the justification names, so both need a fact arriving on those predicates to bring the firing back for re-decision.
The predicates whose change must re-check this rule for its **own** re-check conditions — the predicates its `unknown` antecedents and its **aggregate** bodies mention. (An exceptWhen exception is a separate meta-sentex, registered under its rule by the meta-sentex's own indexing; it is not read off the rule.) The key set the `[:exception-index …]` index posts a rule under when it is indexed. The two kinds are one key set because they are one problem: both read what the KB believes at firing time rather than a fact the justification names, so both need a fact arriving on those predicates to bring the firing back for re-decision.
(rechecked? sentex)Does this rule carry a re-check condition of its own — an unknown antecedent
or an aggregate? The gate on registering it in the re-check index; an exceptWhen
exception is registered by its own meta-sentex and is not read off the rule.
Does this rule carry a re-check condition of its **own** — an `unknown` antecedent or an aggregate? The gate on registering it in the re-check index; an exceptWhen exception is registered by its own meta-sentex and is not read off the rule.
(rewrap sentence direction defeasible assumption constraint)Put the direction / default / assumption / constraint wrappers a rule was written
with back around sentence — the inverse of sx/peel-rule-wrapper, since the
wrappers ride the record, not the stored sentence. Two callers: a polycanonicalized
conjunct keeps the mode of the rule it came from, and an equality merge's migrated
rule twin keeps the mode of the rule it restates (special/migrate-sentex). An
exceptWhen is not among them — it is split off before this runs and stored as a
meta-sentex against each conjunct's handle (split-exceptWhen).
Put the direction / default / assumption / constraint wrappers a rule was written with back around `sentence` — the inverse of `sx/peel-rule-wrapper`, since the wrappers ride the record, not the stored sentence. Two callers: a polycanonicalized conjunct keeps the mode of the rule it came from, and an equality merge's migrated rule twin keeps the mode of the rule it restates (`special/migrate-sentex`). An exceptWhen is not among them — it is split off before this runs and stored as a meta-sentex against each conjunct's handle (`split-exceptWhen`).
(rule-sentence antecedents consequent)Build a rule sentence from antecedent patterns and a consequent pattern.
One spelling for the whole codebase — see sentex/rule-sentence.
Build a rule sentence from antecedent patterns and a consequent pattern. One spelling for the whole codebase — see `sentex/rule-sentence`.
(rule-sentence? sentence)Is sentence a rule form (implies <ante> <conseq>)?
Is `sentence` a rule form `(implies <ante> <conseq>)`?
(rule? sentex)(split-exceptWhen sentence)Split an (exceptWhen <query> <rule>) assertion into [exception inner].
exception is the flattened conjunction of every exceptWhen wrapper (a vector of
literals in the author's variable names, block-if-all-hold), and inner is what the
exceptWhen qualifies: the wrapped rule with its exceptWhen(s) stripped but its
direction / default / assumption wrappers intact, or the (sentexHandle H) a
bare-handle exceptWhen named. [nil sentence] when there is no exceptWhen.
This is the layer at which an exceptWhen becomes a separate meta-sentex: the assert
layer stores inner as the rule (or resolves the handle) and the exception as
(exceptWhen <aligned-query> (sentexHandle H)) against it.
Split an `(exceptWhen <query> <rule>)` assertion into `[exception inner]`. `exception` is the flattened conjunction of every exceptWhen wrapper (a vector of literals in the author's variable names, block-if-all-hold), and `inner` is what the exceptWhen qualifies: the wrapped rule with its exceptWhen(s) stripped but its direction / default / assumption wrappers intact, or the `(sentexHandle H)` a bare-handle exceptWhen named. `[nil sentence]` when there is no exceptWhen. This is the layer at which an exceptWhen becomes a separate meta-sentex: the assert layer stores `inner` as the rule (or resolves the handle) and the exception as `(exceptWhen <aligned-query> (sentexHandle H))` against it.
(wrap-direction sentence direction)Express direction as the corresponding set/*Rule wrapper around sentence.
:both needs no wrapper — a bare (implies …) already works both ways.
Express `direction` as the corresponding `set/*Rule` wrapper around `sentence`. `:both` needs no wrapper — a bare `(implies …)` already works both ways.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |