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. It decides work, not belief: when
two triggers of a rule enumerate the same pair, the later arrival skips the join
(arrival-admit, rule-arrival-admit, fire-rules-for), and no tie-break keys on it.
Keyed on arrival and not handle, since a datum put back on the agenda has an old handle
and a fresh arrival. A handle the run never enqueued has no arrival and is never
suppressed against; a disbelieved trigger declines the filter. Bound by chain for the
length of a run. A java.util.HashMap, since the engine is single-writer. See
docs/inference.md, "What a run pays per witness".
A mutable `{handle -> arrival}` map, the position at which each datum joined this
run's agenda, or nil, and then nothing is suppressed. It decides work, not belief: when
two triggers of a rule enumerate the same pair, the later arrival skips the join
(`arrival-admit`, `rule-arrival-admit`, `fire-rules-for`), and no tie-break keys on it.
Keyed on arrival and not handle, since a datum put back on the agenda has an old handle
and a fresh arrival. A handle the run never enqueued has no arrival and is never
suppressed against; a disbelieved trigger declines the filter. Bound by `chain` for the
length of a run. A `java.util.HashMap`, since the engine is single-writer. See
docs/inference.md, "What a run pays per witness".The lazy-forward re-joins a with-deferred-settle batch owes (owe-lazy-rejoins), as a
java.util.HashMap shaped as *computed-rejoins*' :owed, which the batch's closing
settle runs (run-batch-rejoins). Nil outside a batch.
The lazy-forward re-joins a `with-deferred-settle` batch owes (`owe-lazy-rejoins`), as a `java.util.HashMap` shaped as `*computed-rejoins*`' `:owed`, which the batch's closing settle runs (`run-batch-rejoins`). Nil outside a batch.
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 value its
full join read; nil outside a chaining run, where every closure edge re-joins in full.
A rule whose recorded value 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` value its full join read; nil outside a chaining run, where every closure edge re-joins in full. A rule whose recorded value 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 computed re-joins owed and not yet run (owe-computed-rejoins):
{:owed m :queue q}, m a java.util.HashMap from rule handle to the source datums
that owed it since its marker was queued (:all when one cannot filter the join), q
a volatile vector of the markers the agenda takes next. Nil outside a run, where a
source datum re-joins at once (docs/inference.md, "What a computed answer rests
on").
Per-run record of the computed re-joins owed and not yet run (`owe-computed-rejoins`):
`{:owed m :queue q}`, `m` a `java.util.HashMap` from rule handle to the source datums
that owed it since its marker was queued (`:all` when one cannot filter the join), `q`
a volatile vector of the markers the agenda takes next. Nil outside a run, where a
source datum re-joins at once (docs/inference.md, "What a computed answer rests
on").Per-run cache of inherit/declarations-exist?: a volatile holding the answer, or nil
(unknown); the var is nil outside a chaining run. Bound once by chain and reset by
derive-conclusion when a placed conclusion roots at a declaration functor
(note-placed-declaration!). See docs/inference.md.
Per-run cache of `inherit/declarations-exist?`: a volatile holding the answer, or nil (unknown); the var is nil outside a chaining run. Bound once by `chain` and reset by `derive-conclusion` when a placed conclusion roots at a declaration functor (`note-placed-declaration!`). See docs/inference.md.
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.
True inside a forward-chain called with :on-stop :keep: a run there that its
caller's bound ends returns :truncated? and keeps what it placed, inside
*rollback-scope* as outside it. The heap mark throws all the same (heap-check!).
True inside a `forward-chain` called with `:on-stop :keep`: a run there that its caller's bound ends returns `:truncated?` and keeps what it placed, inside `*rollback-scope*` as outside it. The heap mark throws all the same (`heap-check!`).
The source datum handles planned-join keeps rows of past its last computed or
lazy-forward antecedent, bound while it joins that antecedent, else nil. solve-lazy
proves the literal from those datums alone for a state resting on none of them.
The source datum handles `planned-join` keeps rows of past its last computed or lazy-forward antecedent, bound while it joins that antecedent, else nil. `solve-lazy` proves the literal from those datums alone for a state resting on none of them.
Per-run cache of lazy-table: a volatile holding the table, or nil (unread); the var
is nil outside a chaining run. process-datum empties it when a lazy-forward rule
arrives. A forward join proves a literal a lazy-forward rule concludes by joining the
rule's antecedents (docs/inference.md, "A lazy-forward rule").
Per-run cache of `lazy-table`: a volatile holding the table, or nil (unread); the var is nil outside a chaining run. `process-datum` empties it when a lazy-forward rule arrives. A forward join proves a literal a lazy-forward rule concludes by joining the rule's antecedents (docs/inference.md, "A lazy-forward rule").
The handles of the lazy-forward rules whose antecedents the join is proving: a rule is not offered to the join of its own antecedents.
The handles of the lazy-forward rules whose antecedents the join is proving: a rule is not offered to the join of its own antecedents.
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; vaelii.impl.rete binds
it to an alpha-memory matcher that answers the same set. With the reference bound, a
substituted antecedent with a bound indexable argument and a functor with sub-predicates
is read through res/matches-hierarchical (join-matches); binding this var to anything
else switches that off. See docs/inference.md, "Incremental rule matching".
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`; `vaelii.impl.rete` binds it to an alpha-memory matcher that answers the same set. With the reference bound, a substituted antecedent with a bound indexable argument and a functor with sub-predicates is read through `res/matches-hierarchical` (`join-matches`); binding this var to anything else switches that off. See docs/inference.md, "Incremental rule matching".
{rule-handle types} while a settle re-joins the rules a separation or nonempty move
queued (special/recheck-on-separation, special/recheck-nonempty-readers), else nil.
A rule handle named here that reaches the agenda is joined over types
(fire-rule-over-types) instead of over its extent, and a lazy-forward rule's readers
are (rejoin-lazy-readers-over-types).
`{rule-handle types}` while a settle re-joins the rules a separation or `nonempty` move
queued (`special/recheck-on-separation`, `special/recheck-nonempty-readers`), else nil.
A rule handle named here that reaches the agenda is joined over `types`
(`fire-rule-over-types`) instead of over its extent, and a lazy-forward rule's readers
are (`rejoin-lazy-readers-over-types`).{calculus-name -> #{context}}, the reader contexts an entailed antecedent is solved
against, memoized for one agenda datum (process-datum); nil outside one. Per datum and
not per run: a placed qualitative conclusion is a datum of its own whose re-join reads
the contexts afresh.
`{calculus-name -> #{context}}`, the reader contexts an entailed antecedent is solved
against, memoized for one agenda datum (`process-datum`); nil outside one. Per datum and
not per run: a placed qualitative conclusion is a datum of its own whose re-join reads
the contexts afresh.{:literal <antecedent> :moved {context (:all | #{pair})}}, or nil. Bound by
delta-fire-rule: the antecedent equal to :literal enumerates only the moved pairs
(qcn-kb/join-delta), every other one in full. Keyed by literal, not position, since
plan/order reorders the antecedents.
`{:literal <antecedent> :moved {context (:all | #{pair})}}`, or nil. Bound by
`delta-fire-rule`: the antecedent equal to `:literal` enumerates only the moved pairs
(`qcn-kb/join-delta`), every other one in full. Keyed by literal, not position, since
`plan/order` reorders the antecedents.Whether a completed firing that finds no placement context files a :no-placement
entry. True wherever content arrives. False for the re-chain a teardown owes
(core/settle-after-teardown!), which re-asks firings the removal already swept and
would otherwise fill the ledger (cap 1000) and log a :warn line apiece.
Whether a completed firing that finds no placement context files a `:no-placement` entry. True wherever content arrives. False for the re-chain a teardown owes (`core/settle-after-teardown!`), which re-asks firings the removal already swept and would otherwise fill the ledger (cap 1000) and log a `:warn` line apiece.
True inside a write whose throw rolls the store back to where the write found it
(core/undoing-refusal, edit!'s adds). A run there that its caller's bound ends,
:max-ms, :stop? or :max-derivations, throws :interrupted (docs/inference.md,
"Stopping a run"). The heap mark throws only here (heap-check!).
True inside a write whose throw rolls the store back to where the write found it (`core/undoing-refusal`, `edit!`'s adds). A run there that its caller's bound ends, `:max-ms`, `:stop?` or `:max-derivations`, throws `:interrupted` (docs/inference.md, "Stopping a run"). The heap mark throws only here (`heap-check!`).
The caller's bound on the runs under way (call-with-stop), or nil. Every run reads
the bound in force, so a settle's re-chain inside the bounded call stops with the run
before it. Read at the agenda loop, before each firing (derive-conclusion) and
before each row of every join that enumerates firings (planned-join); never by a
join that tests a condition (solve-rule), so a stop ends what a run generates and
changes no answer a placement reads.
The caller's bound on the runs under way (`call-with-stop`), or nil. Every run reads the bound in force, so a settle's re-chain inside the bounded call stops with the run before it. Read at the agenda loop, before each firing (`derive-conclusion`) and before each row of every join that enumerates firings (`planned-join`); never by a join that tests a condition (`solve-rule`), so a stop ends what a run generates and changes no answer a placement reads.
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.
nil, or a volatile {:clock n :held {key value}} that place-nogoods! binds for one
call: the witnesses subsumption-support and visibility-support read, and the edge
supporters' defeat classes, read while the change clock read n, keyed by what was
read, the walk's scope (tax/read-scope) and the reading (tax/*network-belief*,
tax/*search*). An entry is answered
only while the clock still reads n, so it equals a fresh read
(observe/note-change); a placement pass reads every route of a family before it
writes (plan-sets), and the nogoods of one family share their subsumptions.
nil, or a volatile `{:clock n :held {key value}}` that `place-nogoods!` binds for one
call: the witnesses `subsumption-support` and `visibility-support` read, and the edge
supporters' defeat classes, read while the change clock read `n`, keyed by what was
read, the walk's scope (`tax/read-scope`) and the reading (`tax/*network-belief*`,
`tax/*search*`). An entry is answered
only while the clock still reads `n`, so it equals a fresh read
(`observe/note-change`); a placement pass reads every route of a family before it
writes (`plan-sets`), and the nogoods of one family share their subsumptions.(answered-by-calculus? kb pred)Does a registered calculus claim pred or a sub-predicate of it, by the global spec
closure?
Does a registered calculus claim `pred` or a sub-predicate of it, by the global spec closure?
(arity-class-ends-moved! kb ends)(arity-class-ends-moved! kb ends defer?)Sync the class memberships of the stored memberships of every type at or below one of
ends, the lower ends of moved genl edges (arity/take-class-ends!), that reaches an
exact-arity class (sync-arity-classes!), over the unscoped closure: the class
membership is stored in CxUniverse and reads the edges in every context, as a
relation's length does. Answers {:new :violations}. defer? is
sync-arity-classes!'s.
Sync the class memberships of the stored memberships of every type at or below one of
`ends`, the lower ends of moved `genl` edges (`arity/take-class-ends!`), that reaches an
exact-arity class (`sync-arity-classes!`), over the unscoped closure: the class
membership is stored in CxUniverse and reads the edges in every context, as a
relation's length does. Answers `{:new :violations}`. `defer?` is
`sync-arity-classes!`'s.The informant of a justification of a class membership (C P) a metatype route
derives (sync-arity-classes!).
The informant of a justification of a class membership `(C P)` a metatype route derives (`sync-arity-classes!`).
(arity-classes-moved! kb sxs relabel?)(arity-classes-moved! kb sxs relabel? defer?)Sync the class memberships the stored records sxs move (class-route-memberships,
sync-arity-classes!): a membership arriving, its class rising, or a relabel of a class
membership or of a sentence installing genl edges (relabel?), which syncs below the
edges' lower ends (tax/installed-edges, arity-class-ends-moved!): a strength change
moves no edge in the taxonomy. Answers {:new :violations}. defer? is
sync-arity-classes!'s: a write's store path and its run pass *rollback-scope*.
Sync the class memberships the stored records `sxs` move (`class-route-memberships`,
`sync-arity-classes!`): a membership arriving, its class rising, or a relabel of a class
membership or of a sentence installing `genl` edges (`relabel?`), which syncs below the
edges' lower ends (`tax/installed-edges`, `arity-class-ends-moved!`): a strength change
moves no edge in the taxonomy. Answers `{:new :violations}`. `defer?` is
`sync-arity-classes!`'s: a write's store path and its run pass `*rollback-scope*`.(call-unbounded f)(f) with no bound in force and outside *rollback-scope*, so no run f starts is
stopped or interrupted (docs/inference.md, "Stopping a run"). The call's
:max-depth and :max-term-depth stay in force.
`(f)` with no bound in force and outside `*rollback-scope*`, so no run `f` starts is stopped or interrupted (docs/inference.md, "Stopping a run"). The call's `:max-depth` and `:max-term-depth` stay in force.
(call-with-stop opts f)(f) with the bound opts sets (:max-ms, a wall-clock bound in milliseconds from
now, and :stop?, a function of no arguments whose truthy answer ends the run) in force
for every run f starts, nested runs included (*stop*). A run that reaches it inside
*rollback-scope* throws :interrupted, unless *keep-on-stop* is set; outside one, or
with it set, the run returns :truncated? with what it placed kept. opts setting
neither leaves the bound in force as it is. The chain bounds opts names (:max-depth,
:max-term-depth, :max-derivations) reach the same runs (*bounds*).
`(f)` with the bound `opts` sets (`:max-ms`, a wall-clock bound in milliseconds from now, and `:stop?`, a function of no arguments whose truthy answer ends the run) in force for every run `f` starts, nested runs included (`*stop*`). A run that reaches it inside `*rollback-scope*` throws `:interrupted`, unless `*keep-on-stop*` is set; outside one, or with it set, the run returns `:truncated?` with what it placed kept. `opts` setting neither leaves the bound in force as it is. The chain bounds `opts` names (`:max-depth`, `:max-term-depth`, `:max-derivations`) reach the same runs (`*bounds*`).
(chain kb seed opts)Semi-naive fixpoint forward chaining seeded with seed, strict and defeasible rules on
one agenda. A chain bound opts does not name is the one call-with-stop holds in force
(*bounds*), else default-chain-opts'. opts may carry :on-progress, called about
four times a second (:progress-every-ms) with {:derived n :pending n}; it may throw, which
aborts the run (how a loader cancels one) and leaves the prefix derived, not a corrupt KB. A bound in force (*stop*) or
:max-derivations ends the run: inside *rollback-scope* with :interrupted, outside it or
under *keep-on-stop* without a throw, returning :truncated? with :bound naming
:max-derivations, :max-ms or :stop?. Progress reports at the agenda loop and at each
firing (*tick*); one unproductive join reports nothing until it ends, bounded by the
extent it scans.
Semi-naive fixpoint forward chaining seeded with `seed`, strict and defeasible rules on
one agenda. A chain bound `opts` does not name is the one `call-with-stop` holds in force
(`*bounds*`), else `default-chain-opts`'. `opts` may carry `:on-progress`, called about
four times a second (`:progress-every-ms`) with `{:derived n :pending n}`; it may throw, which
aborts the run (how a loader cancels one) and leaves the prefix derived, not a corrupt KB. A bound in force (`*stop*`) or
`:max-derivations` ends the run: inside `*rollback-scope*` with `:interrupted`, outside it or
under `*keep-on-stop*` without a throw, returning `:truncated?` with `:bound` naming
`:max-derivations`, `:max-ms` or `:stop?`. Progress reports at the agenda loop and at each
firing (`*tick*`); one unproductive join reports nothing until it ends, bounded by the
extent it scans.(chain-all kb seed opts)One fixpoint from seed, strict and defeasible rules on the same agenda
(fire-rules-for). Inside a run over the same store, seed is queued for that run
(*run-queue*) and no run opens. Opens a new run in chain-stats and stashes the result
there, warning when the run was truncated. Internal callers discard :truncated?, so the
warning is how a depth-capped run's lost conclusions surface. The ledger accumulates
across runs. At :debug every run logs what it did.
One fixpoint from `seed`, strict and defeasible rules on the same agenda (`fire-rules-for`). Inside a run over the same store, `seed` is queued for that run (`*run-queue*`) and no run opens. Opens a new run in `chain-stats` and stashes the result there, warning when the run was truncated. Internal callers discard `:truncated?`, so the warning is how a depth-capped run's lost conclusions surface. The ledger accumulates across runs. At `:debug` every run logs what it did.
(check-stop!)Throw :interrupted when the bound in force (*stop*) is reached or the heap mark
stops a write (heap-stop?). A write that runs no chain calls it between its writes
(core/bulk-assert-facts!).
Throw `:interrupted` when the bound in force (`*stop*`) is reached or the heap mark stops a write (`heap-stop?`). A write that runs no chain calls it between its writes (`core/bulk-assert-facts!`).
(closed-extent-antecedents kb antes)rules/closed-extent-antecedents over this KB's taxonomy: the negative antecedents
the join withholds and derive time decides.
`rules/closed-extent-antecedents` over this KB's taxonomy: the negative antecedents the join withholds and derive time decides.
(closed-extent-blocks? kb ce-antes bindings pctx)Is a firing blocked because one of its withheld negative antecedents ce-antes does
not hold under bindings in pctx, asked as the whole level-6 question (docs/naf.md,
"Under the grant, a negative antecedent is NAF")?
Is a firing blocked because one of its withheld negative antecedents `ce-antes` does not hold under `bindings` in `pctx`, asked as the whole level-6 question (docs/naf.md, "Under the grant, a negative antecedent is NAF")?
The informant a correspondence derivation of a fact is justified under.
The informant a correspondence derivation of a fact is justified under.
(declaration-reach kb s c)The facts whose nogoods' verdicts and whose readings the forced-monotonic declaration
s stated in c moves, or nil when s declares no predicate outside the baseline set
(decide/global?): the stored facts of its predicate, and the stored denials of them a
negation pair holds, stated in a context that a context at or below c sees
(tax/contexts-seen-with-global). The closures are unscoped: a placement reads the
network, a superset over every reader (decide/unscoped-closures).
The facts whose nogoods' verdicts and whose readings the forced-monotonic declaration `s` stated in `c` moves, or nil when `s` declares no predicate outside the baseline set (`decide/global?`): the stored facts of its predicate, and the stored denials of them a negation pair holds, stated in a context that a context at or below `c` sees (`tax/contexts-seen-with-global`). The closures are unscoped: a placement reads the network, a superset over every reader (`decide/unscoped-closures`).
The bounds a chaining run takes when opts names none. :max-term-depth is the
termination bound for term-building recursion: a firing whose conclusion nests terms
deeper than it, and deeper than every term the firing rests on, is not placed
(term-cut?). :max-derivations, a cap on the conclusions and minted writes one run
makes, and :max-depth, a bound on derivation depth, have no default
(docs/inference.md, "Forward chaining").
The bounds a chaining run takes when `opts` names none. `:max-term-depth` is the termination bound for term-building recursion: a firing whose conclusion nests terms deeper than it, and deeper than every term the firing rests on, is not placed (`term-cut?`). `:max-derivations`, a cap on the conclusions and minted writes one run makes, and `:max-depth`, a bound on derivation depth, have no default (docs/inference.md, "Forward chaining").
(different-blocks? kb different-antes bindings pctx)Is a firing placed in pctx blocked because one of its (different …) antecedents
does not hold there under the settled bindings? Block-if-any, as an unknown
is. The join withholds a different literal (join-order) and refusal-reason asks
this at each placement, so a merge pctx cannot see blocks nothing here; a reader below
pctx that sees one reads a guard defeat instead (different-guard-placements,
docs/predall.md, "A different guard is re-checked, not supported").
Is a firing placed in `pctx` blocked because one of its `(different …)` antecedents does not hold there under the settled `bindings`? Block-if-**any**, as an `unknown` is. The join withholds a `different` literal (`join-order`) and `refusal-reason` asks this at each placement, so a merge `pctx` cannot see blocks nothing here; a reader below `pctx` that sees one reads a guard defeat instead (`different-guard-placements`, docs/predall.md, "A `different` guard is re-checked, not supported").
(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? True only while a calculus it joins on is unsatisfiable
somewhere (qkb/unsatisfiable-somewhere?).
Can `entailment-withdrawn?` answer true for any firing of the rule `rsx`, whatever context it was placed in? True only while a calculus it joins on is unsatisfiable somewhere (`qkb/unsatisfiable-somewhere?`).
(exception-holds? kb except bindings pctx)Does except, a rule's exception as a vector of literals, hold under bindings,
evaluated in pctx, the context the conclusion would be placed in? An empty exception
never holds, and an unanswerable one does not hold. provers/exception-holds? answers,
which the backward chainers call with the query's context.
Does `except`, a rule's exception as a vector of literals, hold under `bindings`, evaluated in `pctx`, the context the conclusion would be placed in? An empty exception never holds, and an unanswerable one does not hold. `provers/exception-holds?` answers, which the backward chainers call with the query's context.
The informant of every justification a guard defeat stores (place-guard-defeats!).
The informant of every justification a guard defeat stores (`place-guard-defeats!`).
(interrupted! bound)(interrupted! bound cause)Throw the refusal a run ends with when bound ended it: the caller's :max-ms,
:stop?, :max-derivations or :on-progress (whose throw is cause), or :heap, an
old generation the memory guard read as nearly full (caches/heap-critical?).
Throw the refusal a run ends with when `bound` ended it: the caller's `:max-ms`, `:stop?`, `:max-derivations` or `:on-progress` (whose throw is `cause`), or `:heap`, an old generation the memory guard read as nearly full (`caches/heap-critical?`).
(justification-excepted? kb j)Is justification j currently blocked — by a visibility except hiding one of its
antecedents, by a lazy-forward rule it rests on that no join reads or that it reads as
its own converse (lazy-firing-blocked?), 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, by a lazy-forward rule it rests on that no join reads or that it reads as its own converse (`lazy-firing-blocked?`), 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. Past it the rule's record collapses to :overflow and a queued overflowed
rule forces a productive settle pass and a re-join over its extent (docs/exceptions.md).
How many refused firings one rule's record keeps before it stops keeping them individually. Past it the rule's record collapses to `:overflow` and a queued overflowed rule forces a productive settle pass and a re-join over its extent (docs/exceptions.md).
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)(place-guard-defeats! kb firings drop?)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 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? keeps none. A change posts F's re-check (special/recheck-defeat-target). Returns
the conclusions whose guard defeats moved. With drop? false (a settle that sweeps
nothing, core/preview's) no justification is dropped, so a suspended blocker takes its
defeat OUT and the rollback finds the records it left. 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 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?` keeps none. A change posts F's re-check (`special/recheck-defeat-target`). Returns the conclusions whose guard defeats moved. With `drop?` false (a settle that sweeps nothing, `core/preview`'s) no justification is dropped, so a suspended blocker takes its defeat OUT and the rollback finds the records it left. See docs/naf.md.
(place-inherited! kb region {:keys [reach first?]})Find the inherited clashes (discovery/discover-inherited!) and place each at its
vantages, the most general contexts that read it whole, justified by its members and the
genlCx edges each vantage sees them over; 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 unless a member is among the facts a
moved forced-monotonic declaration reaches (declared-reach). moves is the pass's
genlCx moves (special/drain-context-moves!). See docs/nmtms.md, "A recover places
the nogoods its store does not hold".
Find the inherited clashes (`discovery/discover-inherited!`) and place each at its vantages, the most general contexts that read it whole, justified by its members and the `genlCx` edges each vantage sees them over; 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 unless a member is among the facts a moved forced-monotonic declaration reaches (`declared-reach`). `moves` is the pass's `genlCx` moves (`special/drain-context-moves!`). See 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 they are stated in and where no except hides one
(res/exception-aware-placements), each justified by the members, the grounds and the
genlCx edges the placement sees them over (visibility-support; place-justified!).
Returns the handles it created. The caller states the nogood: every member IN. within
restricts the comparison (special/drain-context-moves!' :reach). See docs/nmtms.md.
Place the nogood over the handles `members`, detected with the handles `grounds`, at each maximal context that sees the contexts they are stated in and where no except hides one (`res/exception-aware-placements`), each justified by the members, the grounds and the `genlCx` edges the placement sees them over (`visibility-support`; `place-justified!`). Returns the handles it created. The caller states the nogood: every member IN. `within` restricts the comparison (`special/drain-context-moves!`' `:reach`). See docs/nmtms.md.
(place-nogoods! kb region read {:keys [reach first?]})Place, once a settle pass, the nogoods of the families placed as conclusions whose
placement can have moved since the last call: {:made [h …] :minted [h …] :released [h …]}.
:made holds the handles created (place-negations!, place-memberships!,
place-related!, place-tuples!, after the arity family's refresh arity/drain!,
sync-arity-pairs!); :minted the chaining seeds of the mints a type's length admitting one
again owes (special/mints-on-lengths); :released the handles the argument-hold and arity
refreshes took out of :out, for the settle to re-chain (jtms/revived). Every family
detects over the network's IN label (jtms/network-in?). Each family reads what its
write-time index queued, the handles among region (a delay) that read (a volatile set)
does not hold yet, the handles an except of which moved and what rests on them, and what
the pass's genlCx moves reach (moves' :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: `{:made [h …] :minted [h …] :released [h …]}`.
`:made` holds the handles created (`place-negations!`, `place-memberships!`,
`place-related!`, `place-tuples!`, after the arity family's refresh `arity/drain!`,
`sync-arity-pairs!`); `:minted` the chaining seeds of the mints a type's length admitting one
again owes (`special/mints-on-lengths`); `:released` the handles the argument-hold and arity
refreshes took out of `:out`, for the settle to re-chain (`jtms/revived`). Every family
detects over the network's IN label (`jtms/network-in?`). Each family reads what its
write-time index queued, the handles among `region` (a delay) that `read` (a volatile set)
does not hold yet, the handles an except of which moved and what rests on them, and what
the pass's `genlCx` moves reach (`moves`' `: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!), or does the arity or the argument family
owe a refresh (arity/moved?, argument/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!`), or does the arity or the argument family owe a refresh (`arity/moved?`, `argument/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 or different in pctx, any other literal in the
wildcard. Nil is a block: a literal has no answer, its bound output no longer matches
the recomputed value, or its solutions disagree (also filed as :post-join-ambiguous).
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 or `different` in `pctx`, any other literal in the wildcard. Nil is a block: a literal has no answer, its bound output no longer matches the recomputed value, or its solutions disagree (also filed as `:post-join-ambiguous`). At most two solutions are realized (docs/aggregate.md, "Comparing the count").
(reconcile-corresponded! kb fns)Bring the rules a genlCx move can re-spell through a correspondence of each function
of fns (special/note-moved-correspondences!) to the declarations their contexts and
the contexts below them see, and return the handles that are new content: the rules the
:held forced set holds that apply the function, and the rules a correspondence of it
respelled (nat/corresponded-rules). Linear in those rules and the :held set; reads
no fact and no constant (docs/nat.md, The corresponding predicate).
Bring the rules a `genlCx` move can re-spell through a correspondence of each function of `fns` (`special/note-moved-correspondences!`) to the declarations their contexts and the contexts below them see, and return the handles that are new content: the rules the `:held` forced set holds that apply the function, and the rules a correspondence of it respelled (`nat/corresponded-rules`). Linear in those rules and the `:held` set; reads no fact and no constant (docs/nat.md, The corresponding predicate).
(reconcile-formula-positions! kb preds)Bring the stored rules whose hold a formula position of one of preds decides
(nat/formula-position-rules) to the spelling and the hold the declarations believed
now read (reconcile-reified-row! with redecide?), and return the handles that are
new content, for the agenda, or nil when no such rule is stored (docs/nat.md, The
corresponding predicate). Linear in the rules on preds.
Bring the stored rules whose hold a `formula` position of one of `preds` decides (`nat/formula-position-rules`) to the spelling and the hold the declarations believed now read (`reconcile-reified-row!` with `redecide?`), and return the handles that are new content, for the agenda, or nil when no such rule is stored (docs/nat.md, The corresponding predicate). Linear in the rules on `preds`.
(reconcile-reified! kb fns)(reconcile-reified! kb fns preds)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 (docs/nat.md, A reifiable mark moving). The region of each
function also holds the rules a correspondence of it respelled
(nat/corresponded-rules), over the predicates of its stored declarations and
preds, the predicates of declarations that left. Linear in the regions read.
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 (docs/nat.md, A reifiable mark moving). The region of each function also holds the rules a correspondence of it respelled (`nat/corresponded-rules`), over the predicates of its stored declarations and `preds`, the predicates of declarations that left. Linear in the regions read.
(reconcile-spellings! kb preds)(reconcile-spellings! kb preds rows)Bring the stored rows of every predicate in preds (integrate/rows-spelled-by) — 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` (`integrate/rows-spelled-by`) — 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.
(reconcile-stranded! kb maps)Re-spell the stored uses departed natFormula maps left naming their object constants
(nat/stranded-uses), maps holding the departed [k E] pairs. Each use is planned
from its sentence with every constant expanded and each departed k written E
(nat/written-as), so the write path's walk spells it again. Returns the handles that
are new content, or nil when no map left a use behind (docs/nat.md, A reifiable mark
moving).
Re-spell the stored uses departed `natFormula` maps left naming their object constants (`nat/stranded-uses`), `maps` holding the departed `[k E]` pairs. Each use is planned from its sentence with every constant expanded and each departed `k` written `E` (`nat/written-as`), so the write path's walk spells it again. Returns the handles that are new content, or nil when no map left a use behind (docs/nat.md, A reifiable mark moving).
(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, so the trigger that lifts the block
releases it from its bindings (release-refusal!). :handles is every antecedent but the
rule. Records nothing for a firing whose rule does not forward-chain (refusal-state
reads that entry as :dead), whose antecedent an except hides, or whose post-join
literal no longer answers. Runs before the sweep deletes the conclusion's record.
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, so the trigger that lifts the block releases it from its bindings (`release-refusal!`). `:handles` is every antecedent but the rule. Records nothing for a firing whose rule does not forward-chain (`refusal-state` reads that entry as `:dead`), whose antecedent an `except` hides, or whose post-join literal no longer answers. Runs before the sweep deletes the conclusion's record.
(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. The judgement is
rule-firing-blocked? plus the visibility except check. Bindings are settled to the
representatives pctx now elects first (settled-bindings).
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. The judgement is `rule-firing-blocked?` plus the visibility `except` check. Bindings are settled to the representatives `pctx` now elects first (`settled-bindings`).
(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 created, for the
caller to put back on the agenda. Calls place-conclusion with the recorded bindings and
never a fresh join, so k refusals cost k placements. The depth is recomputed from the
antecedent facts. Re-decided here, since the sweep runs between the caller's scan and
this call.
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 created, for the caller to put back on the agenda. Calls `place-conclusion` with the recorded bindings and never a fresh join, so k refusals cost k placements. The depth is recomputed from the antecedent facts. Re-decided here, since the sweep runs between the caller's scan and this call.
(rerecord-refusals! kb)Rebuild the refusal record by re-firing every believed forward rule that carries a
re-checkable block condition (reads/watched-rules). Returns the chain result, or nil for a
KB where no rule carries one. A closed-extent negative antecedent that does not hold
re-records its refusal; an exceptWhen or unknown that holds records nothing (the firing
is placed with its guard defeat). recover's half of the record: a refused firing left
no justification, so the stored justifications cannot restore it and re-firing re-decides
it. Runs after the settle that establishes belief, since a refusal is a claim about it. ! because it discards the record it replaces. Re-fires under
the default bounds, so rebuilt entries record no derivation-depth bound; docs/exceptions.md
states the one case this differs from the live session.
Rebuild the refusal record by re-firing every believed forward rule that carries a re-checkable block condition (`reads/watched-rules`). Returns the chain result, or nil for a KB where no rule carries one. A closed-extent negative antecedent that does not hold re-records its refusal; an `exceptWhen` or `unknown` that holds records nothing (the firing is placed with its guard defeat). `recover`'s half of the record: a refused firing left no justification, so the stored justifications cannot restore it and re-firing re-decides it. Runs after the settle that establishes belief, since a refusal is a claim about it. `!` because it discards the record it replaces. Re-fires under the default bounds, so rebuilt entries record no derivation-depth bound; docs/exceptions.md states the one case this differs from the live session.
jtms/respell-informant, the informant ensure-respellings! justifies a spelling by.
`jtms/respell-informant`, the informant `ensure-respellings!` justifies a spelling by.
(resync-arity-classes! kb)Sync the class memberships of every stored membership of a type below an exact-arity
class (sync-arity-classes!), chain from the new ones, and answer whether one was
placed. recover's half of the derivation: a store written with no belief holds no
justification under arity-class-informant, and its closing settle replays only the
stored ones.
Sync the class memberships of every stored membership of a type below an exact-arity class (`sync-arity-classes!`), chain from the new ones, and answer whether one was placed. `recover`'s half of the derivation: a store written with no belief holds no justification under `arity-class-informant`, and its closing settle replays only the stored ones.
(rule-fields-of kb handle rsx)The fields the chainer reads of a rule sentex. :strength is the justification class
its firings confer (provers/firing-strength).
The fields the chainer reads of a rule sentex. `:strength` is the justification class its firings confer (`provers/firing-strength`).
(rule-firing-report kb)Per forward rule in the KB: how many firings it placed, how many it refused and why, or
whether it did nothing (docs/web.md). Rules come off the antecedent keys
(:rule-antecedents) and the rule index, so the cost is O(rules); the counts come from
jtms/dependents and the refusal ledger (refusals, refusal-state). Each row is {:rule :sentence :believed? :placed :void :refused :refusals :status}. :void counts firings the
forced-monotonic set holds void; :placed those neither void nor concluding a sentex the
argument hold keeps OUT (argument/held?); :refused is :overflow or the entry count.
:refusals is one map per recorded refusal (:state, :reason, :conseq, :context), then
one :blocked map with reason :constraint per conclusion the argument hold keeps OUT, or
nil. :status is :fires, :blocked or :silent. A conclusion dropped for a violation
is in violations, not here.
Per forward rule in the KB: how many firings it placed, how many it refused and why, or
whether it did nothing (docs/web.md). Rules come off the antecedent keys
(`:rule-antecedents`) and the rule index, so the cost is O(rules); the counts come from
`jtms/dependents` and the refusal ledger (`refusals`, `refusal-state`). Each row is `{:rule
:sentence :believed? :placed :void :refused :refusals :status}`. `:void` counts firings the
forced-monotonic set holds void; `:placed` those neither void nor concluding a sentex the
argument hold keeps OUT (`argument/held?`); `:refused` is `:overflow` or the entry count.
`:refusals` is one map per recorded refusal (`:state`, `:reason`, `:conseq`, `:context`), then
one `:blocked` map with reason `:constraint` per conclusion the argument hold keeps OUT, or
nil. `:status` is `:fires`, `:blocked` or `:silent`. A conclusion dropped for a violation
is in `violations`, not here.(run-batch-rejoins kb owed)Run the re-joins owed (*batch-rejoins*' map) stands for in one chaining run, each
as run-owed-rejoin runs a marker. Nil when owed is nil or empty.
Run the re-joins `owed` (`*batch-rejoins*`' map) stands for in one chaining run, each as `run-owed-rejoin` runs a marker. Nil when `owed` is nil or empty.
(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.
(stop-reached?)Has the bound in force (*stop*) been reached?
Has the bound in force (`*stop*`) been reached?
(sync-arity-classes! kb hs)(sync-arity-classes! kb hs defer?)Bring the class memberships the stored memberships hs derive in step with the genl
edges as they stand, as {:new [handle …] :violations [v]}. A :monotonic membership
(T x) derives (C x) for each class arity/class-paths gives over the edges IN at
:monotonic, justified by the membership and that path's edges (place-arity-class!). A
justification under arity-class-informant that the edges no longer give is dropped. With
defer? nothing is dropped and a membership owing a drop is queued (arity/note-class!).
Bring the class memberships the stored memberships `hs` derive in step with the `genl`
edges as they stand, as `{:new [handle …] :violations [v]}`. A `:monotonic` membership
`(T x)` derives `(C x)` for each class `arity/class-paths` gives over the edges IN at
`:monotonic`, justified by the membership and that path's edges (`place-arity-class!`). A
justification under `arity-class-informant` that the edges no longer give is dropped. With
`defer?` nothing is dropped and a membership owing a drop is queued (`arity/note-class!`).(sync-held-respellings! kb)Store the spellings each rule in the :held forced set reads at the contexts it meets a
correspondence declaration in (sync-rule-respellings!), and answer the rows it
created: recover's pass, for a store written before a held rule stored them. Linear
in the :held set; one functor count on a KB declaring no correspondence.
Store the spellings each rule in the `:held` forced set reads at the contexts it meets a correspondence declaration in (`sync-rule-respellings!`), and answer the rows it created: `recover`'s pass, for a store written before a held rule stored them. Linear in the `:held` set; one functor count on a KB declaring no correspondence.
(sync-rule-respellings! kb h)(sync-rule-respellings! kb h on-stale)Store every other spelling that rule row h's written spellings read through the
believed correspondences, each justified respell by h and the declarations it reads
at the contexts that see both (correspondence-want, docs/nat.md, The corresponding
predicate), and drop the ones no longer read. A row recording no written spelling and
holding no open application (nat/held-application?) is left alone. Returns the rows
it created, for the agenda. on-stale is sync-respellings!'s.
Store every other spelling that rule row `h`'s written spellings read through the believed correspondences, each justified `respell` by `h` and the declarations it reads at the contexts that see both (`correspondence-want`, docs/nat.md, The corresponding predicate), and drop the ones no longer read. A row recording no written spelling and holding no open application (`nat/held-application?`) is left alone. Returns the rows it created, for the agenda. `on-stale` is `sync-respellings!`'s.
(sync-values! kb ks fns fact-fns)(sync-values! kb ks fns fact-fns deferred)Bring the correspondence derivations of the constants ks, of every constant minted
for a function of fns, and of the constants of a function of fact-fns a stored
fact names a value of, to what the declarations, the facts and the uses stored now
owe (sync-value!, docs/nat.md, The corresponding predicate), and return the handles
that are new content, for the agenda. The constants of fact-fns are read off the
smaller side, the function's constants or its predicates' facts. With deferred, a
volatile set, nothing is dropped, and each constant owing a drop is added to it. Linear
in the uses of the constants it reads.
Bring the correspondence derivations of the constants `ks`, of every constant minted for a function of `fns`, and of the constants of a function of `fact-fns` a stored fact names a value of, to what the declarations, the facts and the uses stored now owe (`sync-value!`, docs/nat.md, The corresponding predicate), and return the handles that are new content, for the agenda. The constants of `fact-fns` are read off the smaller side, the function's constants or its predicates' facts. With `deferred`, a volatile set, nothing is dropped, and each constant owing a drop is added to it. Linear in the uses of the constants it reads.
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 |