vaelii.core — com.vaelii/vaelii 0.31.0

Vaelii — a contextualized common-sense knowledge base.

A KB bundles a record store (the durable ground truth), an index store (derived from it, rebuildable), a JTMS, and a taxonomy (cached genl / genlCx closures). The unit of knowledge is a sentex: a sentence plus the context it holds in. Rules are sentexes too.

Public API: open-kb, assert, assert-rule, forward-chain, query, sentexes-matching, ask, prove, retract!, why, in?, isa?. This is a signpost, not the full list — docs/api.md is that, and its "Choosing a query function" table is what separates the five ways to answer a goal.

This namespace is the engine's whole API; the engine itself lives in layered vaelii.impl.* namespaces (kb <- checks <- special <- integrate <- chain <- settle) and everything here is either a delegation into that stack or the assert / retract! / recover orchestration that spans it.

Five entry points are public beside it, each a thin shim over the same stack: vaelii.client (the network client), vaelii.starter (the bundled ontology), and vaelii.web / vaelii.serve / vaelii.cli (the browser, the daemon, the command line). Those six namespaces are the compatibility boundary — everything under vaelii.impl.* is free to change without notice.

*bulk-load?* clj

When true, assert runs in bulk-load mode for a caller-guaranteed well-formed, pairwise distinct premise load. assert-one skips the definitional checks, the find-sentex-handle dedup walk and provenance recording; no argument-type entailment is drawn (record-arg-types records them afterwards). A refusal or a bound the caller set still throws and rolls back (undoing-refusal). with-deferred-settle and {:chain? false} complete the fast path; bulk-assert-facts! does all three.

*clock* clj

A 0-arg fn returning the :created time assert records (epoch milliseconds by default). Bind it in tests to fix the value; belief never reads provenance, so a wall-clock default does not touch order independence.

*creator* clj

The creator assert records in a sentex's provenance when opts carries no :creator. nil by default; bind it per session / import / user.

*query-engine* clj

Which backward executor prove and prove-within run:

:dfs the goal-stack DFS (res/prove-from), the default :inference the node engine (vaelii.impl.inference) :hybrid the node engine, except at :max-depth 0, where no node is expanded past the root and the session would be overhead

