Forward chaining: the semi-naive fixpoint, one agenda for bare and defeasible
rules alike, with the definitional checks re-run on the derivation path and the
exceptWhen guard consulted before a conclusion is placed.
Fifth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): a firing joins antecedents against stored facts (kb), checks its
conclusion (checks), and reflects what it places into the caches through the
derivation-path choke point (special). Belief settling happens after a run,
in vaelii.impl.settle — nothing here defeats or arbitrates.
Forward chaining: the semi-naive fixpoint, one agenda for bare and defeasible rules alike, with the definitional checks re-run on the derivation path and the `exceptWhen` guard consulted before a conclusion is placed. Fifth layer of the engine stack (kb <- checks <- special <- integrate <- chain <- settle): a firing joins antecedents against stored facts (kb), checks its conclusion (checks), and reflects what it places into the caches through the derivation-path choke point (special). Belief settling happens *after* a run, in `vaelii.impl.settle` — nothing here defeats or arbitrates.
A mutable {handle -> arrival} map — the position at which each datum joined this
run's agenda — or nil, and then nothing is suppressed.
This decides work, not belief. A rule a(x,y) <- b1(x,z), b2(z,y) is triggered
by its b1 datum at position 0 and by its b2 datum at position 1, and both
enumerate the same pair: the second runs the whole join, rebuilds the same
conclusion, resolves the same placement contexts, and is thrown away by
jtms/has-justification?. Ordering the agenda's datums lets one of the two skip the
work — the firing that survives is identical whichever side makes it (same
bindings, same antecedent set, same justification), so the derived set and its
supports are unchanged by construction. The rule is a participant as well: a
seeded run puts the rule's own datum on the agenda beside its facts, and its full join
would enumerate every firing again, so its arrival is compared too
(rule-arrival-admit, and the skip in fire-rules-for). Nothing here is read when
belief is computed, and no tie-break anywhere keys on it: the engine's rule that belief never
tie-breaks on a handle is untouched, because this is not consulted about belief.
Arrival order, not handle order, and the difference is the whole correctness
argument. For a datum the run itself derives the two agree — handles are allocated
in creation order and a new conclusion is enqueued as it is placed — but a datum put
back on the agenda has an old handle and a fresh arrival: a fact revived from OUT,
a fact newly matchable under a derived genl edge (special/subsumption-seeds), a
seed list in whatever order jtms/in-datums produced. Keyed on arrival, such a
datum sorts after the partner that was already processed, so it is the one that
enumerates the pair, and the pair is enumerated. Keyed on the handle it would sort
before it and the pair would be lost.
A handle the run never enqueued has no arrival and is never suppressed against:
nothing else will enumerate its combinations, so they are all made here. That covers
a sentex some other write placed while the run was going — a migrated twin the caller
has not seeded yet — and every join run outside a chaining run at all. A
disbelieved trigger declines the filter outright, for the reason arrival-admit
states.
Bound by chain for the length of a run, like the handle cache and the dedup index,
and it is the agenda that bounds its size. A java.util.HashMap rather than an atom
because the engine is single-writer and this is read once per candidate the join
yields.
A mutable `{handle -> arrival}` map — the position at which each datum joined this
run's agenda — or nil, and then nothing is suppressed.
**This decides work, not belief.** A rule `a(x,y) <- b1(x,z), b2(z,y)` is triggered
by its `b1` datum at position 0 and by its `b2` datum at position 1, and both
enumerate the same pair: the second runs the whole join, rebuilds the same
conclusion, resolves the same placement contexts, and is thrown away by
`jtms/has-justification?`. Ordering the agenda's datums lets one of the two skip the
work — the firing that survives is *identical* whichever side makes it (same
bindings, same antecedent set, same justification), so the derived set and its
supports are unchanged by construction. The **rule** is a participant as well: a
seeded run puts the rule's own datum on the agenda beside its facts, and its full join
would enumerate every firing again, so its arrival is compared too
(`rule-arrival-admit`, and the skip in `fire-rules-for`). Nothing here is read when
belief is computed, and no tie-break anywhere keys on it: the engine's rule that belief never
tie-breaks on a handle is untouched, because this is not consulted about belief.
**Arrival order, not handle order**, and the difference is the whole correctness
argument. For a datum the run itself derives the two agree — handles are allocated
in creation order and a new conclusion is enqueued as it is placed — but a datum put
**back** on the agenda has an old handle and a fresh arrival: a fact revived from OUT,
a fact newly matchable under a derived `genl` edge (`special/subsumption-seeds`), a
seed list in whatever order `jtms/in-datums` produced. Keyed on arrival, such a
datum sorts *after* the partner that was already processed, so it is the one that
enumerates the pair, and the pair is enumerated. Keyed on the handle it would sort
before it and the pair would be lost.
A handle the run never enqueued has **no** arrival and is never suppressed against:
nothing else will enumerate its combinations, so they are all made here. That covers
a sentex some other write placed while the run was going — a migrated twin the caller
has not seeded yet — and every join run outside a chaining run at all. A
**disbelieved** trigger declines the filter outright, for the reason `arrival-admit`
states.
Bound by `chain` for the length of a run, like the handle cache and the dedup index,
and it is the agenda that bounds its size. A `java.util.HashMap` rather than an atom
because the engine is single-writer and this is read once per candidate the join
yields.Per-run record of the closure re-joins fire-rules-for has run, as a
java.util.HashMap from rule handle to the special/taxonomy-generations stamp its
full join read; nil outside a chaining run, where every closure edge re-joins in full.
A rule whose stamp has not moved fires at the datum's trigger position instead
(docs/inference.md, "An edge moving re-joins the rule").
Per-run record of the closure re-joins `fire-rules-for` has run, as a `java.util.HashMap` from rule handle to the `special/taxonomy-generations` stamp its full join read; nil outside a chaining run, where every closure edge re-joins in full. A rule whose stamp has not moved fires at the datum's trigger position instead (docs/inference.md, "An edge moving re-joins the rule").
Per-run cache of inherit/declarations-exist? — whether the KB declares any
preservation at all — as a volatile holding the answer, or nil (unknown, read on the
next ask); the var itself is nil outside a chaining run, where the gate reads the
index.
preserving-antecedent? is asked of every non-trigger antecedent of every firing
attempt, and its first question is this one: two cardinality reads that answer false
for nearly every KB there is. It is the only reader that caches it:
inherit/rejoin-rules asks it live, each call.
Bound once by chain, like *evaluatable-preds*, and unlike it invalidated from
inside the run: a run can derive a declaration, and every join after that placement
must see it — the re-join the placing datum queues (inherit/rejoin-rules) and a
datum arriving later both match antecedents through preserving-antecedent?.
derive-conclusion resets the cache when a placed conclusion roots at a
declaration functor (placed-functor, since the conclusion the join hands over may
still be wearing a not), so the next ask pays the two reads once more and caches
the true. A declaration leaves only outside a run (retract!), so a cached true
never goes stale inside one.
Per-run cache of `inherit/declarations-exist?` — whether the KB declares any preservation at all — as a volatile holding the answer, or nil (unknown, read on the next ask); the var itself is nil outside a chaining run, where the gate reads the index. `preserving-antecedent?` is asked of every non-trigger antecedent of every firing attempt, and its first question is this one: two cardinality reads that answer false for nearly every KB there is. It is the only reader that caches it: `inherit/rejoin-rules` asks it live, each call. Bound once by `chain`, like `*evaluatable-preds*`, and unlike it **invalidated** from inside the run: a run can *derive* a declaration, and every join after that placement must see it — the re-join the placing datum queues (`inherit/rejoin-rules`) and a datum arriving later both match antecedents through `preserving-antecedent?`. `derive-conclusion` resets the cache when a placed conclusion **roots** at a declaration functor (`placed-functor`, since the conclusion the join hands over may still be wearing a `not`), so the next ask pays the two reads once more and caches the true. A declaration leaves only outside a run (`retract!`), so a cached true never goes stale inside one.
Per-run cache of the KB's add-evaluatable predicate functors
(provers/evaluatable-preds) — the ones forward chaining computes through the prover
registry instead of looking up as stored facts, exactly as it does the built-in
sentex/deferred-predicates. Bound once per run by chain, since the registry is
fixed for the run and rebuilding the set per antecedent would allocate on the hot join
path. Nil outside a run — the solve-rule why-not reaches through, say — where
deferred-antecedent? reads the registry directly. Empty for the common KB with no
registered evaluatables.
Per-run cache of the KB's `add-evaluatable` predicate functors (`provers/evaluatable-preds`) — the ones forward chaining computes through the prover registry instead of looking up as stored facts, exactly as it does the built-in `sentex/deferred-predicates`. Bound once per run by `chain`, since the registry is fixed for the run and rebuilding the set per antecedent would allocate on the hot join path. Nil outside a run — the `solve-rule` `why-not` reaches through, say — where `deferred-antecedent?` reads the registry directly. Empty for the common KB with no registered evaluatables.
How the forward join looks up the stored facts satisfying a non-trigger
antecedent — (fn [kb pattern context] -> seq of [handle bindings …]), returning
exactly what res/match-pattern does.
The default is res/match-pattern (the count-aware trie), which is the reference
path and leaves forward chaining unchanged. vaelii.impl.rete binds this to a RAM
alpha-memory matcher that answers the same set through an index on argument values,
so a non-trigger antecedent with a leading variable — (parentOf ?x Pi) — is a
hash lookup rather than a full functor scan. The set it returns is identical
(proven by the rete oracle), so every downstream behaviour is the reference's; only
the candidate lookup changes. This is the sole extension point the incremental matcher needs,
because the trigger match (match1) is already selective and everything else —
placement, exceptions, the definitional checks, justification dedup — is reused
verbatim. See docs/inference.md, "Incremental rule matching".
With the reference bound, a substituted antecedent that has a bound indexable
argument and a functor with sub-predicates is read through
res/matches-hierarchical instead (join-matches) — the same set by an argument
lead rather than a trie walk per sub-predicate. Binding this var to anything else
switches that off, so the extension point's caller sees every non-trigger antecedent.
How the forward join looks up the stored facts satisfying a **non-trigger** antecedent — `(fn [kb pattern context] -> seq of [handle bindings …])`, returning exactly what `res/match-pattern` does. The default is `res/match-pattern` (the count-aware trie), which is the reference path and leaves forward chaining unchanged. `vaelii.impl.rete` binds this to a RAM alpha-memory matcher that answers the same set through an index on argument values, so a non-trigger antecedent with a leading variable — `(parentOf ?x Pi)` — is a hash lookup rather than a full functor scan. The *set* it returns is identical (proven by the rete oracle), so every downstream behaviour is the reference's; only the candidate lookup changes. This is the sole extension point the incremental matcher needs, because the trigger match (`match1`) is already selective and everything else — placement, exceptions, the definitional checks, justification dedup — is reused verbatim. See docs/inference.md, "Incremental rule matching". With the reference bound, a substituted antecedent that has a bound indexable argument **and a functor with sub-predicates** is read through `res/matches-hierarchical` instead (`join-matches`) — the same set by an argument lead rather than a trie walk per sub-predicate. Binding this var to anything else switches that off, so the extension point's caller sees every non-trigger antecedent.
Per-run cache of {calculus-name -> #{context}} — the readers of a calculus, which
are the networks an entailed antecedent is solved against.
Collecting them walks the calculus's own extent, the same order as reading one
network, and where its facts span contexts a genlCx closure besides, so it
is cached for the length of a chaining run rather than recomputed per antecedent per
binding. Bound by chain; nil outside one, where it simply recomputes.
Per-run cache of `{calculus-name -> #{context}}` — the readers of a calculus, which
are the networks an entailed antecedent is solved against.
Collecting them walks the calculus's own extent, the same order as reading one
network, and where its facts span contexts a `genlCx` closure besides, so it
is cached for the length of a chaining run rather than recomputed per antecedent per
binding. Bound by `chain`; nil outside one, where it simply recomputes.{:literal <antecedent> :moved {context (:all | #{pair})}}, or nil.
What makes a re-join semi-naive. A qualitative fact re-joins every rule mentioning
its calculus, and joining over every pair the network entails means the nth arriving
fact redoes what the (n-1)th already did. Bound by rejoin-qualitative to the pairs
that have moved since the last such re-join (qcn-kb/join-delta), it narrows the
enumeration of one antecedent — the named literal — and leaves the rest full.
One antecedent, because that is the delta rule: for a rule with two qualitative
antecedents, narrowing both at once would drop every firing pairing a moved binding with
an unmoved one. So rejoin-qualitative runs the join once per qualitative antecedent,
each with a different one narrowed, and the overlap re-derives conclusions the TMS
dedups.
Read by literal rather than by position: plan/order reorders the antecedents, so a
position means nothing by the time the join runs. Two identical antecedents in one rule
are both narrowed, which is the same set — they bind identically.
`{:literal <antecedent> :moved {context (:all | #{pair})}}`, or nil.
What makes a re-join **semi-naive**. A qualitative fact re-joins every rule mentioning
its calculus, and joining over every pair the network entails means the nth arriving
fact redoes what the (n-1)th already did. Bound by `rejoin-qualitative` to the pairs
that have moved since the last such re-join (`qcn-kb/join-delta`), it narrows the
enumeration of **one** antecedent — the named literal — and leaves the rest full.
One antecedent, because that is the delta rule: for a rule with two qualitative
antecedents, narrowing both at once would drop every firing pairing a moved binding with
an unmoved one. So `rejoin-qualitative` runs the join once per qualitative antecedent,
each with a different one narrowed, and the overlap re-derives conclusions the TMS
dedups.
Read by literal rather than by position: `plan/order` reorders the antecedents, so a
position means nothing by the time the join runs. Two identical antecedents in one rule
are both narrowed, which is the same set — they bind identically.Whether a completed firing that finds no placement context files a :no-placement
entry. True wherever content arrives, which is every path a caller drives: a firing
that did everything but conclude is silent otherwise, and it is the commonest
first-session mistake.
False for the re-chain a teardown owes (core/settle-after-teardown!). That pass
re-asks firings the removal already swept, to learn which of them a surviving route
still licenses — so one it cannot place is a restatement of the retraction rather than a
diagnosis of the KB, and the caller who took the wiring away is the last person who
needs telling. Filing one per killed firing would also cost the ledger its real
entries, which cap at 1000, and a :warn line apiece.
Whether a completed firing that finds no placement context files a `:no-placement` entry. True wherever content arrives, which is every path a caller drives: a firing that did everything but conclude is silent otherwise, and it is the commonest first-session mistake. **False for the re-chain a teardown owes** (`core/settle-after-teardown!`). That pass re-asks firings the removal already swept, to learn which of them a surviving route still licenses — so one it cannot place is a restatement of the retraction rather than a diagnosis of the KB, and the caller who took the wiring away is the last person who needs telling. Filing one per killed firing would also cost the ledger its real entries, which cap at 1000, and a `:warn` line apiece.
Whether a run generates each satisfying antecedent combination once rather than
once per side that can trigger it (see *agenda-arrivals*). On by default; bound
false to enumerate every trigger, which is the reference side the oracles compare
against (witness_order_test, rete_oracle_test). A pure cost decision: the
suppressed firings are duplicates of ones the run makes anyway, so the derived set
and its supports are the same either way.
Whether a run generates each satisfying antecedent combination **once** rather than once per side that can trigger it (see `*agenda-arrivals*`). On by default; bound **false** to enumerate every trigger, which is the reference side the oracles compare against (`witness_order_test`, `rete_oracle_test`). A pure cost decision: the suppressed firings are duplicates of ones the run makes anyway, so the derived set and its supports are the same either way.
(answered-by-calculus? kb pred)Can a registered calculus answer a goal on pred — pred or a sub-predicate of it is
one a calculus claims? Such a goal's answer moves with the whole network rather than
with the facts on its own arguments. The global closure, as a re-check trigger reads
it: a sub-predicate any context sees can answer there.
Can a registered calculus answer a goal on `pred` — `pred` or a sub-predicate of it is one a calculus claims? Such a goal's answer moves with the whole network rather than with the facts on its own arguments. The global closure, as a re-check trigger reads it: a sub-predicate any context sees can answer there.
(chain kb seed opts)Semi-naive fixpoint forward chaining seeded with seed, strict and defeasible
rules together on the one agenda.
opts may carry an :on-progress callback, called about four times a second
(:progress-every-ms) with
{:derived n :pending n} — what the run has concluded, and how much agenda is left. A
fixpoint has no total to count towards (the agenda grows as it derives), so those two
numbers are all a run can report of where it is; both are O(1) to take. The callback
may throw, which aborts the run — the one interruption point chaining has, and how a
loader cancels one. What had already been derived stays: the conclusions are placed as
they are made, so an aborted fixpoint is a KB holding a prefix of the run, not a corrupt
one.
Reporting happens at two points, and it takes both to keep a bar moving: at the agenda
loop, which sees the run between datums, and at each rule firing (*tick*), which is
inside the one datum that can run for minutes. The remaining silent stretch is a single
unproductive join — a match search that yields nothing for a long time never reaches a
firing — which is bounded by the extent it is scanning rather than by the corpus.
Semi-naive fixpoint forward chaining seeded with `seed`, strict and defeasible
rules together on the one agenda.
`opts` may carry an **`:on-progress`** callback, called about four times a second
(`:progress-every-ms`) with
`{:derived n :pending n}` — what the run has concluded, and how much agenda is left. A
fixpoint has no total to count towards (the agenda grows as it derives), so those two
numbers are all a run can report of where it is; both are O(1) to take. The callback
may **throw**, which aborts the run — the one interruption point chaining has, and how a
loader cancels one. What had already been derived stays: the conclusions are placed as
they are made, so an aborted fixpoint is a KB holding a prefix of the run, not a corrupt
one.
Reporting happens at two points, and it takes both to keep a bar moving: at the agenda
loop, which sees the run between datums, and at each rule firing (`*tick*`), which is
inside the one datum that can run for minutes. The remaining silent stretch is a single
*unproductive* join — a match search that yields nothing for a long time never reaches a
firing — which is bounded by the extent it is scanning rather than by the corpus.(chain-all kb seed opts)One fixpoint from seed, strict and defeasible rules on the same agenda (there
is no separate defaults phase — see fire-rules-for).
Opens a new run in chain-stats — violations recorded during the run carry its
id — and stashes the result there, warning when the run was truncated. The ledger
accumulates across runs rather than resetting per run, so a bulk load's drops
stay observable one assert later; and because internal callers discard the
:truncated? flag, the :warn log is how a depth-capped chain's lost conclusions
surface.
At :debug every run says what it did, truncated or not — the run is the boundary a
log statement belongs at, and without one a chain that concluded nothing, a chain that
concluded forty thousand things and a chain still joining are the same silence to
somebody watching a load.
One fixpoint from `seed`, strict and defeasible rules on the same agenda (there is no separate defaults phase — see `fire-rules-for`). Opens a new run in `chain-stats` — violations recorded during the run carry its id — and stashes the result there, warning when the run was truncated. The ledger **accumulates** across runs rather than resetting per run, so a bulk load's drops stay observable one assert later; and because internal callers discard the `:truncated?` flag, the :warn log is how a depth-capped chain's lost conclusions surface. At `:debug` every run says what it did, truncated or not — the run is the boundary a log statement belongs at, and without one a chain that concluded nothing, a chain that concluded forty thousand things and a chain still joining are the same silence to somebody watching a load.
(closed-extent-antecedents kb antes)The rule's negative antecedents a closed_extent_predicate grant turns into negation as
failure — closed (every variable bound by a generator) and declared closed somewhere.
The join withholds these and derive time decides them, exactly as it does an unknown.
One set read for a KB that declares no closed extent, which is the common one.
The rule's negative antecedents a `closed_extent_predicate` grant turns into negation as failure — closed (every variable bound by a generator) and declared closed somewhere. The join withholds these and derive time decides them, exactly as it does an `unknown`. One set read for a KB that declares no closed extent, which is the common one.
(closed-extent-blocks? kb ce-antes bindings pctx)Is a firing blocked because one of its withheld negative antecedents does not hold
in pctx?
The question asked is the whole level-6 one, not "is there a positive answer": a
stored (not (P a)) answers it as it always did, and under a visible grant
ClosedExtentProver answers it from the absence of a positive. So a placement context
that cannot see the grant reads the literal exactly as it does today, and the
withholding costs it only the support handle — which the re-check index gives back, by
bringing the firing round again when anything on P moves.
Block-if-any, like unknown: each withheld literal independently has to hold.
Is a firing blocked because one of its withheld negative antecedents does **not** hold in `pctx`? The question asked is the whole level-6 one, not "is there a positive answer": a stored `(not (P a))` answers it as it always did, and under a visible grant `ClosedExtentProver` answers it from the absence of a positive. So a placement context that cannot see the grant reads the literal exactly as it does today, and the withholding costs it only the support handle — which the re-check index gives back, by bringing the firing round again when anything on `P` moves. Block-if-**any**, like `unknown`: each withheld literal independently has to hold.
The two closure generations an argument conviction is read through — genl for the
argument's types, genlCx for which declarations and memberships its context sees.
special/taxonomy-generations itself: settle compares this against the stamp
special puts on a refused mint or lift, so the two cannot be two definitions.
The two closure generations an argument conviction is read through — `genl` for the argument's types, `genlCx` for which declarations and memberships its context sees. `special/taxonomy-generations` itself: `settle` compares this against the stamp `special` puts on a refused mint or lift, so the two cannot be two definitions.
(constraint-refusals kb)Every :constraint entry in the refusal record, as [rule-handle entry] pairs, sorted
on the rule handle and then on the conclusion and its context, read off the rules the
kind roster names (special/kind-entries). Each entry is re-asked on its own, so
the order decides no placement.
Every `:constraint` entry in the refusal record, as `[rule-handle entry]` pairs, sorted on the rule handle and then on the conclusion and its context, read off the rules the kind roster names (`special/kind-entries`). Each entry is re-asked on its own, so the order decides no placement.
max-depth bounds derivation depth to catch productive infinite recursion; max-derivations is a hard backstop on a single chain run.
max-depth bounds derivation depth to catch productive infinite recursion; max-derivations is a hard backstop on a single chain run.
(different-blocks? kb different-antes bindings)Is a firing blocked because one of its (different …) antecedents no longer holds
under bindings? Block-if-any, for naf-blocks?' reason: each one independently
requires its arguments to lie in no shared equivalence class and neither of them to be
an unpinned indeterminate_term, so one that stops holding withdraws the conclusion.
A justification cannot express this. different is negation as failure over the
equality closure and over the indeterminate_term category, so it holds by the
absence of a merge and names no fact a firing's antecedents could carry — the
SupportingProver contract has nothing to report, and different is not assertible
(wff/different-problems), so no handle for it exists to name. The re-check index is
therefore the only instrument that can withdraw such a firing, and this is where it
reads (docs/predall.md, rules/different-flip-predicates).
bindings are the settled ones, so an argument the equality closure has since
merged arrives here as its representative and the test fails on the = arm. The goal
goes to the registry under ?ctx, which is the context solve-deferred joins it under:
the two decisions have to read the literal the same way, or a firing would be placed and
blocked in the same settle.
Is a firing blocked because one of its `(different …)` antecedents no longer holds under `bindings`? Block-if-**any**, for `naf-blocks?`' reason: each one independently requires its arguments to lie in no shared equivalence class and neither of them to be an unpinned `indeterminate_term`, so one that stops holding withdraws the conclusion. A justification cannot express this. `different` is negation as failure over the equality closure and over the `indeterminate_term` category, so it holds by the *absence* of a merge and names no fact a firing's antecedents could carry — the `SupportingProver` contract has nothing to report, and `different` is not assertible (`wff/different-problems`), so no handle for it exists to name. The re-check index is therefore the only instrument that can withdraw such a firing, and this is where it reads (docs/predall.md, `rules/different-flip-predicates`). `bindings` are the **settled** ones, so an argument the equality closure has since merged arrives here as its representative and the test fails on the `=` arm. The goal goes to the registry under `?ctx`, which is the context `solve-deferred` joins it under: the two decisions have to read the literal the same way, or a firing would be placed and blocked in the same settle.
(drop-refusal! kb rh entry)Retire one entry. A refusal is dead when it fires, when its rule goes, or when the
antecedents behind its bindings are no longer believed — the bindings are a snapshot,
and a refusal must not resurrect a firing whose support left. An :overflow record
holds no entries to drop.
Retire one entry. A refusal is dead when it fires, when its rule goes, or when the antecedents behind its bindings are no longer believed — the bindings are a snapshot, and a refusal must not resurrect a firing whose support left. An `:overflow` record holds no entries to drop.
(entailment-withdrawable? kb rsx)Can entailment-withdrawn? answer true for any firing of the rule rsx, whatever
context it was placed in? Only while a calculus it joins on is unsatisfiable
somewhere (qkb/unsatisfiable-somewhere?). False lets a settle skip every firing of
the rule its blocked set does not already hold.
Can `entailment-withdrawn?` answer true for any firing of the rule `rsx`, whatever context it was placed in? Only while a calculus it joins on is unsatisfiable somewhere (`qkb/unsatisfiable-somewhere?`). False lets a settle skip every firing of the rule its blocked set does not already hold.
(exception-holds? kb except bindings pctx)Does except — a rule's exception, a vector of literals — hold under bindings,
evaluated in pctx, the context the conclusion would be placed in?
Three properties make this cheap, and each is required:
sentex constructor), so substitution leaves a ground question. The conjuncts
therefore share nothing and need no join — each is an independent existence check,
and all must hold.first stops
the query at its first result rather than enumerating an extent.arg, where an argument whose type is
unknown cannot violate a constraint: blocking on "cannot tell" would let a
missing fact silently suppress knowledge.An empty / absent exception never holds, so an ordinary rule takes no cost here.
Defined in vaelii.impl.provers because the backward chainers need exactly the same
judgement; pctx here is the conclusion's placement context, where backward passes
the query's.
Does `except` — a rule's exception, a vector of literals — hold under `bindings`, evaluated in `pctx`, the context the conclusion would be placed in? Three properties make this cheap, and each is required: * **Closed.** Every exception variable is bound by an antecedent (enforced in the `sentex` constructor), so substitution leaves a *ground* question. The conjuncts therefore share nothing and need no join — each is an independent existence check, and **all** must hold. * **One answer suffices.** The levels stack is lazy throughout, so `first` stops the query at its first result rather than enumerating an extent. * **An unanswerable exception does not hold**, and the rule fires. That is the open-world reading, and it matches `arg`, where an argument whose type is unknown cannot violate a constraint: blocking on "cannot tell" would let a missing fact silently suppress knowledge. An empty / absent exception never holds, so an ordinary rule takes no cost here. Defined in `vaelii.impl.provers` because the backward chainers need exactly the same judgement; `pctx` here is the conclusion's placement context, where backward passes the query's.
The informant of every justification a guard defeat stores (place-guard-defeats!).
The informant of every justification a guard defeat stores (`place-guard-defeats!`).
(justification-excepted? kb j)Is justification j currently blocked — by a visibility except hiding one of its
antecedents, or by anything its rule carries (rule-firing-blocked?)?
The conclusion's record names the placement context every check is evaluated in, and the informant names the rule.
Is justification `j` currently blocked — by a visibility `except` hiding one of its antecedents, or by anything its rule carries (`rule-firing-blocked?`)? The conclusion's record names the placement context every check is evaluated in, and the informant names the rule.
How many refused firings one rule's record keeps before it stops keeping them individually.
One entry per refused firing is bounded by what a rule did not derive, and a rule
excepted on a common condition can refuse far more than it places — so unlike blocking
it is not bounded by the store. Past this many entries the rule's record collapses to
:overflow and it takes the coarse fallback instead: a queued overflowed rule forces a
productive settle pass and is re-joined over its extent, which finds the same
releases at the cost the record exists to avoid. Correct on both sides of the line,
and the line is stated in docs/exceptions.md.
How many refused firings one rule's record keeps before it stops keeping them individually. One entry per refused firing is bounded by what a rule did **not** derive, and a rule excepted on a common condition can refuse far more than it places — so unlike blocking it is not bounded by the store. Past this many entries the rule's record collapses to `:overflow` and it takes the coarse fallback instead: a queued overflowed rule forces a productive settle pass and is re-joined over its extent, which finds the same releases at the cost the record exists to avoid. Correct on both sides of the line, and the line is stated in docs/exceptions.md.
(naf-blocks? kb naf-antes bindings pctx)Is a firing blocked by any of its unknown antecedents naf-antes — is any inner
query derivable under bindings, in pctx? Block-if-any: each (unknown S)
independently requires S absent, so one derivable S withdraws the conclusion.
Is a firing blocked by any of its `unknown` antecedents `naf-antes` — is any inner query derivable under `bindings`, in `pctx`? Block-if-**any**: each `(unknown S)` independently requires `S` absent, so one derivable `S` withdraws the conclusion.
The informant of every justification a placed nogood stores (place-nogood!).
The informant of every justification a placed nogood stores (`place-nogood!`).
(place-guard-defeats! kb firings)For each [j live? conds] of firings, j a firing's justification record and
conds its block conditions or nil (guard-defeat-placements): store
(defeat (sentexHandle F)), F its conclusion, at each context guard-defeat-placements
names, justified there under guard-informant at :default, and drop each guard
justification the firing owns (guard-justifications) that the current state no longer
gives. A firing that is not live?, blocked or gone, keeps none. A change posts F's
re-check (special/recheck-defeat-target). Returns the conclusions whose guard
defeats moved. The defeat is read at read time (exc/defeat-hidden-fn, its coverage);
chain reads none. See docs/naf.md.
For each `[j live? conds]` of `firings`, `j` a firing's justification record and `conds` its block conditions or nil (`guard-defeat-placements`): store `(defeat (sentexHandle F))`, F its conclusion, at each context `guard-defeat-placements` names, justified there under `guard-informant` at `:default`, and drop each guard justification the firing owns (`guard-justifications`) that the current state no longer gives. A firing that is not `live?`, blocked or gone, keeps none. A change posts F's re-check (`special/recheck-defeat-target`). Returns the conclusions whose guard defeats moved. The defeat is read at read time (`exc/defeat-hidden-fn`, its coverage); `chain` reads none. See docs/naf.md.
(place-inherited! kb region)Find the inherited clashes (discovery/discover-inherited!) and place each found one
at its vantages, the most general contexts that read it whole, justified by its members
(the stored claim and the reading's reasons) and the genlCx edges each vantage sees
them over, and remove the placements of each member set no longer found
(place-justified!), in content order. Returns the handles created. A clash whose
memo entry was carried keeps its placements. A rebuild's settle places too
(docs/nmtms.md, "A recover places the nogoods its store does not hold").
Find the inherited clashes (`discovery/discover-inherited!`) and place each found one at its vantages, the most general contexts that read it whole, justified by its members (the stored claim and the reading's reasons) and the `genlCx` edges each vantage sees them over, and remove the placements of each member set no longer found (`place-justified!`), in content order. Returns the handles created. A clash whose memo entry was carried keeps its placements. A rebuild's settle places too (docs/nmtms.md, "A `recover` places the nogoods its store does not hold").
(place-nogood! kb members grounds)(place-nogood! kb members grounds within)Place the nogood over the handles members, detected with the handles grounds, at
each maximal context that sees the contexts the members and grounds are stated in and
where no except hides one of them (res/exception-aware-placements, the placement a
firing's conclusion takes), each justified by the members, the grounds and the genlCx
edges the placement sees them over (visibility-support), so retracting any of them
takes it OUT (place-justified!, over the placements of the same members and grounds).
Returns the handles it created. The caller states the nogood: every member IN in the
network. With the context set within, only the placements in it are compared
(place-justified!): a genlCx move changes the placements in the contexts whose
ancestor sets it changed and no others (decide/edge-reach's :under). See
docs/nmtms.md.
Place the nogood over the handles `members`, detected with the handles `grounds`, at each maximal context that sees the contexts the members and grounds are stated in and where no except hides one of them (`res/exception-aware-placements`, the placement a firing's conclusion takes), each justified by the members, the grounds and the `genlCx` edges the placement sees them over (`visibility-support`), so retracting any of them takes it OUT (`place-justified!`, over the placements of the same members and grounds). Returns the handles it created. The caller states the nogood: every member IN in the network. With the context set `within`, only the placements in it are compared (`place-justified!`): a `genlCx` move changes the placements in the contexts whose ancestor sets it changed and no others (`decide/edge-reach`'s `:under`). See docs/nmtms.md.
(place-nogoods! kb region read)Place, once a settle pass, the nogoods of the families placed as conclusions whose
placement can have moved since the last call, and return the handles created: the
negation pairs (place-negations!), the membership nogoods (place-memberships!), the
related-types nogoods (place-related!), the tuple nogoods (place-tuples!) and the
arity nogoods (place-arities!). Every family detects over the network's IN label, a
superseded member included (jtms/network-in?), so a supersession moves no placement.
Each family reads what its write-time index queued, the handles among region (a delay)
relabelled that read (a volatile set) does not hold yet, which this adds, the handles
an except of which arrived or left and what rests on them, the placed contradicts
among them, and the genlCx edges moved since (decide/edge-reach). Reads nothing
while no family holds a nogood or queued one and no orthogonal is stored.
Place, once a settle pass, the nogoods of the families placed as conclusions whose placement can have moved since the last call, and return the handles created: the negation pairs (`place-negations!`), the membership nogoods (`place-memberships!`), the related-types nogoods (`place-related!`), the tuple nogoods (`place-tuples!`) and the arity nogoods (`place-arities!`). Every family detects over the network's IN label, a superseded member included (`jtms/network-in?`), so a supersession moves no placement. Each family reads what its write-time index queued, the handles among `region` (a delay) relabelled that `read` (a volatile set) does not hold yet, which this adds, the handles an except of which arrived or left and what rests on them, the placed `contradicts` among them, and the `genlCx` edges moved since (`decide/edge-reach`). Reads nothing while no family holds a nogood or queued one and no `orthogonal` is stored.
(placement-queued? kb)Has the negation, membership, related-types, tuple or arity index queued a nogood the
settle places again (negation/take-moved!, membership/take-moved!,
related/take-moved!, tuple/take-moved!, arity/take-moved!)? A rebuilt index
queues every standing one (recover). The negation family keeps no candidate rows:
after a rebuild every pair is owed while a body is stored in both polarities
(decide/placements-owed?, reads/stores-opposed?).
Has the negation, membership, related-types, tuple or arity index queued a nogood the settle places again (`negation/take-moved!`, `membership/take-moved!`, `related/take-moved!`, `tuple/take-moved!`, `arity/take-moved!`)? A rebuilt index queues every standing one (`recover`). The negation family keeps no candidate rows: after a rebuild every pair is owed while a body is stored in both polarities (`decide/placements-owed?`, `reads/stores-opposed?`).
(post-join-bindings kb literals bindings pctx)Extend bindings with what a firing's post-join literals compute
(rules/post-join-literals), solving each through the registry under the bindings the
earlier ones produced: an aggregate in pctx, any other literal in the wildcard, the
context solve-deferred gives it in the join.
Nil is a block: a literal has no answer, its already-bound output no longer
matches the recomputed value, or its solutions disagree, which is also filed as
:post-join-ambiguous with the solutions in content order. At most two solutions are
realized (docs/aggregate.md, "Comparing the count").
Extend `bindings` with what a firing's post-join literals compute (`rules/post-join-literals`), solving each through the registry under the bindings the earlier ones produced: an aggregate in `pctx`, any other literal in the wildcard, the context `solve-deferred` gives it in the join. Nil is a **block**: a literal has no answer, its already-bound output no longer matches the recomputed value, or its solutions disagree, which is also filed as `:post-join-ambiguous` with the solutions in content order. At most two solutions are realized (docs/aggregate.md, "Comparing the count").
(reconcile-reified! kb fns)Bring the stored rows a reifiable_function mark moving re-spells to the spellings
their readers read, for every function in fns — the ones whose mark moved since the
last settle (special/note-permuting-moves!), or whose readers came to disagree
(nat/queue-split-uses!, special/note-mark-reach!) — and return the handles that are
new content, for the agenda.
The mark arriving reifies each stored application of f, minting what has no term; the
mark leaving spells each use of a constant minted for f with the expression again
(nat/respell-region, nat/respelled). A row moves in place, or folds into the row
already holding its new spelling (integrate/move-row!), carrying its written spellings
through the same re-spell. Where the readers of a row disagree on a mark, the row
stays as written and each other spelling a reader reads is stored justified respell
by it and the mark (reified-plan, sync-respellings!). The constants the moved rows
stop naming are then collected (collect-respelled-orphans!). Linear in the region:
a declaration written before its applications reaches none of them, and a KB declaring
no reifiable function never queues one.
Bring the stored rows a `reifiable_function` mark moving re-spells to the spellings their readers read, for every function in `fns` — the ones whose mark moved since the last settle (`special/note-permuting-moves!`), or whose readers came to disagree (`nat/queue-split-uses!`, `special/note-mark-reach!`) — and return the handles that are new content, for the agenda. The mark arriving reifies each stored application of `f`, minting what has no term; the mark leaving spells each use of a constant minted for `f` with the expression again (`nat/respell-region`, `nat/respelled`). A row moves in place, or folds into the row already holding its new spelling (`integrate/move-row!`), carrying its written spellings through the same re-spell. Where the readers of a row disagree on a mark, the row stays as written and each other spelling a reader reads is stored justified `respell` by it and the mark (`reified-plan`, `sync-respellings!`). The constants the moved rows stop naming are then collected (`collect-respelled-orphans!`). Linear in the region: a declaration written before its applications reaches none of them, and a KB declaring no reifiable function never queues one.
(reconcile-spellings! kb preds)(reconcile-spellings! kb preds rows)Bring the stored rows of every predicate in preds — the ones whose permuting marks
moved since the last settle (special/note-permuting-moves!), or whose marks a placed
defeat or an except moved at some reader (special/note-mark-reach!) — and the rows
rows a write stored while its predicate's readers disagree, to the spellings their
readers read (respell-rows!), and return the handles that are new content, for the
agenda. Linear in the moved predicates' stored rows, with a provenance read per row: a
mark moving is a declaration reaching its facts, and commute-existing pays the same
on arrival.
Bring the stored rows of every predicate in `preds` — the ones whose permuting marks moved since the last settle (`special/note-permuting-moves!`), or whose marks a placed `defeat` or an `except` moved at some reader (`special/note-mark-reach!`) — and the rows `rows` a write stored while its predicate's readers disagree, to the spellings their readers read (`respell-rows!`), and return the handles that are new content, for the agenda. Linear in the moved predicates' stored rows, with a provenance read per row: a mark moving is a declaration reaching its facts, and `commute-existing` pays the same on arrival.
(record-swept-firing! kb j)Record the rule firing whose justification record is j as a refusal, when the
settle blocks it after its placement and the sweep deletes it: the entry a firing
refused at its placement would have recorded, so the trigger that lifts the block
releases it from its bindings (release-refusal!) and not by a join over the rule's
extent. :handles is every antecedent but the rule. Records nothing for a firing
an except hides an antecedent of at its placement, which the refusal record does not
hold (docs/exceptions.md, "A refused firing is remembered as bindings"). Reads the
conclusion's record, so it runs before the sweep's records are deleted.
Record the rule firing whose justification record is `j` as a refusal, when the settle blocks it after its placement and the sweep deletes it: the entry a firing refused at its placement would have recorded, so the trigger that lifts the block releases it from its bindings (`release-refusal!`) and not by a join over the rule's extent. `:handles` is every antecedent but the rule. Records nothing for a firing an `except` hides an antecedent of at its placement, which the refusal record does not hold (docs/exceptions.md, "A refused firing is remembered as bindings"). Reads the conclusion's record, so it runs before the sweep's records are deleted.
(redecide-constraint-refusal! kb rh entry gens)Re-ask :constraint entry entry of rule rh under generations gens: :free when
the conviction no longer holds and the conclusion is owed a placement, nil otherwise.
An entry whose firing has left is retired. One still convicted is restamped with
gens and with the term of the conviction read now (checks/conviction-watch), not
the term it was recorded with, so the entry is re-asked when the argument it is
convicted on is lifted, whichever argument that has become. The term is read by
checks/conviction-watch, the reader record-constraint-drop! records with, so the
restamped entry watches the term a firing refused now would record — which is what a
recover that rebuilds the record by re-firing records.
Re-ask `:constraint` entry `entry` of rule `rh` under generations `gens`: `:free` when the conviction no longer holds and the conclusion is owed a placement, nil otherwise. An entry whose firing has left is retired. One still convicted is restamped with `gens` and with the term of the conviction read now (`checks/conviction-watch`), not the term it was recorded with, so the entry is re-asked when the argument it is convicted on is lifted, whichever argument that has become. The term is read by `checks/conviction-watch`, the reader `record-constraint-drop!` records with, so the restamped entry watches the term a firing refused now would record — which is what a `recover` that rebuilds the record by re-firing records.
(refusal-state kb rh entry)Re-decide one recorded refusal of rule rh, from scratch: :dead when there is no
longer a firing to make, :blocked when the condition that refused it still holds,
:free when it does not and the conclusion is owed a placement.
Nothing remembers the previous answer — the record says which firings to re-ask and
never what the answer is, exactly as exception-blocked-set re-decides every
candidate justification it looks at. Blocking would otherwise drift from belief.
The judgement is rule-firing-blocked?, the same one a placed firing's justification
is re-decided by, plus the visibility except check the justification path also runs.
Bindings are settled to the representatives pctx now elects first, for the reason
settled-bindings records: a snapshot asks about a spelling a merge has retired, and
the empty result that comes back reads as not excepted.
Re-decide one recorded refusal of rule `rh`, from scratch: `:dead` when there is no longer a firing to make, `:blocked` when the condition that refused it still holds, `:free` when it does not and the conclusion is owed a placement. Nothing remembers the previous answer — the record says which firings to re-ask and never what the answer is, exactly as `exception-blocked-set` re-decides every candidate justification it looks at. Blocking would otherwise drift from belief. The judgement is `rule-firing-blocked?`, the same one a placed firing's justification is re-decided by, plus the visibility `except` check the justification path also runs. Bindings are settled to the representatives `pctx` now elects first, for the reason `settled-bindings` records: a snapshot asks about a spelling a merge has retired, and the empty result that comes back reads as *not excepted*.
(refusals kb rh)What is recorded against rule rh: a set of refusal entries, :overflow, or nil.
settle reads this to decide which firings a queued rule owes a re-ask.
What is recorded against rule `rh`: a set of refusal entries, `:overflow`, or nil. `settle` reads this to decide which firings a queued rule owes a re-ask.
(release-refusal! kb rh entry)Re-derive the refused firing entry of rule rh and retire the entry, or retire it
without deriving anything when its support has left. Returns the handles the
re-derivation created, for the caller to put back on the agenda.
place-conclusion with the recorded bindings, never a fresh join — that is the
whole cost argument: re-deriving k recorded refusals is k placements, where seeding
chain with the rule handle joins it over the whole fact extent. The conclusion, its
placement context and its antecedent list are the ones the refused firing computed, so
the justification is the one that firing would have made; the depth is recomputed from
the antecedent facts, as a fresh firing would compute it.
Re-decided here rather than trusted from the caller's scan: the sweep runs in between, and a refusal whose support it collected must not be placed on the strength of an answer taken before it ran.
Re-derive the refused firing `entry` of rule `rh` and retire the entry, or retire it without deriving anything when its support has left. Returns the handles the re-derivation created, for the caller to put back on the agenda. **`place-conclusion` with the recorded bindings, never a fresh join** — that is the whole cost argument: re-deriving k recorded refusals is k placements, where seeding `chain` with the rule handle joins it over the whole fact extent. The conclusion, its placement context and its antecedent list are the ones the refused firing computed, so the justification is the one that firing would have made; the depth is recomputed from the antecedent facts, as a fresh firing would compute it. Re-decided here rather than trusted from the caller's scan: the sweep runs in between, and a refusal whose support it collected must not be placed on the strength of an answer taken before it ran.
(rerecord-refusals! kb)Rebuild the refusal record by re-firing every rule that can refuse a firing. Returns the chain result, or nil for a KB where no rule carries a re-checkable block condition.
recover's half of the record. A refused firing left no justification, so nothing in
the store holds it and replaying the stored justifications cannot bring it back — the
record is derived state and is rebuilt the way blocking is, by re-deciding rather than
by reading. Re-firing is what re-decides it: a firing that can be placed is placed and
deduped by has-justification?, and one that is refused re-records.
Run after the settle that establishes belief, since a refusal is a claim about what
the KB believes, and relabel deliberately lands unblocked. ! because it discards
the record it replaces.
Re-fires at the default depth bound — (chain kb live nil) carries no run config —
so the rebuilt entries record that default rather than whatever bound each original run
set. A run's :max-depth is transient live-session config no store holds, exactly as
recover resets derivation depths to 0 (a bound only governs future chaining), so a
KB chained under a non-default bound rebuilds its refusals, and releases them, at the
default. The recovered KB is internally consistent at that default; docs/exceptions.md
states the one narrow case it can differ from the live session in.
Rebuild the refusal record by re-firing every rule that can refuse a firing. Returns the chain result, or nil for a KB where no rule carries a re-checkable block condition. `recover`'s half of the record. A refused firing left no justification, so nothing in the store holds it and replaying the stored justifications cannot bring it back — the record is derived state and is rebuilt the way blocking is, by re-deciding rather than by reading. Re-firing is what re-decides it: a firing that can be placed is placed and deduped by `has-justification?`, and one that is refused re-records. Run **after** the settle that establishes belief, since a refusal is a claim about what the KB believes, and `relabel` deliberately lands unblocked. `!` because it discards the record it replaces. Re-fires at the **default** depth bound — `(chain kb live nil)` carries no run config — so the rebuilt entries record that default rather than whatever bound each original run set. A run's `:max-depth` is transient live-session config no store holds, exactly as `recover` resets derivation depths to 0 (a bound only governs *future* chaining), so a KB chained under a non-default bound rebuilds its refusals, and releases them, at the default. The recovered KB is internally consistent at that default; docs/exceptions.md states the one narrow case it can differ from the live session in.
The informant of a justification storing a spelling a reader reads of a fact, from the
row holding the fact as written and the marks that sort it (ensure-respellings!).
The informant of a justification storing a spelling a reader reads of a fact, from the row holding the fact as written and the marks that sort it (`ensure-respellings!`).
(rule-firing-report kb)Per forward rule in the KB, what it did with itself: how many firings it placed, how many it refused and why, or whether it did nothing at all. The read behind the chaining funnel (docs/web.md) — the ontological engineer's which of my rules actually do anything.
Rules are enumerated off the antecedent roster (:rule-antecedents) unioned through the
rule index, so this costs O(rules), never a scan of the fact extent. Everything else
is read from what a run already leaves standing — jtms/dependents on a rule handle is
every firing it licensed, and the refusal ledger (refusals / refusal-state, each
entry re-decided against current belief) is what it completed but did not place — so
the funnel needs no per-run instrumentation: the stored ledger and the justification
graph answer it, and a counter beside them would only restate what they already hold.
Each row is {:rule :sentence :believed? :placed :refused :refusals :status}.
:placed is the firing count. :refused is :overflow when the ledger capped the rule,
else the entry count. :refusals is one map per recorded refusal — its live :state
(:blocked / :dead / :free, re-decided now) and, for one that still blocks, the
:reason (:post-join / :exception / :naf / :hidden), plus the :conseq it could
not place and the :context. :status is :fires (placed at least one), :blocked
(placed none, refused at least one), or :silent (no antecedent set ever completed —
nothing placed and nothing refused).
Per forward rule in the KB, what it did with itself: how many firings it **placed**,
how many it **refused** and why, or whether it did nothing at all. The read behind the
chaining funnel (docs/web.md) — the ontological engineer's *which of my rules actually
do anything*.
Rules are enumerated off the antecedent roster (`:rule-antecedents`) unioned through the
rule index, so this costs `O(rules)`, never a scan of the fact extent. Everything else
is read from what a run already leaves standing — `jtms/dependents` on a rule handle is
every firing it licensed, and the refusal ledger (`refusals` / `refusal-state`, each
entry re-decided against *current* belief) is what it completed but did not place — so
the funnel needs no per-run instrumentation: the stored ledger and the justification
graph answer it, and a counter beside them would only restate what they already hold.
Each row is `{:rule :sentence :believed? :placed :refused :refusals :status}`.
`:placed` is the firing count. `:refused` is `:overflow` when the ledger capped the rule,
else the entry count. `:refusals` is one map per recorded refusal — its live `:state`
(`:blocked` / `:dead` / `:free`, re-decided now) and, for one that still blocks, the
`:reason` (`:post-join` / `:exception` / `:naf` / `:hidden`), plus the `:conseq` it could
not place and the `:context`. `:status` is `:fires` (placed at least one), `:blocked`
(placed none, refused at least one), or `:silent` (no antecedent set ever completed —
nothing placed and nothing refused).(rule-view-of kb handle rsx)The chainer's view of a rule sentex. :strength is the justification class its
firings confer (provers/firing-strength).
The chainer's view of a rule sentex. `:strength` is the justification class its firings confer (`provers/firing-strength`).
(solve-rule kb antecedents)(solve-rule kb antecedents b0)(solve-rule kb antecedents b0 consequent-pred)Full join of a rule's antecedents against current facts (used when a rule is
added), in cost order. The seeded arity starts from b0 instead of the empty
binding map, which is how why-not reconstructs a firing backwards from its
conclusion; consequent-pred (the rule's consequent functor, nil if unknown) lets
the planner keep the recursive literal in place.
Full join of a rule's antecedents against current facts (used when a rule is added), in cost order. The seeded arity starts from `b0` instead of the empty binding map, which is how `why-not` reconstructs a firing backwards from its conclusion; `consequent-pred` (the rule's consequent functor, nil if unknown) lets the planner keep the recursive literal in place.
(triggers-rules? kb fact)Can the ground fact, arriving, fire or re-join a forward rule: one keyed by its
predicate or a supertype (rules/trigger-keys), a calculus it moves, a preserved,
permuting, computed, transitive or closure re-join (fire-rules-for's sources)?
Storage, not belief: a rule the index posts counts whether or not it is believed.
Can the ground `fact`, arriving, fire or re-join a forward rule: one keyed by its predicate or a supertype (`rules/trigger-keys`), a calculus it moves, a preserved, permuting, computed, transitive or closure re-join (`fire-rules-for`'s sources)? Storage, not belief: a rule the index posts counts whether or not it is believed.
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 |