:inference needs a caller-chosen depth (*query-options* :max-depth, or inference/*max-depth*). Bind it around the consumption: a binding frame popped before the lazy seq is realized leaves :dfs deciding.

*query-options* clj

How the node engine searches, when *query-engine* routes a query to it; the DFS ignores it.

{:strategy :depth-first} a tactician, or a strategy map (vaelii.impl.tactics) {:portfolio? true} race several orderings and union their answers {:auto? true} pick one from the structure of the query

nil, the default, is the shipped ordering. :portfolio? and :auto? reach only prove. Bind it around the consumption (docs/inference.md).

*write-unrecovered?* clj

When true, accepts writes into a KB opened over a store whose derived state was never built ({:recover? false} or :warn over a populated store, or an import-dump with :belief? false / :stored). False by default, which refuses them (:unrecovered-kb); the repair is recover, or reindex when the index is derived. Binding it accepts unchecked, possibly mis-keyed and duplicated writes (docs/storage.md, "Why a write into an unrecovered KB is refused"). :unrecovered-premise and :stale-belief refuse whatever this says. *bulk-load?* is a different switch.

-main clj

(-main & _)

lein run — open a KB on the configured stores, say which ones answered, and exit. A smoke test for the build rather than a way to use the engine: nothing is loaded and nothing is served, so the process ends where it started. lein browser is the one to work in, lein cli runs a single command, and lein run -m vaelii.web serves the browser (docs/operations.md).

abduce clj

(abduce kb goal)

(abduce kb goal context)

(abduce kb goal context opts)

What would have to be true for goal to be provable in context.

Runs prove's backward search and hypothesizes the dead-ended subgoals a (abducible_predicate P) grant visible from context allows, each as a :default premise in a scratch context below context. Answers

{:solutions   [binding-map …]     `prove`'s, unprojected, under the hypotheses
 :hypotheses  [{:sentence :context :handle} …]   irredundant; empty = proved outright
 :refused     [sentence …]        dead ends not assumed, when none proved
 :context     CxAbductionX
 :status      :complete | :capped}

opts: :max-hypotheses (default 8), :max-depth (8), :keep? (the scratch context stands until abduce-discard!; otherwise every :handle is nil). Refusals: :unknown-option, :shape, :not-ground (a variable context), :too-many-kept. docs/abduction.md.

abduce-discard! clj

(abduce-discard! kb result)

Discard an abduction's scratch context — every hypothesis in it, and everything they licensed. Takes the result of a {:keep? true} abduce (or the context symbol itself) and answers {:removed-sentexes n :removed-justifications n}. Idempotent, and unnecessary after a plain abduce, which discards on its own way out.

add-evaluatable clj

(add-evaluatable kb pred f)

(add-evaluatable kb pred f opts)

Register a plain Clojure fn f as the evaluatable predicate/function pred on kb. Two shapes, chosen by opts:

• a check predicate: (add-evaluatable kb 'evenSum (fn [a b] (even? (+ a b)))) makes (evenSum 2 4) hold; every argument must be ground;
• a result-binding function: (add-evaluatable kb 'sumOf + {:result :first}) binds (sumOf ?r 2 3) to ?r = 5; the :result slot is a variable to bind or a value to check, and the rest are the ground inputs f receives.

opts is provers/evaluatable's: :result, :arity, :cost and :completeness (defaults :lookup, 100); another key is refused (:unknown-option). Returns kb.

add-provenance clj

(add-provenance kb handle m)

Merge m into handle's provenance map (creating it if absent), returning the merged map. For application bookkeeping (source, confidence, review state) beside the creation record; :creator / :created change only when m names them. A nil handle records nothing and returns nil. A non-handle, a vector of handles included, is refused (:bad-handle). An unrecovered KB accepts it.

add-prover clj

(add-prover kb prover)

Register an additional prover on kb: a value prover builds, or a record implementing vaelii.impl.types.prover/Prover.

add-reasoner clj

(add-reasoner kb & names)

Register one or more shipped reasoners on kb by name, returning kb.

(doto (open-kb {}) (add-reasoner :allen :rcc8))

Registration is per-KB and idempotent per name (docs/qcn.md). A bad name in the list registers none of it, and neither does a calculus that answers the goal predicate of a standing watch (:not-watchable). A later open-kb names the same set in :reasoners or passes :reasoners :stored; any other set is refused (:reasoner-mismatch; docs/storage.md, "The reasoner set").

agent-of-context clj

(agent-of-context ctx)

The agent an agent context belongs to — CxAgentAlice ↦ Alice — or nil when ctx is not an agent context. The inverse of context-of-agent.

all-functional-at-instant-violations clj

(all-functional-at-instant-violations kb context)

Audit every (functional_at_instant f) declaration visible in context, and return {f #{violation…} …} — declarations that clash nowhere are omitted, so an empty map is a clean sweep.

all-specified-violations clj

(all-specified-violations kb context)

Audit every binary predAllSpecified and predSpecifiedAll declaration visible in context, and every Exists declaration (exists-violations, keyed [functor pred a b]), and return {[functor pred indep] result…}, each result {:status :audited :violations #{…}} or a {:status :gap …} diagnostic (:missing-slot-typing, or :legacy-ternary-declaration for a stored pre-migration ternary sentex, keyed by its whole argument tuple). Declarations that hold are omitted and gaps never are, so an empty map is a clean sweep. kb-integrity consumes the same per-declaration audit stream.

arg-types-owed clj

(arg-types-owed kb)

What the argument-type pass still owes over kb, or nil when nothing: {:facts :total :swept? :deferred} — the facts drawn and counted at its last commit, whether its sweep over the declared functors has ended, and the facts set aside, each {:fact :functor :reason :phase :budget-ms :ms}. A removal from the records of a KB without belief (edit-records!) makes the whole pass owed; record-arg-types and a record-arg-types! run that completes leave nothing owed.

argue clj

(argue kb asent context)

(argue kb asent context opts)

Four-valued epistemic status of a ground assertion. Queries both asent and its explicit negation (not asent) and returns a map:

{:verdict     :true | :false | :unknown | :contradiction
 :for         <results for asent, when provable>
 :against     <results for (not asent), when provable>
 :for-why     <`why`'s graph for asent, when stored and believed>
 :against-why <`why`'s graph for (not asent), when stored and believed>
 :for-derivation     <the search's proof tree, or below a positive depth one leaf>
 :against-derivation <the same, for (not asent)>
 :defeated-by <the `:defeat` reports, `conflicts`' shape, of the placed nogoods
              that defeat a stored asent at context>}

A side carries at most one of :for-why and :for-derivation, and a derivation leaf a SupportingProver answered names the sentexes it was read from (:supports). Without opts it uses ask; pass {:max-depth N} for rules to fire. opts is query-opt-keys; another key is refused (:unknown-option). When both sides are provable the verdict is :contradiction unless a :monotonic justification beats a :default one (docs/nmtms.md, "Observation beats expectation").

ask clj

(ask kb goal)

(ask kb goal context)

(ask kb goal context opts)

Answer goal in context with the pluggable prover engine: stored facts, taxonomy closures, disjointness, predicate metadata, evaluables, NAF, argument-type inference and any prover the application added. Returns solution binding maps projected to the goal's variables.

No rule expansion: a set/backwardRule's conclusion is not seen; use query with a :max-depth, or prove. An (ist Ctx S) goal asks S in Ctx. One sentence: a vector is refused (:shape). opts is {:max-ms n} (ask-opt-keys); reaching it is :budget-exhausted, not a prefix. ask-within hands the prefix back.

ask-opt-keys clj

Every key ask / ask? reads — the wall clock, and nothing else.

:max-depth is not on it, and its absence is the entry point saying what it is: nothing in the prover registry expands a rule, so there is no transformation depth to bound and a :max-depth here would be a bound accepted and never consulted. Bounding which provers run is ask-within's :max-cost (docs/anytime.md). Public for query-opt-keys' reason.

ask-within clj

(ask-within kb goal budget)

(ask-within kb goal context budget)

Anytime ask: answer goal in context, bounded by budget, a map of any of {:max-ms n :max-results n :max-cost <tier>}. Returns the partial-result contract {:results :status :count :elapsed-ms :resume :unenumerated :unenumerated-in-guards} (vaelii.impl.budget): :results are the solutions realized in this step, :status is :complete / :incomplete / :timeout / :capped, and :resume (nil when :complete or :incomplete) continues the same search under a fresh budget via resume. :incomplete is a run that ran dry after a both-open goal over a transitive predicate named in :unenumerated. :max-cost drops every prover whose cost tier is above the ceiling (:lookup < :compute < :search); any other value throws (:unknown-option). docs/anytime.md.

ask? clj

(ask? kb goal)

(ask? kb goal context)

(ask? kb goal context opts)

Is goal answerable via the prover engine? ask's caveats are this one's too — in particular it expands no rule.

opts is ask's wall clock, spent the way provable? spends prove's: the stream is realized only as far as its first solution, and a clock that runs out with nothing found is :budget-exhausted rather than false.

assert clj

(assert kb sentence)

(assert kb sentence context)

(assert kb sentence context opts)

Assert sentence in context (default 'CxUniverse) as a JTMS premise: enforce naming, arg and disjointness constraints, persist, index, mark IN, integrate into the taxonomy and rule index, then forward-chain. A virtual set/forwardRule|backwardRule|inertRule wrapper directs the enclosed rule. (set/monotonic S) around the whole sentence is S asserted {:strength :monotonic}; (set/inert …) and (set/monotonic …) elsewhere than the outermost wrapper are refused (:shape).

opts: chaining options ({:max-depth ..}, {:chain? false}), :strength (:default or :monotonic), :creator, :provenance (a map), and the bounds :max-ms, :stop? and :max-derivations; a bound the run reaches refuses the call (:interrupted).

Returns the sentex handle, or a vector of handles when a rule concluding a conjunction is polycanonicalized into one rule per conjunct. A rebuttal or definitional clash is stored and settled, not thrown. Refusals: an unread opts key or a :strength outside the two (:unknown-option); a vector sentence (:shape); an unrecovered KB (:unrecovered-kb). A refusal leaves the KB as found, the handle counter aside.

assert-inert clj

(assert-inert kb sentence context)

Store sentence in context as an inert sentex: indexed and persisted (so sentexes-in-context shows it and recover keeps it) but not a JTMS premise: never believed, never chained, never scanned for contradictions. Returns the handle. A solve's materialized labeling uses it (docs/solving.md).

Only the shape, naming and groundness invariants are enforced, and a reference resolves as at assert. Refusals: an open sentence (:not-ground); a ground reifiable NAT with no stored constant (:unminted-nat, since this entry point never mints); a rule (:not-indexable); a reference nothing stores (:unresolved-reference); an unrecovered KB (:unrecovered-kb). An (ist Ctx S) stores S in Ctx. Additive, so no !; drop it with retract! on the handle. A new record carries :inert true in its provenance.

assert-many clj

(assert-many kb sentences context)

(assert-many kb sentences context opts)

Assert every sentence in sentences (into one shared context, optional shared opts) with belief settled once at the end: the collection form of with-deferred-settle. Returns the vector of handles in input order (a conjunctive-consequent rule contributes its vector).

:max-ms and :stop? bound the whole call. The sentence a bound interrupts is rolled back, the sentences before it stay settled, and the call throws :interrupted with :stored, their handles (docs/inference.md, Stopping a run).

assert-opt-keys clj

Every key assert / assert-rule reads. Public for the same reason kb/opt-keys is: it is the answer to "is this a real option?", and a caller that can ask does not have to find out from a wrong answer.

:strength is the assumption class, :chain? whether to forward-chain, :direction the programmatic spelling of a set/*Rule wrapper, :creator / :provenance the provenance it records, :max-ms / :stop? the caller's bound on the whole call (chain/call-with-stop); the rest flow to chain/chain-all.

assert-rule clj

(assert-rule kb antecedents consequent)

(assert-rule kb antecedents consequent context)

(assert-rule kb antecedents consequent context opts)

Assert a rule (a sentex whose sentence is an implication) in context. opts may carry :direction (:forward | :backward | :inert | :both, default :backward) — or use a set/*Rule virtual predicate with assert. A generator (a rule concluding a rule) defaults to :forward instead — no backward goal asks for a rule.

assertable-strengths clj

The strengths assert accepts in {:strength s}, as a set: :monotonic and :default. assert refuses any other value against this set, so a form offering a strength control refuses the same values by calling (assertable-strengths s).

belief-status clj

(belief-status kb handle context)

Explain handle's belief and visibility from context as a deterministic map: storage, raw JTMS IN, context-visible exception force, withdrawal from context, assertion-context inheritance, and the terminal answers :believed? / :visible?. :exceptions is in assertion-context and content order; nested meta-exceptions are under :excepted-by. :withdrawn? is true when context reads the handle as withdrawn (why-not names the defeat). Nil and unknown handles report absent storage and raw belief. A malformed handle is refused (:bad-handle).

believed clj

(believed kb handles)

The subset of handles in? answers true for, as a set — in? asked of many handles at once. What the batch form saves is the call, which for a remote client (vaelii.host.serve) is a whole round-trip. A page listing n rows asks once instead of n times.

Handle order does not survive (a set), because belief is a property of each handle and nothing here ranks them; an unknown or torn-down handle is simply absent.

believed? clj

(believed? kb handle context)

Is handle JTMS IN and not withdrawn from context — hidden by the (except ...) cascade visible from it, the target of a placed defeat in force there, or resting only on such a handle (docs/nmtms.md, "A defeat is scoped to its vantage")?

This is contextual belief force only. It deliberately does not require context to inherit the sentex's assertion context; belief-status reports that final visibility condition separately. nil and unknown handles answer false; a non-handle is refused with :bad-handle, exactly as in?.

blocked-justifications clj

(blocked-justifications kb)

The ids of the justifications the network currently holds blocked: a block their rule carries holds (a closed extent, a withdrawn different), so they confer nothing even with every antecedent IN (docs/exceptions.md). The whole set is returned, one read per page of a proof tree, and the same answer behind the daemon. Each settle replaces the set (jtms/set-blocked), so it is the state as of the last one, and it is empty where no rule carries an exception.

bulk-assert-facts! clj

(bulk-assert-facts! kb facts context)

(bulk-assert-facts! kb facts context opts)

Load a large batch of known well-formed, pairwise-distinct ground facts into context on the fast path: assert under *bulk-load?* inside one with-deferred-settle, with {:chain? false}. The caller owns both preconditions; use assert-many when either is in doubt. A symmetric functor keeps the dedup probe.

Returns the vector of sentex handles in input order. No argument-type entailment is drawn: run record-arg-types after the load, and forward-chain for the rules. opts flows to each assert; :max-ms and :stop? bound the call as at assert-many. :on-progress is handed {:phase :loading :done n :elapsed-ms ms :facts-per-sec r} every 100,000 facts and {:phase :done :total n …} after the closing settle. Cost and the changing-snapshot load: docs/storage.md, "What a bulk load costs".

cache-profile clj

(cache-profile)

The cache tuning in force, process-wide: {:scale <multiplier> :overrides {cache-id limit}}. Every count-bounded cache holds its shipped default limit multiplied by :scale, unless :overrides sets it to an absolute number. set-cache-scale and set-cache-limit change it; caches shows the effective limit each cache enforces.

caches clj

(caches kb)

What this process is holding beside the stores: every derived structure the engine caches, ranked by entries. One row apiece:

{:cache :literal-matches :label "Literal matches" :scope :kb :entries 3841 :limit 4096 :unit "literals" :hits 91204 :misses 12038 :hit-rate 0.883 :counters :kb :recompute-ns 4210388811 :retired 0 :compared 0 :spurious 0 :evicted 0 :clearable? true :note "…"}

:scope and :counters are :kb for a cache hanging off this KB and :process for one every KB in the JVM shares. A nil :entries is a cache that cannot be counted from outside; an :error on a row is a cache whose own read threw. clear-caches empties the clearable ones (docs/caches.md).

calculi clj

(calculi)

The shipped qualitative calculi as data — one map apiece, naming the calculus, the base relations it distinguishes (jointly exhaustive and pairwise disjoint, so exactly one holds of any two terms), the identity it puts on the diagonal, and the predicates it claims. The vocabulary each ships is loaded either way; the prover is opt-in.

canonical-sentex clj

(canonical-sentex kb sentence context)

The canonical sentex for sentence in context, without storing it: the un-stored counterpart of sentex, built through the store's own constructor, so it is the form assert would key on (docs/canonicalization.md). Same map shape as sentex (:sentence / :context) with no :id. (canonical-sentex kb S C) digests to the same value on every KB that shares the taxonomy, so it is a content identity independent of a handle. A ground reifiable NAT resolves to its stored constant, never minting, as handle-of does; an unminted NAT stays a compound (docs/nat.md, Read path).

chain-report clj

(chain-report kb)

Per forward rule, what forward chaining did with it: how many firings it placed, how many it refused and why, or whether it did nothing. chain-stats is the run's headline counters; this is the per-rule breakdown, O(rules), off the rule index, the refusal ledger (re-decided against current belief) and the justification graph, so it reflects the KB as it is now. Each row is {:rule :sentence :believed? :placed :void :refused :refusals :status}, :void the firings the forced-monotonic set holds void (vaelii.impl.chain/rule-firing-report). The violations a firing files are read through violations, keyed by the same :rule handle.

chain-stats clj

(chain-stats kb)

Chaining-run instrumentation: {:runs n :last {:derived n :truncated? bool}}.

:last is the most recent run's result whatever triggered it — a plain assert chains too but returns only its handle, so :truncated? here (plus the :warn log) is how a depth- or derivation-capped run becomes visible without calling forward-chain by hand.

check clj

(check kb sentence)

(check kb sentence context)

(check kb sentence context opts)

Would (assert kb sentence context opts) succeed, and if not, why? Returns a vector of problems, empty when the sentence is admissible, and stores nothing. Each problem is a map with the :type assert would have thrown, a :message, and whatever else that check knows. The stages run in assert's order and stop at the first that finds anything; :unrecovered-kb is reported alone and first. check mints no NAT, evaluates no imperative and does not chain, so a refusal raised while rules fire is assert's alone. Stages and differences from assert: docs/api.md, "Validating without writing".

check-edit clj

(check-edit kb batch)

check over a whole edit batch, {:add [[sentence context opts?] …] :remove [handle …]}, storing nothing. Returns a vector of problems, empty when the batch is admissible. Each is what check returns plus :in (:add / :remove), :index and :entry. An :add is checked against the KB as it stands. A :remove is checked for being a handle (:bad-handle), naming a stored one (:unknown-handle) and the teardown-refusal of a handle with no TMS node. :unknown-option and :unrecovered-kb are about the batch and are reported alone.

clear! clj

(clear! kb)

Wipe the KB's durable stores — every record and every index entry, and the argument-type pass's owed record — the backend-agnostic counterpart to recover: recover rebuilds the in-memory JTMS / taxonomy from the stores, this empties the stores. ! because it destroys stored knowledge irreversibly.

It does not reset the in-memory JTMS / taxonomy, so call it on a freshly-opened KB (an empty in-memory state) or immediately before reloading content — the form a reset-and-reload uses. Returns the KB.

clear-caches clj

(clear-caches kb)

(clear-caches kb opts)

Drop every cache that offers a clear, and say what went: {:cleared [{:cache :label :entries}…] :entries total}. Not !: every entry is derived and no belief moves. Scoped to kb.

opts is {:counters? true}, off by default: it zeroes this KB's own tallies (listed under :tallies-reset) and the hit and miss counters of the :process-scoped caches, and the reply carries :counters-reset. caches' :clearable? says which rows this touches, and a :cleared entry carrying :error is one whose clear threw.

clear-violations! clj

(clear-violations! kb)

Empty the accumulated dropped-conclusion ledger. ! because it destroys the diagnostic record — the drops themselves are long final. The :forced-conclusion entries violations reads off the stored firings stay, since they are stored state and not ledger entries.

close! clj

(close! kb)

Release a durable KB's directory: flush and close the record store, drop it from the durability daemon, and release the exclusive file lock. Returns the KB, which must not be used afterwards. clear! destroys the content and leaves the store open; this keeps the content and lets go of the store.

Two KBs opened over one directory share the stores, so closing either closes both. On a fork it releases the fork's own directory, never the base's. On a KB with no directory it releases only RAM, so it is safe in a finally. It also drops the KB's process-registry state (an engine-allocated space, a disk-backed derived index, the matcher's alpha index, the nogood readers' memos) and every listener watch registered on this KB value. An in-memory :space is released by clear!.

common-genls clj

(common-genls kb types)

(common-genls kb types context)

The supertypes every type in types has, a collection of types: the intersection of their genls. Reflexive, as genls is, so a member above all the others is in the set and one type's common genls are its genls. One memoized closure read per distinct type. A set; #{} for an empty types. With a context, only edges visible from it count.

The short arity reads the KB-wide edge set, as genls' does.

common-specs clj

(common-specs kb types)

(common-specs kb types context)

The subtypes every type in types has: the intersection of their specs. Reflexive, as specs is. common-genls, the other direction.

The short arity reads the KB-wide edge set, as genls' does.

compare-tacticians clj

(compare-tacticians kb goal)

(compare-tacticians kb goal context)

(compare-tacticians kb goal context opts)

Run goal in context under several tacticians (the node engine's search orderings), each to completion, and return one row per tactician: the search it ran, its wall-clock :ms, its :status, its :unenumerated and its answer set. The answer sets must be identical; a row that differs is a bug, surfaced.

opts is compare-tacticians-opt-keys: search-tree's depth and bounds, plus :tacticians (the subset to run, inference/default-compare-tacticians otherwise), and not :strategy. Needs a depth as search-tree does.

compare-tacticians-opt-keys clj

Every key compare-tacticians reads: search-tree's two bounds and the depth, plus :tacticians — the subset of orderings to run.

:strategy is not on it. This entry point sets the ordering per row, which is the whole point of running several, so a caller's :strategy would be accepted and discarded — the silent default the key sets exist to refuse. Name the orderings with :tacticians instead. Public for query-opt-keys' reason.

conflicts clj

(conflicts kb)

(conflicts kb opts)

The contradictions the last settle could not satisfy: irreducible clashes among known-true content, two :monotonic beliefs that cannot both hold. Both stay believed. A coexisting pair at :default is a dilemma, and contradictions reports it.

Each entry has contradictions' shape, with the entry's :sentence composing contradicts over the member sentences, in content order. {:grounds? false} leaves :grounds off. {:defeats? true} adds the decided nogoods, in content order, each with :verdict :defeat, :placed-in (the most general placement contexts that decide it), and :loser and :winners ({:handle :sentence :context :defeat-class :rules}). A context below :placed-in does not believe the loser (docs/nmtms.md).

context-down clj

(context-down kb c)

The contexts that inherit from c, reflexively — c plus every context that sees it.

context-of-agent clj

(context-of-agent agent)

The canonical context for agent — Alice ↦ CxAgentAlice. The engine projects an agent's modal beliefs into this context (modal_predicate, docs/belief.md); a coordination layer can reuse it as the agent's write boundary — everything the agent asserts lands in its own context, lifted under a shared one by genlCx. The forward half of a bijection; the inverse is agent-of-context, and the two round-trip.

context-up clj

(context-up kb c)

The contexts c inherits from, reflexively — c plus everything it sees via genlCx. A sentex in any of these is visible from c.

contexts clj

(contexts kb)

Every context currently in the genlCx hierarchy — the nodes of the closure.

contexts-of clj

(contexts-of kb sentence)

The contexts in which sentence is stored and believed — a read through sentexes-matching, so the context of a defeated or unsupported sentex is not listed. handle-of per context answers storage regardless of belief.

contradictions clj

(contradictions kb)

(contradictions kb context)

(contradictions kb context opts)

The coexisting pairs the last settle left standing: represented dilemmas, not failures. Each entry is {:nogood #{h ..} :handles [h ..] :priority int :kind kw-or-nil :sentence (contradicts ..) :sides [{:handle :sentence :context :defeat-class :justifications [...]} ...] :grounds [{:handle :sentence :context} ...]}, plus :inherited for :kind :inherited and :vantages {context handle} where placements defeat different members, in content order. :priority ranks a definitional clash (3 to 4) above a rebuttal (1 to 2), and an inherited clash is a rebuttal. (contradictions kb) reports the KB as a whole; (contradictions kb context) what stands for one reader (a nil or variable context is the KB-wide reading). {:grounds? false} leaves :grounds off. Kinds and scoping: docs/nmtms.md, "The clash reports"; the inherited clash: docs/inherit.md.

count-in-context clj

(count-in-context kb context)

How many sentexes are stored in context — one set-size read, O(1), nothing fetched.

Counts stored-not-believed sentexes too (a defeated default still occupies the context), so this can exceed (count (sentexes-matching kb pattern context)), which filters belief. For the believed count use (count (sentexes-in-context kb context {:believed? true})) — necessarily O(n), since belief lives in the TMS and not in the index.

count-with-arg clj

(count-with-arg kb pos term)

How many fact sentexes hold term at argument position pos, as stored — cheap, one O(1) set-size read per predicate declaring an argument at that slot.

Counts stored-not-believed sentexes too. The believed count is (count (sentexes-with-arg kb pos term {:believed? true})) and is O(n).

count-with-functor clj

(count-with-functor kb pred)

How many fact sentexes with functor pred are stored — one set-size read, O(1).

Counts stored-not-believed sentexes too, so it can exceed (count (sentexes-matching kb (list pred ...) '?ctx)). The believed count is (count (sentexes-with-functor kb pred {:believed? true})) and is O(n).

covers-of clj

(covers-of kb whole)

The believed covering, separating and partition sentexes whose whole is whole, in every context, as a set of [kind parts]: kind is :covering, :separating or :partition, and parts is the declared part vector, deduplicated and sorted by printed name. A rule-concluded cover sentex counts as a stated one does; an intersection declares no part list and adds nothing. One believed argument-root read per functor at position 1, so the cost follows whole's own declarations.

default-chain-opts clj

The bounds a chaining run takes when opts names none: :max-term-depth, the termination bound for term-building recursion, and :max-derivations, the cap on one run's writes. :max-depth has no default (docs/inference.md, "Forward chaining").

default-describe-limit clj

How many entries one of describe's bounded lists carries when the caller names no :limit. The browser's term page lists this many per line, so the default is the page's own number and the page shows exactly what describe answered.

default-nearest-depth clj

How many rule rewrites {:nearest n} searches through when the caller names no :max-depth. Three, because a near miss is a rule whose antecedents are nearly all there, and one that needs four chained rewrites to reach the goal is not near anything a reader is going to fix by asserting one fact. The node engine's termination is the depth bound (docs/inference.md), so this is a real ceiling and not a hint: a rule further down is not reported, and :max-depth is how a caller who knows their KB says so.

default-nearest-ms clj

The wall clock {:nearest n} gives its search when the caller names no :max-ms. Two seconds — long enough for a schema-sized KB to empty its frontier, short enough that a diagnostic called on a large one answers rather than hangs. A run that hits it reports :status :timeout under :nearest-search rather than pretending the frontier emptied.

defeat-class clj

(defeat-class kb handle)

The current defeat-class of a believed handle (:monotonic / :default), or nil when it is OUT — the effective strength of the belief after settling. nil for a nil handle too; a non-handle is refused (:bad-handle).

dependent-justifications clj

(dependent-justifications kb handle)

Justifications that use handle as an antecedent, in content order as supporting-justifications is: what rests on it, as an impact analysis before a retract! asks. A rule handle's dependents are every firing it licensed. Empty for a nil handle; a non-handle is refused (:bad-handle).

deprecated? clj

(deprecated? kb term)

(deprecated? kb term context)

Did a believed rewriteOf name term the dispreferred side? False for a sameAs or equals member: those merge without retiring either name. Scoped by context like representative — a retirement holds where it is visible, so a context outside the rewriteOf's ancestor set is told nothing and keeps the name.

describe clj

(describe kb term)

(describe kb term context)

(describe kb term context opts)

Everything the KB holds about one term, as one map, keyed by the term's own role (term-role; stored content overrides it, described-role). Four shapes carry :term, :role, :context, the KB's :comment strings and the closure lines :genls, :specs and :disjoint. On top of that:

:role	also carries
:predicate	:arity (the exact length that binds it, nil where none binds or two do), :arity-via, :arg-declarations, :props, :inverse, :extent-count, and the grants :closed-extent? :abducible? :modal? :decontextualized?
:type	:predicates-for-type (whose argument declarations admit it) and :instance-count
:individual	:types (asserted, not supertypes) and :predicates with a count each
:context	:up / :down (the genlCx ancestor sets), :sentex-count, :computed-spec-of for a reified NAT

A :predicate and a :type also carry :definitional-block, the handbook/06-definitional-block.md parts as {:part :value} rows, each :missing where the KB holds nothing. Declarations and closures are read from context's genlCx ancestor set; ?ctx, the default, reads every context.

Each list is {:terms|:rows :total :exact? :sorted?}: :exact? is false where :total is a bound, :sorted? false where the list is in closure order. :limit (default-describe-limit) caps a list; describe-opt-keys is the key set. :extent-count and :instance-count are stored counts (count-with-functor's contract), so they can exceed what sentexes-matching answers. props and has-prop? answer the metadata :props leaves out. docs/api.md.

describe-opt-keys clj

Every key describe reads, and the key set a key off it is refused against (:unknown-option): :limit, how many entries one of its bounded lists carries and how many supertypes its predicates-for-type walk probes.

digest clj

(digest kb handle)

(digest kb sentence context)

The content digest of a sentex: "sha256:" and the lowercase hex SHA-256 of its context, sign and canonical sentence (docs/storage.md, "Content digests"). Two KBs holding one sentex compute one digest for it, and a (sentexHandle n) inside the sentence digests as the record n names. (digest kb handle) reads the stored record and answers nil when the handle names none. (digest kb sentence context) canonicalizes through canonical-sentex and needs nothing stored. A sentence holding a value the encoding does not cover (a map, a Date) is refused :not-encodable.

digest? clj

(digest? x)

Is x a content digest string: "sha256:" then 64 lowercase hex characters?

digests clj

(digests kb handles)

(digests kb handles opts)

(mapv #(digest kb %) handles), digesting each record a chain of references names once. {:provenance? true} digests each record's :creator and :created with its identity, so the digest changes when the provenance does.

direct-genls clj

(direct-genls kb t)

(direct-genls kb t context)

The types t is a subtype of by one genl edge in the closure — its direct parents, where genls is everything they reach. Not reflexive. An edge counts whatever installed it: a stated (genl t super), or a covering, separating or partition declaration naming t as a part of super. O(degree). A set; #{} when t is not a node in the type hierarchy. With a context, only edges visible from it count.

The short arity reads the KB-wide edge set, as genls' does.

direct-specs clj

(direct-specs kb t)

(direct-specs kb t context)

The types that are a subtype of t by one genl edge in the closure — its direct children. direct-genls, the other direction.

The short arity reads the KB-wide edge set, as genls' does.

disjoint-metatypes clj

(disjoint-metatypes kb)

The declared disjoint metatypes — each a type whose member types are pairwise disjoint by (disjoint_metatype M). The clique is consulted, not materialized: no (disjoint a b) pair is stored, so to render the induced pairs, take metatype-members of each and pair them yourself.

disjoint? clj

(disjoint? kb a b)

(disjoint? kb a b context)

Are types a and b provably disjoint (via disjoint declarations, closed under genl)? With a context, only declarations and genl edges visible from it count — the vantage every definitional check now judges from.

The 3-arity reads every declaration and edge the taxonomy holds, including one a defeat or an except hides from every reader: the KB-wide reading.

disjointness-audit clj

(disjointness-audit kb)

(disjointness-audit kb context)

The subsumption-status of every unordered pair of distinct types visible from context (default CxWell). Returns {:types n :pairs n :by-status {status count …} :pairs-data [{:a t :b t :status s :statuses ss} …]}. The shared-instance query runs only for a pair the taxonomy and disjoint declarations leave open, facts-only. :unknown pairs are the candidates for a missing disjoint or orthogonal assertion. An entry whose :statuses holds :orthogonal also carries :witness (:declared, :shared-instance, :shared-spec or :unwitnessed-spec) and, for the last three, :via, the instance or subtype found.

edit! clj

(edit! kb batch)

(edit! kb batch opts)

Apply a batch of assertions and retractions in one settle.

add — a seq of [sentence context] (or [sentence context opts]), asserted in order first; remove — a seq of handles, retracted after.

The final state equals running the asserts and retracts singly. All-or-nothing: a refusal check-edit cannot see rolls the batch back at the handles it wrote; the handle counter stays moved. Returns {:added <one entry per add,assert-shaped> :removed {:removed-sentexes n :removed-justifications n}}; edit-with-consequences adds the belief diff. opts takes edit-opt-keys; :max-ms and :stop? bound the adds' chaining, and ending it before the first removal refuses the batch (:interrupted) and rolls it back. docs/api.md, "Contract notes: edit!".

edit-batch-keys clj

Every key an edit batch may carry, read by edit, check-edit, preview and edit-with-consequences alike. Public for the reason assert-opt-keys is: it is the answer to "is this a real key?".

edit-opt-keys clj

Every key edit! and edit-with-consequences! read for the batch as a whole: the caller's bound on the adds' chaining (chain/call-with-stop). An add's own opts are assert's.

edit-records! clj

(edit-records! kb batch)

Apply a batch of premise removals and rule direction changes to the records of a KB without belief, and return what it did. No check, dependency sweep or settle runs; settle-record-edits! settles any number of batches with one rebuild.

:remove — a seq of handles. A record is deleted with its postings, unless a justification the batch leaves standing concludes it, which then only loses its premise mark; :direction — {handle direction}, a rule's new :forward / :backward / :forward-only / :inert / :both.

Justifications resting on a deleted record and firings of a rule taken off :forward are deleted. A removal naming no stored record counts under :absent, so a rerun after a crash completes the batch. Returns {:removed n :unpremised n :absent n :redirected n :justifications-removed n :seeds [h …]}; :seeds names where the settle sweeps from. Refuses, before writing, a KB with belief (:belief-built); an except, defeat or exceptWhen removal (:record-edit-unsupported); and a direction on a handle that is not a stored derive rule or onto or off :lazy-forward (:unknown-option, :unknown-handle). docs/storage.md, "Editing the records of a KB without belief".

edit-with-consequences! clj

(edit-with-consequences! kb batch)

(edit-with-consequences! kb batch opts)

edit, plus what the batch turned out to mean: the belief it added and took away, in preview's entry shapes. Returns edit's {:added :removed} with :believed-added, :believed-removed and :bounded? merged in. The removed half omits what the dependency-directed sweep deleted; preview names it. opts takes :max-results n and edit!'s edit-opt-keys; an unknown key and a cap that is not a positive integer are refused (:unknown-option). docs/preview.md, "The other direction".

equiv-class clj

(equiv-class kb term)

(equiv-class kb term context)

Every term known equal to term, itself included. #{term} when nothing has merged it — an unseen term is its own singleton class. Scoped by context like representative.

escalate clj

(escalate kb goal)

(escalate kb goal context)

(escalate kb goal context floor)

(escalate kb goal context floor opts)

The cheapest level that answers goal: climb from floor and stop at the first level with results. Returns {:level :name :results :tried}, :results that level's lazy seq; nothing answering gives :level nil. :unenumerated is present when the stopping level answered a both-open goal over a transitive predicate from its extent (docs/levels.md). floor defaults to 2 (also for nil). opts is escalate-opt-keys: {:max-ms n}; a climb stopped before any level answered returns {:level nil :status :timeout}.

escalate-opt-keys clj

Every key escalate reads — the wall clock, and nothing else. It is checked between levels and inside level 7's search, and a climb it stops before anything answered says :status :timeout rather than that nothing answers (docs/levels.md). Public for query-opt-keys' reason.

exists-violations clj

(exists-violations kb declaration context)

The audit result for one Exists declaration in context, {:status :audited :violations #{x…}}: for (predAllExists pred indep dep) each member x of indep with no believed (pred x y) whose y is a member of dep; for (predExistsAll pred dep indep) each member x of indep with no believed (pred y x) whose y is a member of dep; for (predExistsInstance pred indep fixed) and (predInstanceExists pred fixed dep) the fixed term when no such tuple bears to it or from it. Any member, an indeterminate_term included, is a filler. Throws :bad-args for any other sentence. Computed on demand and not filed (predall.md).

explain-levels clj

(explain-levels kb goal)

(explain-levels kb goal context)

What every level yields for goal: a seq of {:level :name :count}. The level at which the count first rises is the machinery the answer depends on. Unlike lookup it realizes every level fully. A row carries :unenumerated when its count lacks the closure pairs of a both-open goal over a transitive predicate (docs/levels.md). It explains the retrieval stack, not belief; why / why-not explain belief.

export! clj

(export! kb dir)

(export! kb dir opts)

Write kb out as a portable export dump in dir and return a summary:

{:variant :records :sentexes n :justifications n :provenance n
 :index-entries n :bytes n :elapsed-ms n :dir "…"}

opts: {:variant :records|:records+index :compression :gzip|:xz|:none :chunk-size n :provenance? bool :belief? bool :on-progress f} (defaults :records, :gzip, 10000, true, true). :belief? true also writes the reasoning image. :on-progress is called with {:phase :done :total} at each chunk boundary; a callback that throws cancels, leaving a directory with no meta.edn, which is not loadable. An unread key is refused (:unknown-option). dir must be absent or empty, and no one may be writing kb. ! although it destroys nothing here: it writes outside the process (docs/storage.md).

export-text! clj

(export-text! kb dir)

(export-text! kb dir opts)

Write kb's premises and inert sentexes as a text KB, one <Context>.txt per context, in the format load-text! reads, and return a summary:

{:contexts n :sentences n :skipped n :files ["CxUniverse.txt" …]
 :bytes n :elapsed-ms n :dir "…"}

opts: {:context C} writes that one context's file, {:ancestor-set C} writes C and every context it sees; with neither, every context holding a premise or an inert sentex. {:delta? true} on a fork writes the fork's own writes only and adds :retractions to the summary; on a non-fork it is refused. An unread key is refused (:unknown-option). dir must be absent or empty.

No derived sentex is written. Each premise keeps its :strength (:monotonic as a (set/monotonic S) wrapper), each rule its set/*Rule wrappers and exceptWhen, and an inert sentex is (set/inert S). A KB without belief refuses (:unrecovered-kb) when it stores a sentex that is neither premise nor inert. A handle at a reference position is (ist Cx S), a delta adding its digest; :skipped counts the records with no text. ! although it destroys nothing. docs/kbs.md, docs/overlay.md, "A delta".

exposed-clashes clj

(exposed-clashes kb)

Every disjointness clash the KB currently makes jointly visible: a term holding two types some context can see as disjoint, where each membership was admissible where it was written. Entries are in violations' shape ({:violation :disjoint :detail {:term :held :visible-from :message}}), computed on demand and not filed. settle files none: a pair a reader sees whole is decided there and answered by contradictions or conflicts. Reads only.

filed-violations clj

(filed-violations kb)

The filed ledger alone: the entries violations begins with, in its order, without the :forced-conclusion, :inert-argument and :inert-rule entries it reads off the stored firings and held sentexes. A deref that reads no record, where violations fetches every held sentex and convicted firing from the record store.

find-sentexes clj

(find-sentexes kb term)

Every stored sentex that contains term anywhere (any position, any nesting). Powered by the inverted term index.

find-sentexes-all clj

(find-sentexes-all kb terms)

Every stored sentex that contains all of terms.

find-terms clj

(find-terms kb q)

(find-terms kb q opts)

The vocabulary terms whose name matches q, sorted by name. Cost is the size of the vocabulary.

opts:

:match :prefix (default) | :substring | :regex :case-sensitive? false by default; ignored by :regex (use (?i)) :limit keep the first n of the sorted answer; a non-positive-integer is refused (:unknown-option)

q is a string or symbol, or under :regex a compiled Pattern in-process. An unparsable regex throws; a pattern past its step budget throws :pattern-too-costly.

fork clj

(fork kb)

(fork kb opts)

A private, writable KB over this one's stores (a fork). Reads resolve fork-first and fall through to kb; writes land only in the fork.

opts is the fork's own storage (default {:backend :memory}, dropped by close!; {:backend :disk-log :dir …} is durable). :tms takes the engine default when unnamed; :naming and the registered reasoners inherit from kb. A :columnar index is refused. Mount and remount rules: docs/overlay.md.

forward-chain clj

(forward-chain kb)

(forward-chain kb opts)

Run forward chaining to a fixpoint over every believed sentex, then settle belief. Returns {:derived n :truncated? bool}, with :bound (:max-derivations, :max-ms or :stop?) naming what ended a run kept under :on-stop :keep.

opts: :max-depth, :max-term-depth and :max-derivations bound the run (default-chain-opts); :max-term-depth refusals return :term-cut, their count, and a :max-depth cut returns :truncated? true. :on-progress is called with {:derived n :pending n} every :progress-every-ms and may throw to stop. :max-ms bounds the call and :stop? is a no-argument function whose truthy answer ends it. :on-stop (docs/inference.md, Stopping a run) is :rollback (default: a stopped run throws :interrupted with :bound and leaves the KB as found, the handle counter aside) or :keep (the run keeps what it placed, is settled, and returns :truncated? true). A nearly full heap ends the run with :interrupted :bound :heap under either, except during an oplog replay. An unread opts key is refused (:unknown-option).

functional-at-instant-violations clj

(functional-at-instant-violations kb f context)

The per-instant functionality clashes of one (functional_at_instant f) declaration in context, as a set of maps {:function f :subject s :instant t :values #{v…} :kind k}, one per moment t at which more than one distinct value of the fluent function f holds for one subject s. :kind is :merge when the clashing values are all symbols and :contradiction otherwise. Computed on demand and not filed; the candidate moments are the time_point members ask answers in context (docs/time.md, "Functionality at an instant").

genl? clj

(genl? kb sub super)

(genl? kb sub super context)

Is sub a (reflexive-transitive) subtype of super? Types, not individuals — for an individual's type membership use isa?. With a context, only edges visible from it count.

The short arity reads the KB-wide edge set, as genls' does.

genls clj

(genls kb t)

(genls kb t context)

The supertypes of type t, reflexively — t itself plus everything reachable from it by genl. A set; #{t} when t is not a node in the type hierarchy. With a context, only edges visible from it are walked (docs/taxonomy.md).

The 2-arity reads every edge the taxonomy holds, including one a defeat or an except hides from every reader: the KB-wide reading.

handle-id clj

(handle-id form)

The sentex id a (sentexHandle <id>) term names, or nil when form is not one. The inverse of sentex-handle, so the two round-trip.

handle-of clj

(handle-of kb sentence context)

The handle of the sentex already storing sentence in context, or nil. The non-creating counterpart to ist: it turns a sentence into a handle for retract!, in?, why or supporting-justifications. Storage, not belief: a stored-but-defeated sentex has a handle.

Either spelling of a ground symmetric literal finds the one stored sentex. An (exceptWhen <query> <rule>) answers the exception's meta-sentex handle (docs/exceptions.md); a whole-form (set/monotonic S) answers S's; an (ist Ctx S) is read as ist writes it; a ground reifiable NAT resolves to its stored constant and a reference to its target's handle. A vector, a non-sentence, and a nil, numeric or variable context are refused (:shape), since nil means "not stored".

handles clj

(handles kb)

Every live sentex handle in the KB, premises and forward-derived alike, read off the record store. The whole-KB counterpart to sentexes-in-context and sentexes-matching. Storage, not belief: filter with in? for belief.

A set to read, not one to build on: contains?, count, seq and sort answer it; convert with (set …) before conj / disj / clojure.set, since a large store answers a compressed handle set (vaelii.impl.handle-set).

has-prop? clj

(has-prop? kb kind pred)

(has-prop? kb kind pred context)

Does pred carry the metadata property kind? vaelii.impl.predicates/prop-kinds enumerates the kinds (docs/api.md). A kind outside the list answers false.

With a context, the declaration must be visible from it, except :symmetric, :commutative and the two forced-monotonic kinds (docs/nmtms.md). The 3-arity reads the KB-wide declarations. transitiveInArg is read through matches-visible (docs/inherit.md).

import! clj

(import! kb dir)

(import! kb dir opts)

Read an export dump from dir into the empty kb, the inverse of export!. opts: {:belief? true|:stored|false :report-every n :on-progress f :drop-principal? bool :reasoners :stored :rebase? bool :on-replayed f}. :belief? true (the default) lands the state a restart produces, :stored stores everything and leaves recover for later, false stores and indexes records only. :on-progress is called every :report-every frames (default 500000) with {:phase :done :total}; under :rebase?, :on-replayed with each replayed premise's old record and new handle. Refused: an unread key or value (:unknown-option); another reasoner set (:reasoner-mismatch). A foreign dump needs its reader plugin; one refused for its content leaves kb empty. The summary: docs/api.md, "Reading a dump back".

in? clj

(in? kb handle)

Is the sentex handle believed as the context it is stored in reads it: JTMS IN, and not hidden there by a placed defeat in force there or by resting only on a handle one hides (docs/nmtms.md, "A read with no reader")? Visibility excepts are not applied.

When this answers true but a contextual read cannot see the sentex, call belief-status to inspect the exception condition and the assertion-context inheritance condition.

indexable-terms clj

(indexable-terms sentex)

The distinct terms that make sentex findable — the indexable subterms of its connective-free content (numbers, strings, and variables dropped). These are exactly the keys of the inverted term index this sentex is posted under.

Every name it mentions is here. A ground compound subterm is here when it sits between sentex/*min-indexed-depth* and sentex/max-indexed-compound — outside those bounds find-sentexes still returns this sentex for it, narrowing on the atoms and verifying against the record rather than reading a key.

install-memory-guard! clj

(install-memory-guard! {:keys [kbs] :as opts})

Attach a listener to the JVM's garbage collectors that moves the cache profile's :pressure with how full the old generation is: over the high mark it shrinks the caches, under the low mark it grows them back. Returns nil. :kbs is a thunk answering the live KBs whose per-KB caches the trim reaches. Idempotent: a second call replaces the thunk and attaches no second listener. Nothing attaches the guard at engine load. ! because it attaches to the process's collectors. docs/caches.md

interpreted clj

(interpreted term)

What the engine does with vocabulary term term: {:enforced "where"}, {:inert "why"}, or nil. :enforced means a code path reads the term and the KB refuses, derives or answers differently because of it; the string names the path. :inert means nothing does, and the string says why. Nil means the term is not one core.txt comments, so an ordinary domain predicate is out of scope. vocabulary-audit classifies every declared term.

inverse-of clj

(inverse-of kb pred)

(inverse-of kb pred context)

The predicate declared inverse to pred by an (inverse P Q) sentex, or nil. The relation is stored both ways, so (inverse-of kb Q) answers P. With a context, the declaration must be visible from it.

The 2-arity reads the KB-wide declarations, as disjoint?'s does.

isa? clj

(isa? kb x t)

(isa? kb x t context)

Is individual x (transitively) of type t? Considers only type memberships visible from context (default: any context).

ist clj

(ist kb ctx s)

The ist operation: find or create sentence s in context ctx, returning its handle. (ist ctx s) given to assert does the same — ist is never stored.

justification clj

(justification kb jid)

The justification for an id, or nil — nil in, nil out; a non-id is refused (:bad-handle).

Read from the record store, not the network: a justification is a record, and the network keeps only the part belief is computed from (jtms/graph-just — the firing's variable bindings are not among it).

justification-verdicts clj

(justification-verdicts kb handle context)

The verdict context reads on each justification of handle, as {justification-id reason}: :supports where every handle it rests on is believed there, else :antecedent-out, unless the network blocks it (:blocked, its rule's exceptWhen holds) or holds it void (:void), context's forced-monotonic reading holds it void (:void), a guard defeat in force at context covers it (:guard, docs/naf.md), or it is a nogood justification of a placement context exempts (:exempt). Belief here is why's reading, with the excepts not applied. Empty for a nil handle; a non-handle is refused (:bad-handle).

kb-diff clj

(kb-diff a b)

What two KBs disagree about, as content: {:added :removed :moved :belief-changed}.

Each side is a KB, or a string naming a text KB (a directory of Cx….txt files or one such file), read into an in-RAM KB of its own (load-text!) and closed before this returns. lein cli diff <a> <b> compares two exports.

key	holds
:added	in b and not in a
:removed	in a and not in b
:moved	the same sentence at the same strength, in a different context
:belief-changed	the same sentex on both sides, believed on one and not the other

An :added / :removed row is {:sentence :context :strength :premise? :believed?}, a :belief-changed row carries :believed-in-a / :believed-in-b instead of :believed?, and a :moved row reads {:sentence :from :to :strength :premise?}. Rows are keyed on content, never on a handle, and every list is in content order. Justifications, provenance and handles are not compared. O(|a| + |b|).

kb-integrity clj

(kb-integrity kb candidate-terms context)

(kb-integrity kb candidate-terms context options)

Run the bounded, read-only integrity sweep in context. candidate-terms is a finite set of ground terms (:bad-args otherwise). Answers {:status :audited :candidate-count n} when no pass finds anything, :status :gap with the non-empty finding categories, or :status :truncated with its :reason, the :pass it stopped in and the findings kept. Every answer carries :work and :elapsed-ms. options takes :max-work, :max-ms, :max-results, and :categories, a set of category keys to run; the review-only categories run only when named. Categories: docs/integrity.md. Stores nothing.

kb-quality clj

(kb-quality kb)

(kb-quality kb opts)

Seven readings about the knowledge, one map with the keys :rules, :extents, :chains, :taxonomy, :declarations, :subsumption and :clashes, each a distribution rather than a number (shapes: docs/quality.md, "The result map"). Data, not a printer: quality-report renders it.

opts: :limit caps each listed set (default 25); :on-progress is called with {:phase :done :total} and may throw to cancel; an unknown option is refused (:unknown-option). Extents count what is stored, not what is believed.

last-program clj

(last-program kb)

The last edge Program handed to the solver — the contested assumptions and the nogoods among them — or nil if no tie has ever been arbitrated.

do/labeling records it, and vaelii.impl.asp.label/classify reads it (docs/asp.md, "Two things keep classify from reporting a tie as forced").

levels clj

(levels)

The stack as data: {:level :name :below :adds} per level.

load-foreign! clj

(load-foreign! kb kind path opts)

Load the directory at path into kb through the foreign reader plugin registered for kind (:cyc-corpus, for one), passing opts to it, and return what the reader returns. A build with no plugin for kind, or one whose reader loads no directory, is refused by name (:no-foreign-reader). A foreign dump needs none of this — import! reads one through the same plugin. docs/foreign.md

load-text! clj

(load-text! kb source)

(load-text! kb source opts)

Read a text KB into kb, a directory of Cx….txt files or one such file, and return a summary:

{:contexts n :sentences n :files ["CxUniverse.txt" …] :elapsed-ms n :path "…"}

The inverse of export-text!, and the entry point lein cli load is. The file name is the context, and a sentence for another context says so with (ist Cx S). Forms are read with clojure.edn, so a file never runs code. Every form goes through the ordinary write path, and the KB need not be empty. (set/monotonic S) asserts S known-true and (set/inert S) stores S through assert-inert.

A directory is one order-insensitive pass: a refused form is retried until a round stores nothing more, then re-asserted without the catch so it throws its own error. A reference (ist Cx S) resolves as assert resolves it. A delta's digests are compared with those of the sentexes its references resolve to (:canonical-mismatch). {:merge? true} reads a delta (export-text!'s :delta?) into a KB holding content of its own: a refused form is reported as :refused [{:form :context :type} …], not thrown (docs/overlay.md, "A delta"). ! because it writes knowledge into the KB. docs/kbs.md.

log-level clj

(log-level)

The level the engine's own logging prints at, or nil when the engine has installed no backend — which is the state a process is in until set-log-level is called or VAELII_LOG_LEVEL is set. Nil is not :info: it says the level is whatever taoensso.trove/*log-fn* already holds, which is Trove's console backend at :info unless the host application installed one of its own.

lookup clj

(lookup kb level goal)

(lookup kb level goal context)

Answer goal in context using exactly the machinery of level:

0 :raw handles at an index location 4 :typed + genl spec walk 1 :extent one literal context 5 :closed + transitive closure 2 :local + unification 6 :solved full provers, no rules 3 :visible + genlCx inheritance 7 :proved full stack

A lazy seq of {:level :handle :sentence :context :bindings}; a field the level cannot supply is nil. Levels 0-4 carry the handle of a result read off the store. At level 0 a vector goal is an index path; elsewhere the goal is a sentence. docs/levels.md.

mark-inert! clj

(mark-inert! kb opts)

Write :inert true into the provenance of the unsupported records opts names, and return {:marked n :handles [h …]}. {:handles hs} marks the unsupported records among hs, {:contexts cs} those unsupported reports in a context of cs. With neither, refused (:unsupported-unattested). For an assert-inert record written before assert-inert marked its records: a marked record is no longer counted by unsupported. docs/storage.md.

max-common-specs clj

(max-common-specs kb types)

(max-common-specs kb types context)

The maximal common subtypes of types: the members of common-specs that are no member of types and have no other such member strictly above them. One distinct type gives max-specs of it, exactly. min-common-genls, the other direction, and (maxCommonSpec ?x t1 t2 …) as a query.

The short arity reads the KB-wide edge set, as genls' does.

max-context-children clj

(max-context-children kb c)

The maximal contexts that inherit from context c: the contexts that reach c over one genlCx edge with no other such context strictly above them. min-context-parents, the other direction. Read as context-down reads: while an except reaches a genlCx edge, a context is a member when c is one of its own min-context-parents.

max-specs clj

(max-specs kb t)

(max-specs kb t context)

The maximal subtypes of type t: its direct children (direct-specs) with no other direct child of t strictly above them. min-genls, the other direction. One memoized closure read per direct child, so the cost follows t's own fan-out.

The short arity reads the KB-wide edge set, as genls' does.

metatype-members clj

(metatype-members kb m)

The member types of disjoint metatype m — the set whose every pair disjoint? holds of, closed under genl.

min-common-genls clj

(min-common-genls kb types)

(min-common-genls kb types context)

The minimal common supertypes of types: the members of common-genls that are no member of types and have no other such member strictly below them. Not reflexive: for dog and mammal under dog ⊂ mammal ⊂ animal the set is #{animal}. One distinct type gives min-genls of it. A set. With a context, only edges visible from it count; the short arity reads the KB-wide edge set. (minCommonGenl ?x t1 t2 …) asks the same question as a query.

min-context-parents clj

(min-context-parents kb c)

The minimal contexts context c inherits from: the contexts c reaches over one genlCx edge with no other such context strictly below them. Every other context c sees (context-up) is seen through one of these, so the set is c's position in the context lattice read from below. A stated (genlCx CxLeaf CxTop) beside CxLeaf → CxMid → CxTop leaves CxTop out. Read as context-up reads: an edge an except hides from c is not walked. Not reflexive. One memoized closure read per direct parent. A set; #{} when c is not a node in the context hierarchy.

min-genls clj

(min-genls kb t)

(min-genls kb t context)

The minimal supertypes of type t: its direct parents (direct-genls) with no other direct parent of t strictly below them. Every other strict supertype of t is a supertype of one of these. Read over every believed edge, whatever installed it: a stated (genl dog animal) beside dog ⊂ mammal ⊂ animal leaves animal out. Two parents that subsume each other are both members. Not reflexive. A set; #{} when t is not a node. With a context, only edges visible from it count; the short arity reads the KB-wide edge set, as genls does.

negative? clj

(negative? sentex)

Is sentex a negative literal — a sentex whose sentence is (not S)? Canonical form leaves at most one not, at the head, so the head decides it. False for a rule, which holds no sentence. Reads :sentence alone, so it answers the same for a record and for the map a daemon sends in its place.

open-kb clj

(open-kb)

(open-kb opts)

Construct a KB. Every option is optional; (open-kb {}) is records and index in RAM.

opt	what it picks	default
:backend	a records×index pair, <records>-<index>	:memory
:records / :index	one axis of that pair	from :backend
:space	which in-RAM stores this KB shares	0
:dir	the directory of a durable half	derived from the space
:base / :overlay	the two halves of an :overlay fork	—
:tms	:dense or :reference	:dense
:naming	:strict / :warn / :off	:strict
:recover?	:trust / :auto (or true) / :background / :warn / false	:trust
:oplog?	true (or :each) / :tick / false	false
:reasoners	the shipped reasoners to register, or :stored	none

An unread option is refused (:unknown-option), and an unrecovered KB refuses writes (:unrecovered-kb; *write-unrecovered?* accepts them). Opens that name no :space share space 0, and a second one logs a warning. Details: docs/storage.md, "Opening a KB".

owed-releases clj

(owed-releases kb)

How many departures and arrivals the settles of an open, a recover, an upgrade or a bulk load left owed: the general argument-type mints a departed specific membership had withheld are not drawn until release-withheld! runs, so the KB may miss them. A close and a reopen keep the count (docs/argtypes.md, "Nothing records a withheld mint").

possible-relations clj

(possible-relations kb calculus context a b)

The base relations calculus still allows between a and b, given everything believed in context — the set ask checks a goal against, exposed directly. A singleton is a determined arrangement; the full set is total ignorance; #{} means a or b lies in an unsatisfiable component of the network, and no goal naming it is answered there.

A variable context reads every context's facts into one diagnostic network, which is not the set ask checks against (docs/qcn.md, "Which networks it joins against").

premise? clj

(premise? kb handle)

Is the sentex at handle a premise — asserted in its own right rather than derived? A premise rests on nothing, so no justification names it as a conclusion and retracting its supports cannot take it OUT; a derived sentex is the other case, and supporting-justifications is what shows why. False for a handle the TMS has no node for.

preview clj

(preview kb batch)

(preview kb batch opts)

What would this batch do to the KB, without leaving it done. batch is edit's shape, {:add [[sentence context opts?] …] :remove [handle …]}. The adds are asserted, the removes suspended, belief settles once, the difference is read off, and every write is taken back. Returns

{:believed-added [{:sentence S :context C :handle h|nil :premise? bool :justification {:informant i :strength k :rule S :antecedents [S …]}} …] :believed-removed [{:sentence S :context C :handle h :reason kw :detail {…}} …] :refused [ …check-edit shape… ] :violations [ …violations shape… ] :contradictions [ …contradictions shape… ] :bounded? bool :owed-releases n :release-path :deferred | :swept}

Each half is in content order, :handle is nil for content the batch created, :reason is why-not's, and the standing dilemmas are subtracted from :contradictions. A :refused line is skipped and the rest previewed. opts: :max-depth, :max-term-depth, :max-derivations, :max-results (a positive integer capping each half; :bounded? reports a cut) and :release-withheld? (runs the release sweep, :release-path :swept). A bad key, a bad cap and an unrecovered KB are refused (:unknown-option, :unrecovered-kb). Under oplog/replay! it returns nil. docs/preview.md.

props clj

(props kb kind)

The set of predicates carrying metadata property kind (see has-prop?).

The KB-wide reading: every predicate a declaration the taxonomy holds marks, including one a defeat or an except hides from every reader; has-prop? with a context reads one reader's.

provable? clj

(provable? kb goal)

(provable? kb goal context)

(provable? kb goal context opts)

Is goal provable in context? Takes prove's goal; a conjunction is provable iff all its conjuncts are, under one consistent binding. The search stops at the first solution. opts is prove's bound (prove-opt-keys). A bound it exhausts is :budget-exhausted, never false. A depth prunes, so {:max-depth 2} answers false for no derivation within two rewrites.

prove clj

(prove kb goal)

(prove kb goal context)

(prove kb goal context opts)

Backward-chain in context with the DFS prover; returns a vector of solution binding maps, type-aware and visible from context. prove finds at least what ask finds.

goal is a sentence or a vector of sentences, a conjunctive query whose shared variables join; an empty vector proves trivially. Conjuncts are reordered for cost (query-plan), so solution order is not contract. An (ist Ctx S) goal proves S in Ctx; as a conjunct it is refused, and so is a non-sentence conjunct (:shape).

One solution per derivation: equal binding maps repeat, so use distinct, or query / ask. opts is prove-opt-keys, {:max-ms n :max-depth n}: :max-depth prunes, and reaching :max-ms throws :budget-exhausted (docs/anytime.md).

prove-opt-keys clj

Every key prove / provable? reads: the wall clock, and the rule-expansion depth.

The two bound different things and only one of them suspends. :max-ms is a deadline — the search stops where it is, and a stop is a refusal here rather than a short answer. :max-depth is a pruning bound: the space under it is genuinely exhausted, so the answer is complete for that depth and nothing is refused (docs/anytime.md). Public for query-opt-keys' reason.

prove-within clj

(prove-within kb goal budget)

(prove-within kb goal context budget)

Anytime prove: run the depth-first backward chainer over goal (a sentence or a conjunction vector, as prove) in context, bounded by budget, a map of any of {:max-ms n :max-results n :max-depth n :max-term-growth n}. Returns the partial-result contract of ask-within, and resume continues from the unfinished goal stack (docs/anytime.md). :max-depth bounds the rule expansions the search may stack; :max-term-growth overrides res/default-max-term-growth, the nesting a rule may add past the deepest term its path has met. :max-cost is ignored here.

provenance clj

(provenance kb handle)

The provenance map recorded for handle — {:creator … :created … …} — or nil if none. assert records :creator / :created when a sentex is first created; add-provenance layers on application fields. Removed when the record is retracted. The store's own bookkeeping — the spellings a permuting mark folded into the row — is kept beside these fields and not returned.

prover clj

(prover spec)

A prover built from plain fns, the value add-prover registers. Every fn takes [kb goal context].

(prover {:applicable? (fn [kb goal context] …)   ; does this prover answer the goal?
         :solve       (fn [kb goal context] …)}) ; a seq of binding maps

A prover reading stored facts gives :solve-with-support in place of :solve, so a forward rule that fired on an answer is withdrawn when a fact it named is retracted:

:solve-with-support a seq of [bindings support], support the handles of the facts the answer was read from :support-functors the predicates it answers with support, a non-empty set :support-sources the predicates it reads to answer them, a set

Three readings take a constant or a fn: :est-bindings (a non-negative number; by default 1 for a ground goal and unbounded for an open one), :cost (:lookup, :compute by default, or :search) and :completeness (0 to 100; 50 by default). Refused (:unknown-option): an unknown key, a missing :applicable?, both or neither solve key, a support key without its companions, a value outside its domain (a fn's return is checked at each call), and a support element that is not a handle (as the answer is read). docs/inference.md, What a computed answer rests on.

qualitative-network clj

(qualitative-network kb calculus context)

The constraint network calculus computes over everything believed and visible in context: every pair of terms its predicates relate, tightened by path consistency.

{:calculus :rcc8 :context CxWell :nodes [A B C] :consistent? true :constraints {[A B] #{:ntpp} [B A] #{:ntppi} …}}

When the believed facts are unsatisfiable :consistent? is false, :constraints is the network as stated, and :unsatisfiable names the pairs no model satisfies. :unsatisfiable-sources has one map per component {:source :metric :pairs [[P Q] …] :cycle [P Q R] :support [handle …]}; :cycle is the instants on a negative cycle (:metric only), :support the facts behind them (docs/qcn.md). A variable context reads every context into one diagnostic network.

qualitative-scenario clj

(qualitative-scenario kb calculus context)

One concrete arrangement consistent with everything believed in context, {[a b] → relation} with one base relation per pair, or nil when the believed facts are unsatisfiable. The arrangement is a function of the facts alone, never of arrival order. A variable context draws it from the union network of every context, a diagnostic reading, not a world any reader sees (docs/qcn.md).

qualitative-scenarios clj

(qualitative-scenarios kb calculus context limit)

Up to limit distinct arrangements, as qualitative-scenario renders one. The number of scenarios is exponential in the node count, so the bound is required rather than optional — an unbounded enumeration is not something to reach for by accident.

quality-report clj

(quality-report quality)

A kb-quality map as Markdown — the counts first and the capped lists after. Takes the map, not the KB, so a caller reports on a reading it already holds (and a stored one renders the same a year later).

A map that is not one of kb-quality's answers is refused (:not-a-report). The alternative is a page of zeros and dashes, which is a report a caller who passed the wrong map has no way to tell from a report of an empty KB.

query clj

(query kb goal)

(query kb goal context)

(query kb goal context opts)

Answer goal in context as a seq of binding maps ({?x val …}) projected onto the goal's own variables. goal is a sentence, or a vector of them: a conjunctive query whose shared variables join, as prove takes.

opts makes one decision, how deep to expand rules:

(query kb goal ctx)                   no rule expansion — the registry alone
(query kb goal ctx {:max-depth 3})    the node engine, ≤3 rewrites deep

There is no default depth. Detail: docs/api.md, "Contract notes: query".

query-contexts clj

The query contexts, as a set: CxEverything, CxInference and CxNothing, each a reading mode spelled as a context rather than a context a sentex can be stored in. A write given one is refused. A set is a predicate, so (query-contexts x) asks whether x is one. docs/contexts.md

query-opt-keys clj

Every key query / query? read: :max-depth, :proof?, :strategy, :portfolio?, :auto? and :racers (the node engine's keys go to inference/solutions). A key off this set is refused (:unknown-option). :first-result? is a strategy key ({:strategy {:first-result? true}}), as are the signs and weights in vaelii.impl.tactics/defaults.

query-plan clj

(query-plan kb goal)

(query-plan kb goal context)

How a goal would be answered. A single sentence gives the provers applicable to it with their per-prover estimates and which of them run; an entry that does not run carries :runs? false with a :shadowed-by, or :guarded-by naming a source no prover reads. A vector gives the join plan: the conjuncts in run order, each a map of :goal, :bound-before, :est-matches (upper bound on fan-out under those bindings), :est-rows, :est-prefix, :block and the flags :deferred?, :recursive? and :isolated? (docs/inference.md, "Conjunctive query planning").

(query-plan kb '[(dog ?y) (parentOf Tom ?y)] 'CxMantle) ;; => ({:goal (parentOf Tom ?y) :est-matches 2 :bound-before #{} ...} ;; {:goal (dog ?y) :est-matches 1 :bound-before #{?y} ...})

query-status clj

(query-status kb goal context)

(query-status kb goal context opts)

query's answers, plus a report of the run, so a query truncated at the depth bound reads differently from one whose goal is unprovable.

{:answers                 [{?x v} …]   `query`'s own answers, realized
 :count                   n
 :status                  :complete | :truncated | :incomplete
 :truncated?              bool         = (= status :truncated)
 :unenumerated            [P …]        transitive predicates whose closure a goal
                                       with both arguments open did not enumerate
 :unenumerated-in-guards  [P …]        those recorded inside an `unknown` or
                                       `exceptWhen` evaluation
 :depth                   d | nil      the depth bound the read ran under
 :time-to-first-answer-ms t | nil      nil when there are no answers
 :total-time-ms           t
 :stats                   {…}}         node-engine `tree-stats`, at a depth

:truncated? is conservative: true means the depth bound stopped at least one rewrite, so the answers may be incomplete; false with an empty :unenumerated guarantees every answer the KB entails at that depth. :incomplete means :unenumerated is non-empty and the bound cut nothing. Opts and depth resolution are query's. A variable or query context is refused (:unsupported-context). docs/api.md, "What an exhausted bound answers".

query? clj

(query? kb goal)

(query? kb goal context)

(query? kb goal context opts)

Is goal answerable under opts? query, asked for one answer: the search stops at the first.

read-manifest clj

(read-manifest f)

The EDN manifest in file f — a dump's or a store's meta.edn / format.edn — read under a byte bound. Refused as :manifest-too-large past the bound, and as :malformed-manifest for content the EDN reader cannot parse, so a caller probing a directory it knows nothing about reads a bounded number of bytes and can tell "not a KB" from "a broken one".

readable-sentence clj

(readable-sentence sx)

A sentex's sentence with the author's variable names restored — pass a sentex map (from sentex / sentexes-matching). A rule is stored canonically numbered (?var0, ?var1, …), which reads as gibberish; this applies its :varmap back so it displays as written (?x, ?y). A fact has no varmap and is returned unchanged; nil in, nil out. Used by why and by any display of a stored rule.

reasoner clj

(reasoner nm)

The prover named by keyword, a value for add-prover. add-reasoner is the ordinary way in. Six are the relation algebras calculi describes; :duration and :metric-time are the quantitative pair (docs/duration.md, docs/stp.md), :sign the qualitative arithmetic (docs/sign.md), :calendar the clock behind the calendar constructors and :includes-instant a temporal read off the point network (docs/time.md), and :brave-cautious the ASP reader of (bravely S) / (cautiously S) (docs/labeling.md). An unknown name is refused as :unknown-option.

reasoners clj

(reasoners)

The names of the optional reasoners, sorted — what add-reasoner takes. calculi describes the six that are relation algebras in full; the other five are the quantitative reasoners, the calendar clock and the instant-inclusion reader, and :brave-cautious is the ASP dilemma reader (docs/labeling.md).

rebuild-progress clj

(rebuild-progress kb)

Where the belief rebuild behind kb's installed image (:recover? :background) has got to, or nil when none runs: the state write-hazards reports as {:stale-belief true}. A rebuild that threw stays reported, with :failed, until recover rebuilds belief on the calling thread.

:step :of :label the step running now (1-based), the step count, its phrase :failed after a throw: {:at :class :message} :started-at :elapsed-ms when the rebuild began (epoch ms), and how long it has run :image the installed image's :source digest and :written-at, and its :recover step timings when recorded :source the running build's source digest :expected-ms :fraction the image's recorded recover total, and the share the steps done so far took

record-arg-types clj

(record-arg-types kb)

Record the argument-type memberships and genl edges the stored facts entail, over a store loaded without them (a dump import, a *bulk-load?* load or bulk-assert-facts!), and settle. Returns {:facts n :recorded n :violations n}: the facts read, the records created, and the derivations the ledger reports. Idempotent; nothing is recorded under VAELII_ASSERTIVE_ARG_TYPES=0. It runs no forward chaining. record-arg-types! draws the same facts and can stop, resume and set a fact aside (docs/argtypes.md).

record-arg-types! clj

(record-arg-types! kb)

(record-arg-types! kb opts)

record-arg-types as a run that can stop and resume, for a store where the pass takes hours. What the pass owes is kept in the store (arg-types-owed), so the next call resumes it (docs/argtypes.md, "The pass over a stored KB").

opts:

:resume? default true: carry on from what the store says is owed. :budget-ms default 2000: how long one fact's checks may run; a fact past it is set aside (owed, with the :phase that ran out). nil: none. :retry-deferred? default false: after the sweep, draw each set-aside fact again. :stop? a no-argument function; truthy stops at the next fact. :on-progress called at most every :progress-every-ms (default 1000) with {:phase :done :total :recorded :deferred}; :phase is :arg-types, :releases, :deferred, :settle or :done. A throw stops the pass and is rethrown once it has committed. :commit-every-ms default 30000: how long the pass draws between two commits.

Returns {:drawn :done :total :recorded :violations :deferred :stopped :complete?}; :stopped is nil or :requested / :shutdown / :cancelled. Refuses a KB without belief (:unrecovered-kb) and an owed record written after the records the store holds (:owed-record-ahead).

recover clj

(recover kb)

Rebuild the in-memory JTMS and taxonomy from the persistent stores. Call after constructing a KB against an existing store, e.g. after a restart. Derivation depths reset to 0 (they only bound future forward chaining). The JTMS is rebuilt first, the taxonomy replays every stored special-predicate sentex and is then reconciled against belief, and belief is settled last (docs/taxonomy.md). The orchestration lives in vaelii.impl.recovery (docs/namespaces.md, "The layering").

register-modal-predicate clj

(register-modal-predicate kb pred)

(register-modal-predicate kb pred context)

Grant pred belief-style projection: (pred agent sentence) is answered by proving sentence in agent's context, as believes is (docs/belief.md). Asserts the (modal_predicate pred) marker, so retract! of it takes the grant back. With no context the grant is in CxUniverse, where the default believes grant lives; pass a context to scope it. Returns kb.

reified-term? clj

(reified-term? term)

Is term a reified non-atomic term — the opaque constant a ground (F a…) under a reifiable_function was minted as (docs/nat.md)? A pure test on the symbol's reserved namespace, so a display layer can ask it of every term it renders and pay a read only where the answer is true. term-expression is what to render in its place.

reindex clj

(reindex kb)

Rebuild the index store — the trie, secondary roots, rule index, exception index, and term index — wholesale from the stored sentexes, then recover. The repair for a torn record/index write and the migration for an index layout change; see vaelii.impl.reindex. Returns {:sentexes n :rules n}.

This is the repair a derived index needs and recover alone is not: an index rebuilt from the records is what makes assert find a stored sentence again, so it is what makes such a KB writable (*write-unrecovered?*).

relation-arity clj

(relation-arity kb term)

The exact number of places that binds term, its own or one inherited through genl, or nil when no exact length binds it (a variable_arity relation, or none stored). Read the same at every context. docs/taxonomy.md, "Arity".

relation? clj

(relation? kb term)

(relation? kb term context)

Is term a relation of two or more places by what the KB stores of it, visible from context (default ?ctx, every context): an (arity P n) declaration or exact-arity class membership of two or more, or a variable_arity membership, or, where none of these answers, a length of two or more inherited through genl. A genl edge between two relations puts both in types; such a node is a relation and not a type, and a node with an arity of one or none is a type. No spelling is read. docs/taxonomy.md.

release-withheld! clj

(release-withheld! kb)

Draw the mints the owed departures and arrivals (owed-releases) can have withheld, chain from them and settle. Returns {:terms n :released n :ms n}: the terms whose mints were drawn again, the records drawn and the wall time. Nothing runs it implicitly; a second run draws nothing.

remove-unsupported! clj

(remove-unsupported! kb opts)

Delete the unsupported records opts names (unsupported), with their postings, each through retract!, and return {:unsupported-removed n :handles [h …]}. {:handles hs} removes the unsupported records among hs; others are left. {:force? true} removes every record unsupported reports. With neither, refused (:unsupported-unattested): this call deletes only what its caller attests. docs/storage.md.

representative clj

(representative kb term)

(representative kb term context)

The term standing for term's equivalence class — term itself when nothing has merged it, so this is total and never nil.

With a context, only the merges that context inherits count, and the answer is its own election over them, since an invisible edge can split a class (docs/equality.md, "Scope, context, and re-election").

request-stop! clj

(request-stop! kb)

Ask the record-arg-types! pass running over kb to stop at its next fact boundary, from any thread. True when a pass was running, false when none was; a request is not held for a later pass.

reset-settle-stats! clj

(reset-settle-stats! kb)

Clear the settle instrumentation, including the histogram.

rests-on clj

(rests-on j)

Every handle justification j needs believed to be valid: its antecedents, plus its informant when the informant is a rule handle. A pure read of the map justification returns, so a caller asking which of a justification's supports are OUT, or which justifications a retraction would take down, reads the same set the JTMS reads.

resume clj

(resume partial budget)

Continue a :timeout / :capped partial result from ask-within / prove-within under a fresh budget, returning the next partial result, whose :unenumerated holds every step's. A :complete or :incomplete result has no continuation and is returned unchanged (docs/anytime.md), so

(loop [r (ask-within kb goal ctx budget)] (consume (:results r)) (when (:resume r) (recur (resume r budget))))

terminates when the search is exhausted.

retract! clj

(retract! kb handle)

Retract premise support for a handle, tear down solely-supported sentexes and justifications (keeping anything re-derivable via other witnesses), and reverse their taxonomy / rule-index effects. Returns counts.

An inert sentex (assert-inert) was never a TMS datum and is torn down directly, with no settle. A stored premise the TMS has no node for is refused (:unrecovered-premise); see retract-storage!.

same-class? clj

(same-class? kb a b)

(same-class? kb a b context)

Do a and b denote the same thing? Distinct symbols denote distinct individuals until an equality sentex says otherwise. Scoped by context like representative. Not the complement of a provable (different a b): both read false of an unmerged indeterminate_term (docs/predall.md). (not (same-class? …)) answers "not known to be the same thing".

seal clj

(seal kb)

Seal kb's operation log (open-kb's :oplog?): write the index image and the reasoning image, name them in seal.nippy, and start the log's next generation (docs/storage.md, "The operation log"). Returns {:sealed true :generation g :watermark w :ms t}, or {:sealed false :reason r} with nothing changed, r being :not-applicable (no log), :in-operation, :settle-deferred or :settle-running. A KB whose images cannot be written answers that reason and marks the log unusable, so the next open rebuilds from the records. A log that stopped on a failed write or fsync refuses with :store-unusable. Call it from the thread that writes kb.

search-tree clj

(search-tree kb goal)

(search-tree kb goal context)

(search-tree kb goal context opts)

The backward search for goal in context as data: every node the frontier reached, what each cost and what was dropped. The read behind the inference debugger.

Needs a depth ({:max-depth n}, or *query-options* :max-depth) and runs query's search. The key set is search-tree-opt-keys (:node-budget, an optional :max-ms that reports :timeout, and :strategy); another key is refused (:unknown-option). Returns {:goals :context :strategy :status :bounded? :answers :nodes :stats :unenumerated :unenumerated-in-guards}; :status is :complete, :bounded or :timeout, and each answer carries the :node it came off.

search-tree-opt-keys clj

Every key search-tree reads: the depth, the search ordering, the node-expansion budget and the wall clock. Not query's key set plus two: search-tree runs under :proof? true and reaches the node engine's session directly, so :proof?, :portfolio?, :auto? and :racers are keys it overwrites or never reads (docs/api.md, "Argument-shape contracts").

sees? clj

(sees? kb k y)

Does context k see assertions made in context y? True iff y is in k's genlCx up-closure (reflexively, so a context sees itself).

sentence-of clj

(sentence-of sx)

A sentex map's canonical sentence: a literal's :sentence, or for a rule the (implies <antecedent> <consequent>) form built from its :antecedent and :consequent — a rule map carries no :sentence of its own. The variables are the canonical ?var0 ?var1 …; readable-sentence gives the author's names instead. nil in, nil out.

sentex clj

(sentex kb handle)

The sentex for a handle as a map, or nil. Same shape contract as sentexes-matching's elements: :id (the handle), :sentence, :context, and for a rule :antecedent / :consequent / :engines / :defeasible / :effect. Key into it; the concrete vaelii.impl.types.sentex/LiteralSentex / RuleSentex record class is internal and not part of the contract. nil (handle-of of an absent sentence) answers nil; a non-handle (a vector of handles included) is refused (:bad-handle).

sentex-count clj

(sentex-count kb)

How many sentexes the KB holds, in total — the count the count-aware trie keeps at its root, so O(1) and nothing fetched.

A count of what is stored, like the count-* trio: a defeated or unsupported sentex is included, as is a rule and a metadata declaration. Summing count-in-context over contexts is not the same number — that counts only what is in a context the taxonomy knows, so content in a context no genlCx edge mentions is invisible to it.

sentex-handle clj

(sentex-handle n)

The (sentexHandle <id>) term that names the sentex stored at handle n. A meta-sentex predicates about another sentex by carrying this term in an argument — (exceptWhen <query> (sentexHandle H)) names the rule it qualifies, and a target- following predicate (target_following_predicate) names the claim its reply hangs on — so retracting the named sentex can cascade to the meta. The inverse is handle-id.

sentex-handle? clj

(sentex-handle? form)

Is form a (sentexHandle <id>) term — the naming wrapper sentex-handle builds?

sentexes-in-context clj

(sentexes-in-context kb context)

(sentexes-in-context kb context opts)

Every stored sentex asserted in context (its extent, rules included), a defeated or unsupported one included. Pass {:believed? true} to keep only what the JTMS believes, at a TMS lookup per handle. An opts key this fn does not read is refused (:unknown-option). The result is a lazy seq over live state (see records-of); vec it for a snapshot.

sentexes-matching clj

(sentexes-matching kb sentence)

(sentexes-matching kb sentence context)

Believed sentexes matching sentence in context (default ?ctx). Literal (no subtype expansion); use ask for full inference. find-sentexes is the raw read.

Returns a lazy seq of sentex maps over live state (vec it for a snapshot) with keys :id (the handle), :sentence (a negative literal's is (not S)), :context, and for a rule :antecedent / :consequent / :engines / :effect. Beside a writer thread the answer is not one state's (docs/storage.md, "The single-writer contract"). A ground reifiable NAT reifies to its existing constant (never mints); an (ist Ctx S) sentence asks S in Ctx. A vector pattern is refused (:shape).

sentexes-naming clj

(sentexes-naming kb handle)

(sentexes-naming kb handle opts)

Every stored sentex whose sentence nests (sentexHandle handle) — the meta-sentexes naming handle — a defeated or unsupported one included. One term-index read. Pass {:believed? true} to keep only what the JTMS believes (O(n) in the answer). An opts key this fn does not read is refused (:unknown-option). Empty for a nil handle; a non-handle is refused (:bad-handle). A lazy seq over live state, as sentexes-in-context is — vec it for a snapshot.

sentexes-with-arg clj

(sentexes-with-arg kb pos term)

(sentexes-with-arg kb pos term opts)

Every stored fact sentex holding term at 1-based argument position pos — a defeated or unsupported one included. Pass {:believed? true} to keep only what the JTMS believes (O(n) in the extent). An opts key this fn does not read is refused (:unknown-option). A lazy seq over live state, as sentexes-in-context is — vec it for a snapshot.

sentexes-with-functor clj

(sentexes-with-functor kb pred)

(sentexes-with-functor kb pred opts)

Every stored fact sentex whose functor is pred, any arity, either polarity — a defeated or unsupported one included. Pass {:believed? true} to keep only what the JTMS believes (O(n) in the extent). An opts key this fn does not read is refused (:unknown-option). A lazy seq over live state, as sentexes-in-context is — vec it for a snapshot.

separating-covers clj

(separating-covers kb)

The believed separating and partition declarations, as a set of [whole parts kind]: every two distinct parts are disjoint, and disjoint? reads them from this table. Like a metatype's clique, the pairs are consulted, never stored as (disjoint a b).

set-cache-limit clj

(set-cache-limit id n)

Override cache id's bound with n regardless of the scale, or clear the override when n is nil, and return the profile. id is a :cache keyword from caches, n a positive whole number. Refused (:unknown-option) when id is not a keyword or n is neither nil nor a positive whole number, and for a cache no override moves (docs/caches.md). An id that names no registered cache is warned, not refused, and the override is recorded.

set-cache-scale clj

(set-cache-scale x)

Multiply every count-bounded cache's shipped limit by x, on a running process, and return the profile. 1.0 restores the shipped bounds; below 1 shrinks the caches, above 1 grows them. A per-cache floor keeps a small scale from taking a cache below the point where it saves nothing. Process-wide, as set-log-level is. VAELII_CACHE_SCALE sets the starting value. Refused when x is not a number or is below zero (:type :unknown-option).

set-log-level clj

(set-log-level level)

Set how much the engine says, on a running process, and return the level. One of :error :warn :info :debug :trace, quietest first; anything else is refused (:type :unknown-option). Process-wide, since two KBs in one JVM share one *log-fn*; the daemon's op table does not carry it, and a daemon's level is the one its process started with (VAELII_LOG_LEVEL) or this call from its own REPL. log-level reads it back.

set-solver clj

(set-solver kb solver)

Install the solver a labeling (docs/labeling.md) solves a dilemma's program with when no ASP backend is reachable, returning kb. Takes a name:

:stub (the default) a deterministic local stub: greedy, one contradiction at a time :asp the real answer-set backend: globally optimal, order-independent (docs/asp.md); native clingo, else the clasp subprocess, else the stub

or any vaelii.impl.types.solve/Solver value.

settle-record-edits! clj

(settle-record-edits! kb)

(settle-record-edits! kb opts)

Settle what edit-records! batches left: build belief over the edited records (reindex when the index was never built, else recover when belief was not), delete the stored justifications resting on a record the store does not hold, sweep the consequence closure of their conclusions and of :seeds as a retraction does, and re-chain the affected rules. Unless :arg-types? false, record-arg-types then draws the argument-type mints a removal released.

opts: :seeds, the union of the batches' :seeds; :arg-types?, default true (when false the pass is owed, arg-types-owed, whenever anything was removed); :on-progress, called with {:phase :done :total} as each step begins, :phase being :reindex, :recover, :sweep or :arg-types. A throw from it is rethrown at the next phase boundary, and a second call finishes. Returns {:rebuilt :reindex|:recover|nil :unrooted n :removed-sentexes n :removed-justifications n :rules-chained n :rechained n :arg-types {…}}, or :arg-types-owed? bool in place of :arg-types. docs/storage.md, "Editing the records of a KB without belief".

settle-stats clj

(settle-stats kb)

Instrumentation for the exceptWhen fixpoint in settle: {:iterations n :passes n :histogram {n count}}. :iterations counts the passes of the last settle in which the blocked set moved (0 nothing blocked, 1 one pass sufficed, ≥2 the fixpoint iterated), :passes the total loop passes including the confirming one, and :histogram the distribution of :iterations over every settle since reset-settle-stats! (docs/exceptions.md).

sort-by-content clj

(sort-by-content keyfn coll)

(sort-by-content keyfn cmp coll)

coll ordered by (keyfn element) under cmp, the engine's content order, for ranking sentexes, sentences or terms instead of sort-by on a printed key or a handle.

cmp defaults to the structural comparator the engine's orders use; pass compare when the key is already a Comparable tuple. A keyfn that returns a handle makes the ranking depend on load order: key on :sentence / :context (docs/nmtms.md).

specified-violations clj

(specified-violations kb pred indep context)

(specified-violations kb pred indep context arg-pos)

The audit result for one binary (predAllSpecified pred indep) integrity requirement in context, always carrying a :status: {:status :audited :violations #{x…}}, every member x of indep for which no believed (pred x y) carries a determinate filler y satisfying pred's derived slot contract, or {:status :gap :gap :missing-slot-typing …} where pred carries no visible slot typing at the audited position. arg-pos selects the twin: :second (the default) is predAllSpecified; :first is predSpecifiedAll. Computed on demand and not filed (docs/predall.md).

specs clj

(specs kb t)

(specs kb t context)

The subtypes of type t, reflexively — t itself plus everything that reaches it by genl. A set; #{t} when t is not a node in the type hierarchy. This is the fan-out that lets an antecedent (animal ?x) match a stored (dog Muffet). With a context, only edges visible from it are walked.

The short arity reads the KB-wide edge set, as genls' does.

store-backend clj

(store-backend dir)

The :backend to pass open-kb for the store in dir, read off its files, or nil when dir holds no store: :disk-snapshot for a mapped index image, :disk-log for a write-ahead-logged index, :disk-columnar for records with no index file, :sqlite for the SQLite adapter's file, and :pg-disk-log or :pg-snapshot for a local index or its images whose records are on a server (the open reads that server off the directory's records identity when no :pg is given). An open under the wrong backend throws nothing and returns an empty KB, so a caller opening a directory it did not write reads the backend here rather than naming one.

store-state clj

(store-state kb)

(store-state kb ks)

What kb's record store and belief network hold, as a map of booleans:

:readable? one stored record reads back as a sentex (true for an empty store); on false the map adds :thawed-keys, the keys that record read back with :network? the belief network holds a node for at least one handle :believes? the belief network holds at least one IN node :recoverable? the store holds a premise mark or a justification, which recover rebuilds belief from

ks names the keys to compute and defaults to all four; another key is refused (:unknown-option). :believes? false over a non-empty store means every answer is empty; recover repairs it when :recoverable? is true, a reload when false.

stored-first-args clj

(stored-first-args kb pred)

The terms stored at argument 1 of a fact with functor pred, as a set: the index's own child set under pred, one read — no record fetched and no belief consulted, so a defeated or unsupported fact's term is in it. For a type, its members without its extent: a type with a hundred thousand members answers in milliseconds, where sentexes-with-functor fetches a hundred thousand records. A caller that needs belief checks the terms it keeps (types-of).

subsumption-status clj

(subsumption-status kb a b)

(subsumption-status kb a b context)

The subsumption relationship of type a to type b, one of: :coextensional (each is genl the other), :genl (a is a subtype of b), :spec (a is a supertype of b), :disjoint (provably no shared instance), :orthogonal (see subsumption-statuses), :unknown (none provable) or :inconsistent (contradictory relationships hold). Wraps subsumption-statuses: an empty set is :unknown, a singleton is that status and two or more is :inconsistent. context is the vantage :disjoint and :orthogonal are read from (default CxUniverse).

subsumption-statuses clj

(subsumption-statuses kb a b)

(subsumption-statuses kb a b context)

The set of applicable subsumption relationships between types a and b: any subset of #{:coextensional :genl :spec :disjoint :orthogonal}. A consistent pair yields a singleton, an inconsistent pair several, and a pair with no provable relationship the empty set. genl? reads the global cached closure; disjoint? and the :orthogonal witnesses read context (default CxUniverse). The instance and subtype reads are facts-only, so the status is the same under every query engine. Witnesses and combinations: docs/taxonomy.md.

supporting-justifications clj

(supporting-justifications kb handle)

Justifications that conclude handle, in content order (kb/justification-content-key), so one knowledge base answers identically whatever order it arrived in. Empty for a nil handle; a non-handle is refused (:bad-handle). docs/nmtms.md.

switch-value clj

(switch-value spelling)

The value of the build switch spelled spelling, a VAELII_* environment variable or a vaelii.* system property, read against its domain now, as open-kb's check reads it. A value outside the domain is refused (:unknown-option, :mismatch :bad-value), as is a name the build reads no switch under (:mismatch :unknown-key); either names the switch under :switch and the older key under :property. The table is vaelii.impl.config/switches, tabulated in docs/operations.md.

term-count clj

(term-count kb)

How many distinct terms the KB's vocabulary holds — one set-size read, O(1), nothing fetched. The cardinality of terms, and like it a count of what is stored.

term-expression clj

(term-expression kb term)

The functional expression a reified term denotes — (FruitFn AppleTree) for the constant minted from it — or nil for an ordinary term, and for a reified one whose (natFormula K E) map is not believed.

One hop: an argument that is itself a reified term comes back as its constant (docs/nat.md, Display / export). One index read per call.

term-role clj

(term-role term)

The naming role of term: :variable (?x), :number, :lexeme, :context, :individual, :predicate, :sense, :type, or nil (a string, or a symbol matching no convention). Reads the naming invariants assert enforces (docs/naming.md). The most specific role wins: :lexeme before :context before :individual, and :sense before :type.

terms clj

(terms kb)

Every term the index is keyed by: each predicate, individual, type and context name mentioned by a stored sentex, at any nesting depth, as a vector sorted by name. Cost is O(terms). A ground compound subterm is not a name and is not listed. Defeated and unsupported sentexes keep their names here (docs/indexing.md).

try-assert clj

(try-assert kb sentence)

(try-assert kb sentence context)

(try-assert kb sentence context opts)

assert, refusing a sentence that would open a definitional clash with believed content visible from context. The refusal is :definitional-clash, carrying the kind in :violation (the fourteen kinds: docs/api.md, "Refusing a clash"), the members it clashes with in :clashes-with, and :entailed-from when a mint clashes; the call stores nothing. An :unsatisfiable-network is refused after the settle unless opts carries :refuse-unsatisfiable? false. Every other refusal, argument and return value is assert's. The result depends on what is already stored, so this is the one write entry point whose result depends on arrival order.

types clj

(types kb)

(types kb context)

Every type currently in the genl hierarchy — the nodes of the closure, i.e. every type named by some believed genl edge. With a context, only a node touched by an edge visible from it counts — the same visibility genl? and disjoint? read with a context.

types-of clj

(types-of kb x)

(types-of kb x context)

The types asserted of individual x — functors of unary sentexes (T x), found via the term index. Scoped to memberships visible from context (default: any context).

unsupported clj

(unsupported kb)

The stored records the last recover found with no premise mark, no justification and no :inert mark, as {:n n :handles [h …]}, ascending, re-checked against the KB now: a handle since premise-marked, concluded, marked :inert or retracted is left out. The re-check reads the network and no store. Such a record stays OUT. The count can include an assert-inert record written before assert-inert marked its records; mark-inert! marks one. remove-unsupported! deletes them.

unwatch clj

(unwatch kb token)

Stop calling the listener token names; true if there was one. Idempotent — a token already dropped removes nothing and says so.

Called off the writer's thread, the listener can be called once more after this returns, for an event whose delivery read the registry before it (docs/feed.md).

violations clj

(violations kb)

The ledger of definitional constraints a derived conclusion would have broken during forward chaining, and what a bounded pass did not reach: a vector of {:violation <kind> :sentence S :context C :rule handle :run n :detail {…}}. Read :sentence and :context with when-let: an entry about a term, pair, budget, network or antecedent names no dropped sentence. The ledger keeps the newest 1000; clear-violations! empties it, except the :forced-conclusion, :inert-argument and :inert-rule entries, which are read off stored state at each call. Every kind and its :detail keys: docs/api.md, "The violations ledger".

vocabulary-audit clj

(vocabulary-audit kb)

Every term core.txt comments in kb, classified: {:enforced [[term why] …] :inert [[term why] …] :unclassified [term …] :retired [term …] :contradicted [term …]}. :unclassified is a declaration nobody classified, :retired a classification of a term the KB no longer declares, :contradicted a term the special-predicate table gives an arm to and the classification calls inert. The three are empty on the shipped ontology.

watch clj

(watch kb f)

(watch kb goal context f)

Be told when belief moves, instead of asking again. Two shapes, both returning a token for unwatch:

(watch kb f) every belief change (watch kb goal context f) a standing query: only what answers goal

f is called with one argument, {:believed-added [...] :believed-removed [...]} in preview's entry shapes, plus :defeats and, for a plain listener, :unsatisfiable (docs/feed.md). A standing query's entries carry :bindings too, and f is not called when nothing its goal answers moved. context scopes the goal up the genlCx ancestor set; '?ctx watches every context.

One settle, one call: a batch under with-deferred-settle / assert-many / edit delivers one event. f runs on the writing thread after the settle and may read and write; delivery gives up after 64 rounds with a warning, and a listener that throws is logged and skipped. A goal whose answer is not a function of the region is refused (:not-watchable): a conjunction, an aggregate, unknown, thereExists, an evaluable, an ist, and either polarity of a predicate a registered calculus answers.

watchers clj

(watchers kb)

What is currently listening, in registration order: {:token t} for a plain listener, plus :goal and :context for a standing query. The functions themselves are left out — a token is what unwatch takes, and a listener is not a value to compare.

why clj

(why kb handle)

Why does the KB believe handle? The justification graph reachable from handle, as data:

{:root h :nodes {h {:handle h :sentence S :context C :believed? true :defeat-class :default :premise? false :support [{:justification jid :informant <rule handle or symbol> :rule <the rule's sentence> :strength :monotonic :verdict :supports :because [h1 h2 …]}]} h1 {…} h2 {…} …}}

:nodes holds one node per reachable handle and :because names antecedents by handle. A premise is :premise? true with its :strength and no :support. A derived node's :support is its justifications in content order. Each :verdict is the reason the node's context reads on that justification; a believed node can list one a guard defeat (:guard) or an exception (:blocked) covers. Belief is read at each node's own context. A stored node not believed there is a leaf {:believed? false}; ask why-not (docs/nmtms.md). An unknown handle (nil included) is a node {:stored? false}.

why-not clj

(why-not kb handle)

(why-not kb sentence context)

(why-not kb sentence context opts)

Why does the KB not believe handle? The complement of why, as data: {:handle h :sentence S :context C :believed? false :reason <keyword> …}, with one :reason per way a handle goes unbelieved (:not-stored, :superseded, :defeated, :withdrawn, :inert, :forced-conclusion, :unsupported, :excepted, :closed-extent). A believed handle yields {:believed? true}. A nil handle is :not-stored; a non-handle is refused (:bad-handle). (why-not kb sentence context) takes an (ist Ctx S); {:nearest n} adds the n closest rules for :not-stored (why-not-opt-keys). docs/api.md, "Contract notes: why-not".

why-not-opt-keys clj

Every key why-not's sentence arity reads. :nearest n asks for the n rules that came closest and is the switch that runs a search at all; :max-depth and :max-ms are that search's bounds. A key off the key set is refused (:unknown-option) — a misspelt :nearset would answer the ordinary why-not and read exactly like a goal no rule concludes.

with-deferred-settle clj macro

(with-deferred-settle kb & body)

Run body, a batch of assert / assert-rule / ist calls on kb, with belief settled once at the end instead of after every assertion. The belief is the same as a settle per assertion. Returns body's value.

(v/with-deferred-settle kb (doseq [f facts] (v/assert kb f 'CxSome)) (v/assert-rule kb ante conseq 'CxSome))

A read inside body sees the batch unsettled, and a retract! inside settles eagerly. Nesting composes, and the outermost settles. Not a transaction: a throw mid-batch leaves what was stored in place (docs/api.md, "Batched assertion").

write-hazards clj

(write-hazards kb)

What makes a write into kb wrong, as a map of the hazards that hold: {:no-belief true} when its belief network was never rebuilt from the records, {:no-index true} when its index was never rebuilt either, both, {:stale-belief true} while belief is rebuilt behind an installed image (:recover? :background), or {}. The write entry points refuse on a non-empty answer (:unrecovered-kb), so a caller rendering a write form can refuse first. recover retires :no-belief and reindex retires both. A hazard over an empty store reads as absent.