vaelii.core — com.vaelii/vaelii 0.1.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 / genlContext 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 roster — 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 only public one; the engine 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.

*bulk-load?* clj

When true, the assert path runs in bulk-load mode: for a caller-guaranteed well-formed, DISTINCT premise load (a corpus import, the bench wload/w8x/w5x setup), the per-fact machinery that only validates or dedups is turned off, since the caller has already guaranteed what it checks. Specifically, assert-one skips:

• the definitional checks (nm/problems naming, check-ground, wff-problems, check-edge-stratified, constraint-checks — the last of which runs a LIVE (argIsa pred ?n ?type) store query on every fact, the dominant per-fact cost);
• the find-sentex-handle dedup trie-walk — a distinct corpus creates one sentex per fact regardless, so the probe is guaranteed to miss;
• provenance stamping (stamp-provenance!) — belief never reads provenance, so a bulk premise carries none.

It does not touch what gets stored, indexed, or believed: the same sentex lands for the same fact, so the KB answers identically to a per-fact load (same query results + count-with-functor). Bind it only around a load whose facts are known well-formed and pairwise distinct; normal assert (the default) keeps every guarantee. Pair it with with-deferred-settle (one settle at the end) and {:chain? false} for the full fast path — bulk-assert-facts! does all three.

*clock* clj

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

*creator* clj

The creator stamped into a sentex's provenance on assert 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), a frontier of whole conjunctions ordered by cost :hybrid the node engine, except at :max-depth 0, where no node is ever expanded past the root and the session and its queue would be pure overhead

The default is :dfs. Two engines that disagree are worse than one engine that is slow, and they do disagree past the node engine's depth bound: it terminates on that bound where the DFS terminates on the data, so a derivation deeper than the node engine's depth bound is found by one and not the other — and that bound has no default, so :inference requires the caller to choose one (*query-options* :max-depth, or inference/*max-depth*). Within the bound the two return the same answer set, which is what inference_parity_test holds them to.

*query-options* clj

How the node engine searches, when *query-engine* routes a query to it. Ignored by the DFS, which has one order and no choice to make.

{: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 shape of the query

nil — the default — is the shipped ordering, and costs nothing to leave alone. Every tactician returns the same answer set (docs/inference.md), so this is a latency choice: an exhaustive run expands the same nodes whatever the order, and an ordering can only pay a consumer that stops early. :portfolio? and :auto? reach only prove; a race has no partial answer to hand back, so prove-within takes the strategy and drives the ordinary stream.

-main clj

(-main & _)

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.

prove answers whether a goal follows. This answers what it is missing: it runs the same backward search, watches where the proof dead-ends, and hypothesizes the missing subgoal — as an ordinary :default premise in a scratch microtheory hung below context, so the assumption sees everything the question could see and nothing that existed before can see the assumption.

{:solutions   [binding-map …]     under the hypotheses, not instead of them
 :hypotheses  [{:sentence :context :handle} …]
 :refused     [sentence …]        dead ends the gate would not assume
 :context     AbductionXContext
 :status      :complete | :capped}

An empty :hypotheses means the goal was proved outright. Otherwise the solutions hold given those sentences — which is why they come back together, and why there is no arity that returns the solutions alone. They are prove's solutions either way, unprojected, so they carry a rule's canonical variables; and because a hypothesis is minted through the whole assert pipeline, chaining included, a goal a rule concludes is usually answered twice over — once as the fact that firing stored in the scratch context, once by the rule expanded over the hypothesis.

A predicate is hypothesized only if it was granted. (abduciblePredicate P) is what makes a (P …) assumable, read from the asking context's genlContext up-cone; nothing else is, ever. A hypothesis must also be ground, must pass every check an assertion passes, and must not contradict anything believed where it lands. An abducer without those explains everything and is worth nothing.

It is defeasible, needing no rule of its own: a :monotonic fact that contradicts a hypothesis defeats it through the ordinary path, and what the hypothesis licensed goes OUT with it.

opts carries the caps — :max-hypotheses (default 8) and :max-depth (8), the rule depth past which a dead end is left alone — plus :keep?. Without it the scratch context is torn down before returning, so a call whose result you ignore leaves the KB as it found it; with it the context stands, the handles are real, and you discard it with abduce-discard!. Committing a hypothesis to a context that outlives the scratch is deliberately yours to do: abduction proposes.

The hypothesis set is irredundant — no single member can be dropped and still answer the goal — which is not the same as minimum. See 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. One edit, so the dependency-directed sweep takes the derived content with the premises it rested on.

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-defined bookkeeping layered onto the creation record — source, confidence, review state — without touching :creator / :created unless m names them. Provenance is metadata, not belief, so this is additive with no !.

add-prover clj

(add-prover kb prover)

Register an additional prover (implementing vaelii.impl.provers/Prover) on kb.

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 the whole of the opt-in, and it is per-KB: an unregistered algebra's facts are stored and retrieved as ordinary facts and cost nothing. Registering changes what is derivable, not what is stored — the entailed relation is computed from the network the stored facts constrain, carries the handles it rests on as its support, and so can be forward-chained on and retracted through like any other antecedent (docs/qcn.md).

Idempotent per name: registering one twice would have the goal claimed twice and answered identically, so the second is dropped rather than paid for. Sameness is the prover value, not its class — the six algebras share one record type and differ only in the calculus they carry, so a class check would register the first and silently drop the other five.

ask clj

(ask kb goal)

(ask kb goal context)

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

No rule expansion. Nothing in the registry backchains, so ask answers from what the KB stores or has cached and never opens a proof search. That is what makes its cost a property of the goal rather than of the rule graph, and it is why the closed-world readers (exceptWhen, unknown, thereExists, the aggregates) can run the same registry from inside a relabel loop. A set/backwardRule's conclusion exists only while a backchainer is looking for it, so ask does not see one: reach for query with a :max-depth, or prove.

ask-within clj

(ask-within kb goal budget)

(ask-within kb goal context budget)

Anytime ask: answer goal in context, but 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} (see vaelii.impl.budget): :results are the solutions realized in this step, :status is :complete / :timeout / :capped, and :resume (nil when :complete) continues the same search under a fresh budget via resume.

:max-ms and :max-results bound how much of the (lazy) answer stream is realized; :max-cost is qualitative — it drops every prover whose cost tier is above the ceiling before the stream is built (:lookup < :compute < :search), so {:max-cost :lookup} answers from cached closures and the index but runs no closure fixpoint and no backward search. A :max-cost that is not one of those three throws (:type :bad-opt) rather than being read as no ceiling: a caller writing :cheap for :lookup is asking to exclude the expensive tier, and quietly running it is the one reading of a typo that is certainly wrong.

Same answers as ask when the budget is generous enough to run dry — the goal prepared the same way included (prepare-goal-for-read), so a NAT or a retired spelling is the same question here that it is there. A bounded run is a strict prefix of ask's stream, so concatenating :results across resume steps reconstructs it.

ask? clj

(ask? kb goal)

(ask? kb goal context)

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

assert clj

(assert kb sentence)

(assert kb sentence context)

(assert kb sentence context opts)

Assert sentence in context (default 'UniverseContext) as a JTMS premise: enforce naming, arg, and disjointness constraints, persist, index (trie + term index), mark IN, integrate into the taxonomy / rule index, then forward-chain. A virtual set/forwardRule|backwardRule|inertRule wrapper directs the enclosed rule. opts flows to chaining ({:max-depth ..}, {:chain? false}) and carries the assumption :strength (:default, the common case, or :monotonic for known-true content that no default may defeat and that is never sent to a solver). A contradiction is resolved softly at settle time, never thrown. A rule that concludes a conjunction is polycanonicalized into one rule per conjunct — then this returns the vector of their handles; otherwise it returns the single sentex handle.

Records provenance for the created sentex: :creator (from opts :creator, else *creator*) and :created (from *clock*), plus any opts :provenance map merged in — read with provenance, extended with add-provenance.

An opts key this fn does not read is refused (:unknown-option), as is a :strength outside {:default :monotonic} — see assert-opt-keys. Both would otherwise store the sentence at a defeat class the caller did not ask for, which nothing downstream can tell from one that was asked for.

assert-inert clj

(assert-inert kb sentence context)

Store sentence in context as an inert sentex — indexed and persisted (so it is inspectable via sentexes-in-context and survives recover) but not a JTMS premise: never believed, never chained, never scanned for contradictions. Returns the handle.

This is the primitive behind a solve's materialized labeling (docs/solving.md): a recorded truth value, not a claim about the base KB. Because every belief-filtered read — sentexes-matching, in?, and the settle nogood scan — sees only IN sentexes, an inert (not head) sitting in a context that sees a believed head forms no nogood and moves no belief. So many labelings coexist and the always-true KB is untouched, with no per-context (ATMS) belief needed — coexistence falls out of not premising.

Only the naming invariant is enforced (a materialized head is already well-formed); no constraint / wff / equality / chaining runs. assert-inert is additive, so no !; drop it with retract! on the returned handle.

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 sentence that expands to several — a conjunctive-consequent rule — contributes its vector, so the result is mapv-shaped, one entry per input sentence).

For a bulk fact/rule load this is the fast path: N asserts, one settle.

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 stamp; 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 :both) — or use a set/*Rule virtual predicate with assert.

believed clj

(believed kb handles)

The subset of handles currently believed, as a set — in? asked of many handles at once. Belief is a label already computed on the JTMS node, so this is one map read per handle either way; what the batch form saves is the call, which for a remote client (vaelii.impl.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.

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?* (skips the per-fact definitional checks — including the argIsa store query — the dedup trie-walk, and provenance) inside one with-deferred-settle (one belief reconciliation at the end), with {:chain? false} so no forward inference runs. This is assert-many stripped of the machinery a trusted corpus import does not need — a corpus load, or the bench wload/w8x/w5x premise setup.

Returns the vector of sentex handles, in input order. The result is identical to loading the same facts one-by-one with plain assert {:chain? false} — same stored sentexes, same index, same beliefs, same count-with-functor — because the skipped work only validates or dedups; it never changes what is stored. The caller owns the two preconditions the mode trades on: every fact is well-formed (the checks would have passed) and no two are the same sentence in the same context (the dedup would have missed). Use plain assert / assert-many when either is in doubt.

opts flows to each assert (e.g. :strength :monotonic); :chain? is forced false — a rule/consequent that needs forward firing is not a bulk-fact load.

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.

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: no sentex, no index entry, no taxonomy edge, no chaining, no settle.

Each problem is a map carrying the :type keyword assert would have thrown, a human-readable :message, and whatever else that check knows (:sentence, :context, :arg / :expected / :position for an argIsa breach, :cycle for a stratification one):

:naming a naming invariant (predicate / individual / type / context) :not-ground a fact still holding a variable :not-well-formed a special predicate's structure (genl, argIsa, the equalities…) :not-range-restricted a rule variable the antecedents never bind :not-stratified a cycle through negation the rule or edge would close :not-assertible a do/ imperative inside a rule :arg-type an argIsa constraint on an argument :disjoint a type membership the taxonomy separates :functional a second, irreconcilable value for a functional slot

plus three that are about the request rather than the knowledge: :shape (the context is not a symbol, the sentence is not an s-expression, opts is not a map), :unknown-option (an opts key assert does not read, or a :strength that is not an assertable class — see assert-opt-keys) and :not-checkable (a top-level do/ imperative — an instruction, which check will not run to find out what it does).

The stages run in assert's order and stop at the first that finds anything, since each later one reads the KB assuming the earlier ones held. A rule is checked the way assert checks it — every conjunct of a conjunctive consequent — and an exceptWhen is checked as the wrapped rule plus the exception's closure.

Two things assert does that check deliberately does not: it does not reify a ground reifiable NAT (that mints a constant, which is a write), and it does not evaluate an imperative. Everything else is the same code on the same KB.

check-edit clj

(check-edit kb batch)

check over a whole edit batch — {:add [[sentence context opts?] …] :remove [handle …]}, the shape edit takes — storing nothing.

Returns a vector of problems, empty when the batch is admissible. Each is what check returns plus where it came from: :in (:add / :remove), :index (the position in that vector) and :entry (what was there), so a caller can point at the line rather than at the batch. An :add is checked against the KB as it stands — an entry admissible only because an earlier entry in the same batch would have landed first is reported, since nothing here is stored. A :remove is checked for naming an actually stored handle (:unknown-handle).

clear! clj

(clear! kb)

Wipe the KB's durable stores — every record and every index entry — 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 shape a reset-and-reload uses. Returns the KB.

clear-violations! clj

(clear-violations! kb)

Empty the accumulated dropped-conclusion ledger. ! because it destroys the diagnostic record — the drops themselves are long final.

conflicts clj

(conflicts kb)

The contradictions the last settle could not satisfy — the reported 'solve result'.

This is irreducible clashes among known-true content and nothing else: two :monotonic beliefs that cannot both hold, where the engine has no grounds to prefer either. Both stay believed — defeating one would be the engine deciding which of your premises to discard — so this is where that decision is handed back. A coexisting pair at :default is not here: that is a represented dilemma, and contradictions reports it. Calling a dilemma a conflict would say the engine failed at something it deliberately declines to do.

Same entry shape as contradictions, down to :kind and both sides' justifications — the two readings differ in why the pair was left standing, not in what a caller needs in order to act on it, and this is the case where there is most to do. Nothing here is stored: a clash is recomputed from current belief each settle and (contradicts X Y) is a report form, never a sentex.

context-down clj

(context-down kb c)

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

context-size clj

(context-size 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.

context-up clj

(context-up kb c)

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

contexts clj

(contexts kb)

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

contexts-of clj

(contexts-of kb sentence)

The contexts in which sentence is asserted.

contradictions clj

(contradictions kb)

The coexisting pairs the last settle left standing — represented dilemmas, not failures.

Two sources, one shape. A rebuttal: two rules concluding opposite literals with neither naming the other's case (the Nixon diamond) is a genuine dilemma — both arguments are equally good, both sides stay believed at :default, and deciding it would be an arbitrary pick dressed up as an inference. And a definitional clash: disjointness, functionality or asymmetry, each of which convicts by naming a second believed sentex, so an equal defeasible pair is a dilemma for the same reason. So the engine represents it and hands the ranking to the application.

Each entry is {:nogood #{h1 h2} :handles [h1 h2] :priority int :kind kw-or-nil :sentence (contradicts ..) :sides [{:handle :sentence :context :defeat-class :justifications [...]} ...]}, carrying both handles and both sides' justifications — the material an argument is made from. :kind names the constraint a definitional clash violated (:disjoint / :functional / :asymmetric) and is nil for a rebuttal; :priority ranks a definitional clash (3–4) above a rebuttal (1–2).

A dilemma is what rebutting defeat leaves behind. Undercutting — "this rule does not apply here" — is written as an exceptWhen on the rule, which blocks rather than rebuts and produces no pair at all (see docs/exceptions.md).

count-with-arg clj

(count-with-arg kb pos term)

How many fact sentexes hold term at argument position pos, as stored — one set-size read, O(1).

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).

default-chain-opts clj

max-depth bounds derivation depth to catch productive infinite recursion; max-derivations is a hard backstop on a single chain run.

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.

dependent-justifications clj

(dependent-justifications kb handle)

Justifications that use handle as an antecedent.

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 cone is told nothing and keeps the name.

disjoint-metatypes clj

(disjoint-metatypes kb)

The declared disjoint metatypes — each a type whose member types are pairwise disjoint by (disjointMetatype 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.

edit clj

(edit kb {:keys [add remove]})

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.

Adds land before removes, and the whole batch settles once at the end, so a datum the removed premises solely-supported but an added one re-derives keeps a witness through the dependency-directed sweep — belief that survives the edit is never swept and rebuilt, and never flickers OUT and back. The final state equals running the asserts and retracts singly; the win is skipping the intermediate tear-down and the N per-op settles. Not a transaction: a throw mid-batch leaves what was already stored in place (the KB stays consistent — only the settle did not run — so settling by hand recovers it).

Returns {:added <one entry per add,assert-shaped> :removed {:removed-sentexes n :removed-justifications n}}. To also learn what the batch turned out to mean — the belief it added and took away — use edit-with-consequences, which is this plus the diff.

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 the belief it took away, in preview's entry shapes. Returns edit's {:added :removed} with :believed-added and :believed-removed merged in.

This is the after to preview's before, and it answers the question a commit leaves open: edit reports the handles it stored, which is what the caller already said, and says nothing about what followed from it.

Where the diff comes from. Not a snapshot of the believed set — that would be O(KB) per write. Every relabel records the region it touched (jtms/touched) and which of that region was already believed when it first touched it (jtms/touched-in); the window spans everything since the last settle finished, so for a batch it covers the whole deferred phase and its one settle. Region plus before-labels plus belief now is the delta, and it is proportional to what the batch moved rather than to what is stored.

preview cannot use this and does not need to: its rollback puts the KB back, so it reads belief-before off the restored KB instead. This has no rollback to read after, which is exactly why the labels have to be captured on the way through.

What the removed half cannot say. A datum the dependency-directed sweep deleted has no record left to describe, so it is omitted rather than guessed at: what is listed is belief that went away and is still stored — defeated, superseded, unsupported. A :remove sweeps, so ask preview what a removal would take with it; it suspends instead of retracting and can still name every casualty. An add-only batch (the common one, and the proposal panel's) has no such gap.

opts is {:max-results n}, capping each half as preview's does.

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)

The cheapest level that answers goal — climb the stack from floor and stop at the first level with results. Returns {:level :name :results :tried}; :results is that level's lazy seq, so the climb costs one result per level tried. Nothing answers → :level nil.

floor defaults to 2, the first level that answers a goal rather than a question about storage: level 1 ignores the goal's arguments and level 0 ignores belief, so either can report a hit it cannot verify. Pass 0 to include them.

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. A diagnostic — it counts, so unlike lookup it realizes every level fully.

This explains the retrieval stack, not belief: it says which machinery reaches a sentence, not why the KB holds it. For that, see why / why-not, which walk the justification graph.

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 "…"}

A dump is a directory of field-map frames — no frame carries a class name — so it survives a backend change, an index-representation change, and a record class rename, none of which the :disk store's own directory survives. What it holds is what the record store holds, because everything else is derived: the index is a cache (reindex), belief and the taxonomy are recomputed (recover). Read back with vaelii.impl.io.import.

opts: {:variant :records|:records+index :compression :gzip|:xz|:none :chunk-size n :provenance? bool :on-progress f} (defaults :records, :gzip, 10000, true). :records+index writes the index too, as a cache a reader replays only if it can prove it describes the records beside it. :provenance? false drops the per-handle annotation — an open map with no size bound, measured at 57% of the converted engine KB's dump — which the importer already treats as optional, so what is left is a complete KB rather than a partial one. :on-progress is called with {:phase :done :total} at each chunk boundary; a callback that throws is how a caller cancels, which leaves a directory with no meta.edn — and so not a loadable dump.

dir must be absent or empty: a dump merged into another dump is not a dump. Export from a KB nobody is writing — the walk fetches record by record, and there is no snapshot to walk instead.

! although it destroys nothing here: it writes a directory tree outside the process, which is not something the KB can take back.

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 in violations' shape ({:violation :disjoint :detail {:term :held :visible-from :message}}), computed on demand and not filed.

settle reports the same clashes as they arise — what the change just made newly visible — which is the incremental question and the one an author wants while writing. This is the standing question, and it is the one to ask of a KB that arrived all at once: an import rebuilds belief rather than changing it, so nothing is newly anything and the settle pass sits it out (see settle/*rebuilding?*). Reads only; nothing is stored and belief does not move.

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. This is the search a term picker wants: it filters the term roster, so it costs the size of the vocabulary and never a scan of the KB.

opts:

:match :prefix (default) | :substring | :regex :case-sensitive? false by default — a search box should find Dog for dog; ignored by :regex, where the pattern says so itself ((?i)) :limit keep the first n of the sorted answer, so a bounded search is a stable prefix of the unbounded one

q is a string or symbol; under :match :regex it may also be a compiled java.util.regex.Pattern in-process (over the daemon wire, send the pattern's source as a string — EDN carries no regex literal). An unparsable regex throws, like re-pattern itself.

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, and kb is never written, so several forks may share one base and evolve independently.

opts names the fork's own storage, as an ordinary opts map (:backend :memory by default — an ephemeral hypothesis on space numbers nothing else uses; {:backend :disk :dir …} gives a durable one, which can be remounted over the same base later and serves the merged view it was left in). :tms selects the fork's truth-maintenance representation.

The fork's belief is rebuilt, not inherited. Belief is not storage — it is a derived graph over the records — so the fork is recovered over the merged view rather than layered over the base's network. That is one pass over the merged records, which is what recover costs anywhere.

The base is frozen by the mount, not copied: nothing is written and nothing is duplicated, so the cost of taking a fork is the recovery and not the base. The index must be one written over the KvBackend seam (:memory, :dense, :disk); a :columnar index is refused, since a KV decorator would fork its roots and leave its native trie behind.

The front-door policies are inherited, :naming and :constraints both, unless opts names one. A fork is a hypothesis over the base's own content, and a fork that quietly held it to different conventions — or that refused a clash the base would have arbitrated — would answer a different question from the one the caller asked.

forward-chain clj

(forward-chain kb)

(forward-chain kb opts)

Run forward chaining to a fixpoint over every believed sentex, then settle belief (resolve contradictions). Returns {:derived n :truncated? bool}.

opts: {:max-depth n :max-derivations n} bound the run, and :on-progress is a callback the fixpoint calls about four times a second (:progress-every-ms) with {:derived n :pending n} — the one window into a phase that otherwise says nothing for minutes. It may throw to abort the run (a loader cancelling), in which case belief is left unsettled and the KB holds the conclusions the run had already placed.

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.

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).

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. ist is find-or-create, so using it to ask whether something is stored silently asserts it — and then retracting "it" retracts a sentex the caller just made. This asks without writing, which is what you want to turn a sentence into a handle for retract!, in?, why, or supporting-justifications.

Storage, not belief: a stored-but-defeated sentex still has a handle and is returned. Test belief with in?, or use sentexes-matching (which filters it).

A ground symmetric literal also probes its mirror, so (siblingOf Ann Bob) finds a stored (siblingOf Bob Ann).

has-prop? clj

(has-prop? kb kind pred)

(has-prop? kb kind pred context)

Does predicate pred carry the metadata property kind — one of :transitive, :symmetric, :asymmetric, :reflexive, :functional, :decontextualized, :forced-decontextualized? Declared by the corresponding sentex, e.g. (symmetric siblingOf).

Argument-position preservation is not here: (argPreserving P n R) is per position, so like argIsa it is an ordinary stored sentex read through matches-visible rather than a cached predicate property (vaelii.impl.inherit).

With a context, the declaration must be visible from it.

in? clj

(in? kb handle)

Is the sentex handle currently believed (JTMS IN)?

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.

interpreted clj

(interpreted term)

What the engine does with vocabulary term term: {:enforced "where"}, {:inert "why"}, or nil.

:enforced means a code path reads it and the KB refuses, derives, or answers differently because of it — the string names which path. :inert means nothing does, and says why that is the intended answer rather than an omission (most are derived predicate types, which exist so a KB can be queried for what a mark implies; the checks read the mark).

Nil is not "nothing reads it". The question is asked of the engine's own grammar — the terms CoreContext declares — so an ordinary domain predicate is simply not in scope. vocabulary-audit is the whole picture, and what keeps this one honest.

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.

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.

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).

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.

This is the question the solver was asked; conflicts is the part of the answer that could not be satisfied, and the TMS holds the rest. It is recorded rather than recomputed because resolving a tie removes the evidence for it: the defeated side stops matching, so the nogood is no longer derivable (see the KB record).

vaelii.impl.asp.edge/classify reads it to say which of the current beliefs were forced and which were an arbitrary pick among equally good alternatives.

levels clj

(levels)

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

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 + genlContext inheritance 7 :proved full stack

A lazy seq of {:level :handle :sentence :context :bindings}; a field the level cannot supply is nil (levels 5-7 derive answers, so they carry no handle). Each level adds one mechanism to the one below, so an answer that appears at level n and not at n-1 is attributable to that mechanism.

At level 0 a vector goal is taken as an index path directly; anywhere else the goal is a sentence.

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.

open-kb clj

(open-kb)

(open-kb opts)

Construct a KB.

Storage is two independent choices: the records (the ground truth, which must survive) and the index (derived state — reindex rebuilds every entry of it from the records, so it need never be persisted). :records takes :memory or :disk; :index takes :memory, :dense (int postings), :columnar (a native int-token trie) or :disk. :backend is sugar naming a pair, spelled <records>-<index>:

:memory (default) records and index in RAM, keyed by :record-space / :index-space (default 0/1) so a KB rebuilt over the same numbers sees the same durable-within-the-JVM records :memory-dense RAM records + the dense int-postings index :memory-columnar RAM records + the columnar trie index :disk-memory durable records, the flat map index in RAM — nothing but records is written :disk-dense durable records, the dense int-postings index in RAM :disk-columnar durable records, the columnar trie index in RAM :disk records and index persisted to on-disk log/idx stores in a directory (:dir, or derived from the space numbers) that survives a process restart :overlay a fork: a private writable overlay over a shared read-only base, which :base (the opts naming that base) and :overlay (the opts naming this fork's own writable stores) fill in. See fork, which is the ergonomic spelling; this one is for a second process mounting the same frozen base.

:memory and :disk are the two pairs that are one store on both axes, named for the store rather than doubled. That is every legal combination: RAM records under the durable index is refused, since an index outliving the records it was derived from describes records that are gone.

An option this fn does not read is refused rather than ignored, and the space numbers are why: a misspelt :record-space is a key nothing looks at, so the KB would quietly open on the default space and two KBs meant for separate stores would share one — each one's flush emptying the other. vaelii.impl.kb/opt-keys is the roster it is held to, a fork's :base and :overlay maps included.

A derived index over durable records opens empty, so such a KB is reindexed before it is recovered (see :recover? below); the cost is one pass over every stored record per open, which is what not persisting the index buys.

:tms selects the truth-maintenance representation: :reference (default) holds the network as one persistent map, :dense holds it in bitmaps and primitive-keyed maps (3.7x denser, measured — see docs/density.md). Beliefs are identical either way; the dense one trades a reader's consistent snapshot for the density, which the one-writer contract already permits. :naming is this KB's front-door policy, not the build's: :strict (default) refuses a sentence breaking a naming invariant, :warn logs it and stores anyway, :off stores in silence. The conventions are how a symbol's role is read (docs/naming.md), so a KB holding a corpus with spelling conventions of its own — hyphens, a dialect's own case — is not malformed, it is a KB whose door is set differently, and one process can hold both. What no setting moves is the role reading: under :off a name nothing can classify is stored and classified as nothing, never as something else. A bulk path never consults this at all — an import builds records directly — so the two doors are reconciled by a report rather than by a check (vaelii.impl.io.import).

:constraints is this KB's other front-door policy — what a definitional clash does. :refuse (the default) has assert refuse a disjointness or functionality clash outright, and a declaration arriving after the content it convicts report rather than decide. :arbitrate refuses only against :monotonic content: against a :default claim the sentence is admitted and settle arbitrates the pair, and a declaration reaches back over what is already stored — so a violating set lands on the same belief whether the schema or the facts arrived first. A KB naming neither reads the process default (VAELII_ARBITRATE_CONSTRAINTS), which is what lets a whole suite run under one policy. :arbitrate is the one to want for an import, where the schema routinely arrives last; :refuse for a curated KB, where a writer would rather be told no than have belief quietly rearranged. Neither is persisted — the policy is this handle's, not the store's — and under :refuse a recover decides a standing clash that incremental settles left both sides of, since a rebuild's region is every stored sentex (kb/constraint-policies has the full statement).

:provers is an atom of the query prover registry; :solver an atom of the edge solver (see vaelii.impl.solve); :conflicts an atom of the reported contradiction sentences; :program an atom of the last Program solved; :violations an atom of the accumulating dropped-conclusion ledger (see violations / clear-violations!); :contradictions an atom of the coexisting P/¬P dilemmas; :recheck an atom of {rule-handle -> triggers} for the rules whose exception needs re-evaluating and the sentences that moved (or :all); :settle-stats an atom of the settle loop's iteration instrumentation; :chain-stats an atom of {:runs n :last result} for the chaining runs; :opposed an atom of the bodies stored in both polarities (the P/¬P coincidence set settle/negation-nogoods iterates), maintained on every store/remove; :negations an atom of the nogoods each of those bodies currently yields, so a settle re-derives only the bodies it could have moved and carries the rest.

A non-empty store needs recover. A fresh KB over databases that already hold sentexes has an empty TMS and taxonomy: sentexes-matching silently answers nothing (the belief filter), isa? answers false, and the definitional checks pass vacuously — every answer quietly wrong for one forgotten call. The :recover? opt decides what construction does about a non-empty store: :warn (default) logs the problem once, :auto repairs it — recover for a durable index, reindex (rebuild the index from the records, then recover) for a derived one — and false stays silent (for a caller that manages recovery or clearing itself — the web -main, the tests).

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 pinned arrangement; the full set is total ignorance; #{} means the network is unsatisfiable and no goal of that calculus is answered there.

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 stop being premises, belief settles once, the difference is read off, and then every write is taken back. Returns

{:believed-added [{:sentence S :context C :handle h|nil :premise? bool :justification {:informant i :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}

:believed-added and :believed-removed are the two halves of the belief diff, in handle order. The removed half is the interesting one and the one a naive implementation misses: it is where defeat, supersession and the dependency-directed sweep show up, and its :reason is why-not's (:defeated, :superseded, :unsupported). :handle is nil for content the batch created — after the rollback there is no such sentex, and a number naming nothing is worse than nothing. Content that was already stored keeps its handle either way, so a revived default and a defeated one are both still addressable.

:refused is check-edit's verdict, plus any entry that threw anyway when applied (check is a fair account of assert's refusals, not a proof of one). A refused entry is skipped, and the rest of the batch is previewed without it — an admissible batch minus its bad line is what a caller is about to ask for. :violations is what the derivation path dropped during the run — the definitional constraints a derived conclusion would have broken — and the KB's own ledger is left as it was found. :contradictions is the dilemmas the batch would open, and it is here because otherwise the most obvious thing a reviewer can do would report nothing at all: asserting the negation of a believed default withdraws nothing, since a defeasible tie is represented rather than arbitrated (docs/nmtms.md), so both halves of the diff would be silent about a clash the batch just created. Standing dilemmas are subtracted, so what is listed is what the batch is answerable for.

opts bounds the run: :max-depth / :max-derivations are passed to chaining and :max-results caps each half of the diff. :bounded? says one of them bit, so a partial answer never reads as a complete one.

The KB is left byte-identical — same live sentexes, same justifications, at the same handles — which is the property everything else here rests on. What does move: the handle counter (a preview mints handles and they are not reissued), and the chain-stats / settle-stats counters, which record work that genuinely ran.

Cost is the batch's own cost — one settle over the affected region, as edit — plus the rollback, which is a second one. The diff is taken over the relabelled region and never over the believed set, so nothing here scans the KB and a preview is proportional to what the batch touches rather than to what is stored. A batch whose conclusions cascade is expensive because the cascade is, and that is exactly the answer being asked for. Bound it with :max-derivations when that matters.

Not concurrent: a preview is a write followed by its undo, so it holds the single writer for its duration (docs/storage.md, "The single-writer contract").

props clj

(props kb kind)

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

provable? clj

(provable? kb goal)

(provable? kb goal context)

Is goal provable in context? Takes the same single-sentence or vector-of- sentences conjunction as prove; a conjunction is provable iff all its conjuncts are, under one consistent binding of their shared variables.

prove clj

(prove kb goal)

(prove kb goal context)

Backward-chain in context with the simple recur DFS prover; returns a vector of solution binding maps. Type-aware (specificity) and context-aware (only facts visible from context).

goal is either a single sentence — (grandparentOf Tom ?who) — or a vector of sentences, which is a conjunctive query:

(prove kb '[(parentOf ?x ?y) (dog ?y)] 'MantleContext)

Conjuncts are solved with bindings threaded across them, so a variable shared between conjuncts joins them: ?y above must be both the child and a dog. Each solution binds every variable of every conjunct. An empty vector proves trivially (one empty solution).

Conjuncts are reordered for cost (vaelii.impl.plan) — so you don't hand-order them. The most selective literal is run first, measured from the count-aware trie and the argument roots, and each pick re-estimates the rest under the variables it binds (sideways information passing), so ordering adapts as the join proceeds. A rule's antecedents are planned the same way at each expansion.

Ordering is a cost decision and never a semantic one: a conjunction is commutative, so every write order returns the same answer set. The two literals whose position is operational rather than logical are pinned — evaluables (evaluate / lessThan / greaterThan) never outrun what binds them, and a rule's recursive literal stays last so right-recursion is preserved. Solution order within the returned vector is not part of the contract.

query-plan on the same vector shows the chosen order and why.

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}. Returns the same partial-result contract as ask-within, and resume continues from the unfinished goal stack.

:max-depth bounds transformation depth — the number of rule expansions the search may stack — so a runaway or merely deep proof yields a :timeout / :capped partial you can inspect and then resume with a larger budget. (:max-cost is an ask concept — prove runs only facts and rules — and is ignored here.)

provenance clj

(provenance kb handle)

The provenance map recorded for handle — {:creator … :created … …} — or nil if none. assert stamps :creator / :created when a sentex is first created; add-provenance layers on application fields. Removed when the record is retracted.

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 to the base relations still possible between them.

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

A pair constrained to one relation is pinned; a pair with several is genuinely open; an unrecorded pair is unknown (every base relation). When the believed facts are unsatisfiable :consistent? is false, :constraints is the network as stated rather than a tightened one, and :unsatisfiable names the pairs no model satisfies as written — empty when only composition found the clash, which is the case with no single pair to blame.

qualitative-scenario clj

(qualitative-scenario kb calculus context)

One concrete arrangement consistent with everything believed in context — {[a b] → relation}, one base relation per pair — or nil when the believed facts are unsatisfiable. Which arrangement is a function of the facts alone, never of the order they arrived, so it is repeatable and comparable across KBs.

Path consistency leaves a set per pair; this picks one member of every set at once, which is the difference between "nothing rules this out" and "here is a world".

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.

query clj

(query kb goal)

(query kb goal context)

(query kb goal context opts)

Answer goal in context — the front door — 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, exactly as prove takes.

opts makes one decision, and it is 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, deliberately. A bound decides which derivations exist, so a number chosen here would be this namespace quietly answering a question that belongs to the application: find the smallest depth that answers yours and pass it. Without one the answer is whatever needs no rule, which is a real answer and not a degenerate case — most of a common-sense KB's reads are stored facts and cached closures.

The depth may also come from *query-options* :max-depth or inference/*max-depth*, which is where prove reads it from too — so one dynamic binding sets the depth for every read in its scope. opts wins over both. Neither has a default, so a depth bound nowhere stays the no-rule-expansion answer rather than a number nobody chose.

{:proof? true} changes the result shape to [{:bindings … :proof …}], one justification tree per answer — the derivation the search took, reading the way why does (:goal / :via / :because). why explains a stored belief by reading the JTMS; this explains an ephemeral one by reading the search, and the two are deliberately one shape. Needs a depth, since without one no rule was expanded and there is no derivation to show.

Everything else in opts is the node engine's, defaulting from *query-options* — :strategy (vaelii.impl.tactics), :portfolio?, :auto?, :first-result? — and is ignored where no depth sends the query there.

Two things this is not. prove is the unbounded backward chainer: it terminates on the data rather than on a bound, so it answers a chain deeper than any depth you would have guessed, at the cost of facts-and-rules only. sentexes-matching is the belief-filtered index read, and returns sentexes rather than bindings.

query-plan clj

(query-plan kb goal)

(query-plan kb goal context)

How a goal would be answered, at whichever of the two scales the goal has.

A single sentence gives the provers applicable to it with their per-prover estimates — which methods could answer it, what each expects to cost, and which of them actually run. Applicable is not consulted: when one prover may answer the goal alone the engine runs it alone, so every other entry carries :runs? false and a :shadowed-by naming what displaced it. And a prover claiming to be complete can still not run alone, when a source none of them reads bears on this goal — those entries carry :guarded-by naming it, which is what makes a union diagnosable rather than merely visible.

A vector — the conjunctive query prove takes — gives the join plan instead: the conjuncts in the order they will actually run, each with the fan-out it was estimated at, the variables already bound when it starts, and what decided its position — cost, an operational pin (:deferred? / :recursive?), or being a cartesian factor (:isolated?, sharing no variable with the rest and able to multiply it, so it is held to the back on structure and the estimate beside it is not what placed it — a literal matching at most once leads instead). So a surprising plan is diagnosable rather than merely observable:

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

Note the second literal is estimated under the binding the first produced, which is why the pair does not read as a sorted list of independent costs.

query? clj

(query? kb goal)

(query? kb goal context)

(query? kb goal context opts)

Is goal answerable under opts? query, asked for one answer.

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, or for a caller assembling a registry of its own. add-reasoner is the ordinary way in.

reasoners clj

(reasoners)

The names of the optional reasoners, sorted — what add-reasoner takes. calculi describes the six that are relation algebras in full; these two are the rest of the roster.

recover clj

(recover kb)

Rebuild the in-memory JTMS and taxonomy from the persistent stores (records and all indexes are already in the store). Call after constructing a KB against an existing store — e.g. after a restart. The JTMS is rebuilt first so belief is established, then the taxonomy (which reads believed special-predicate sentexes), then belief is settled. Derivation depths reset to 0 (they only bound future forward chaining).

reified-term? clj

(reified-term? term)

Is term a reified non-atomic term — the opaque constant a ground (F a…) under a reifiableFunction 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.

The constant is an implementation of term identity, not a name anybody wrote, so nothing should show one to a reader: this is the gate, and term-expression is what to render instead.

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}.

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 — the equality analogue of genls / specs taking one, and for the same reason: an equality is a sentex, so it holds where it is visible. Dropping an edge can split a class, so the scoped answer is not a filter of the global one but its own election.

reset-settle-stats! clj

(reset-settle-stats! kb)

Clear the settle instrumentation, including the histogram.

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. A :complete result has no continuation and is returned unchanged, 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, so the dependency sweep cannot find it; it is torn down directly through the removal choke point instead. That is complete on its own — nothing rests on an inert sentex (it licenses no justification) and belief cannot move, so no settle is needed; the re-check the choke point queues is vacuous and drains at the next settle.

same-class? clj

(same-class? kb a b)

(same-class? kb a b context)

Do a and b denote the same thing? The complement of a provable (different a b): distinct symbols denote distinct individuals until an equality sentex says otherwise. Scoped by context like representative.

sees? clj

(sees? kb k y)

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

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, :truth, and for a rule :antecedent / :consequent / :direction / :defeasible. Key into it; the concrete vaelii.impl.sentex/AtomicSentex / RuleSentex record class is internal and not part of the contract.

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 context-size over contexts is not the same number — that counts only what is in a context the taxonomy knows, so content in a context no genlContext edge mentions is invisible to it.

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 currently believes; that costs a TMS lookup per handle (O(n)), unlike the unfiltered read.

sentexes-matching clj

(sentexes-matching kb sentence)

(sentexes-matching kb sentence context)

Believed sentexes matching sentence in context (context defaults to ?ctx). Literal (no subtype expansion); use isa? / rules for taxonomic queries, or ask for full inference (see the query-family guide above). Belief-sensitive: a stored-but-disbelieved sentex (a defeated default) is excluded — use sentex/find-sentexes for raw introspection.

Returns a seq of sentex maps. The stable contract is the map keys — :id (the handle), :sentence, :context, :truth, and for a rule :antecedent / :consequent / :direction — so key into the result. The concrete record type (vaelii.impl.sentex/AtomicSentex / RuleSentex) is an internal detail: do not instance?- test it or rely on it, only its keys.

A ground reifiable NAT in the goal is reified to its existing constant first (dedup, never mint), so it matches the stored atomic form; an unknown NAT matches nothing.

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).

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).

set-solver clj

(set-solver kb solver)

Install the edge solver used to arbitrate default/default contradictions, returning kb. Takes a name —

:stub (the default) a deterministic local stub: greedy, one contradiction at a time, so two overlapping pairs can cost two defeats where one would do :asp the real answer-set backend — globally optimal, order-independent, and what conflicts / last-program / brave-cautious classification are for (docs/asp.md). Degrades on its own: native clingo, else the clasp subprocess, else the stub

— or any vaelii.impl.solve/Solver value, for an application with a backend of its own. A name is what the public surface needs: the shipped backends are vaelii.impl.* values, so without this the only way to ask for the real one is to reach past the boundary for it.

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 actually moved (0 = nothing blocked, 1 = one pass sufficed, ≥2 = the fixpoint genuinely iterated), :passes the total loop passes including the confirming one, and :histogram the distribution of :iterations over every settle since reset-settle-stats!.

What it measures is how much of the fixpoint realistic content actually uses: how often a settle iterates past its first productive pass (docs/exceptions.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 Fido). With a context, only edges visible from it are walked.

supporting-justifications clj

(supporting-justifications kb handle)

Justifications that conclude handle (its supporting justifications).

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 (termOfUnit K E) map is not believed.

One hop. An argument that is itself a reified term comes back as its constant, so a caller rendering each term individually (linking it, colouring it) recurses and keeps every level addressable; a caller wanting the whole thing flat calls again on what it finds. One index read per call, belief-filtered like any other.

term-role clj

(term-role term)

The naming role of term, for display / classification — one of :variable (?x), :number, :context, :individual, :predicate, :type, or nil (a string, or a symbol matching no convention). Reads the naming invariants (vaelii.impl.naming) that assert enforces, so a caller — a UI coloring a term, a tool grouping one — can classify it by the same rules the engine validates by. Decided most-specific first: a context name is also CapitalCamel, so :context wins over :individual.

terms clj

(terms kb)

Every term the index is keyed by — the KB's vocabulary: each predicate, individual, type, and context name mentioned by a stored sentex, at any nesting depth. Sorted by name, so the answer is stable and reads the same in-process and over the wire (a sorted set would lose its order to EDN; a vector keeps it).

Read from the term roster, so it is O(terms), not O(sentexes) — and the sort is the only superlinear part, which find-terms pays over its hits alone. A ground compound subterm keys the term index too (find-sentexes takes one), but it is a sentence fragment rather than a name, so it is not part of the vocabulary.

Terms are what is stored: a defeated or unsupported sentex keeps its names here, exactly as it keeps its extent in the secondary roots.

types clj

(types kb)

Every type currently in the genl hierarchy — the nodes of the closure, i.e. every type named by some believed genl edge.

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).

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.

violations clj

(violations kb)

The definitional constraints a derived conclusion would have broken during the last forward-chaining run. Each is {:violation :arg-type|:disjoint|:functional|:not-stratified :sentence S :context C :rule handle :detail {...}}.

:not-stratified is the rule-set constraint rather than one of the three definitional ones: a derived genl / genlContext edge that would give the rule set a cycle through negation (docs/exceptions.md). It is dropped for the same reason and reported in the same place; its :detail carries the :cycle.

The same three checks guard assert, where they throw — asserting content the KB has declared impossible is a caller error. A rule that derives such content is not: chaining is a fixpoint and cannot abort halfway through one without making belief depend on firing order, and the engine's stance is that contradictions are soft. So on the derivation path the conclusion is dropped — no sentex, no justification, nothing believed — and reported here instead of thrown.

:no-placement records a firing whose completed join had no context to land in — no context sees the rule and all its antecedent facts (sibling microtheories).

An :arity entry with a :declared-after detail is a retroactive reach rather than a dropped conclusion: an (arity P n) declaration (or the predicate-type membership saying the same thing) arriving after facts of P at the wrong arity, which the check on the way in could not have seen because the declaration did not exist yet. The facts are still stored and believed — this reports and decides nothing, because the second sentex arity names is the vocabulary entry the conviction is read through and a nogood over the pair would defeat its own premise (docs/taxonomy.md, "What each constraint does in each arrival order").

One entry per declaration, not per fact: :declared-after is the declaration's handle, :count how many stored facts disagree, :sample a few of them, and :truncated whether the instance budget cut the sweep short. Per fact would let one predicate's extent evict the whole ledger, and nothing is lost — unlike an exposure, which reports a visibility that took a change to create, the wrong-arity facts of P are re-derivable from the store whenever somebody wants the list. An event like the exposures below it, so a rebuild files none and a declaration that leaves and revives files it again.

A :disjoint entry with a :visible-from detail is a cross-context exposure rather than a dropped conclusion: two believed memberships each admissible where stated, whose types some context can jointly see as disjoint (settle's exposure pass — the definitional checks refuse a writer only on grounds it can see, and the joint question is answered here). The ledger is append-only about exposures too: retracting the ingredient that exposed a clash does not withdraw the entry, and an ingredient that leaves and revives files it again — each exposure is an event, stamped with its run. :exposure-truncated is that pass being honest about its bound: a separating declaration or edge implicates every instance below its types, one settle enumerates at most settle/*exposure-instance-budget* of them, and a pass cut short says so here instead of reading as full coverage — one entry per settle, with :triggers counting what went unswept and :sample naming a few of them. Per trigger would say the same thing once per trigger, since the budget belongs to the pass: whichever triggers it reaches first spend it and the rest are cut short by arithmetic. A corpus load's closing settle holds tens of thousands of them, against a ledger that keeps the newest 1000.

:non-confluent is a warning, not a drop: a newly asserted schematic equation forms a non-joining critical pair with an existing one, so two rewrite rules disagree about a shared term (docs/equational.md). Nothing is dropped — the normal form stays deterministic — but the conflict is surfaced with the two rules (:rule / :with) and the two forms in :message.

The ledger accumulates: each entry carries the :run id of the chaining run that dropped it (chain-stats counts runs), so a bulk load's drops are still here at the end instead of erased by the next assert. Capped at the newest 1000; every drop is also logged at :warn as it happens. clear-violations! empties it.

vocabulary-audit clj

(vocabulary-audit kb)

Every term CoreContext declares in kb, classified — {:enforced [[term why] …] :inert [[term why] …] :unclassified [term …] :retired [term …] :contradicted [term …]}.

:unclassified is the finding this exists to surface: a declaration that landed in the grammar without anybody deciding whether the engine reads it. :retired is the mirror, a claim about a term the KB no longer declares. :contradicted needs no judgement at all — a term the special-predicate table gives an arm to and the roster calls inert.

Empty in all three on the shipped ontology, and a test holds it there.

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, so an application renders a preview and a feed with one renderer. A standing query's entries carry :bindings as well — which solution moved — and f is not called at all when nothing its goal answers did. context scopes the goal up the genlContext cone like any other read, and a variable ('?ctx) watches every context and binds to the one that answered.

The unit is the settle, and one settle is one call. A batch under with-deferred-settle / assert-many / edit settles once, so it is one event whose halves are exactly what edit-with-consequences reports for the same batch — a conclusion derived and then defeated within the batch appears in neither, because a feed reports what changed and not what happened on the way. A retract! that re-derives what it swept is held to the same net answer.

What does not arrive. A mutation that moved no label (re-asserting a stored sentex). Anything during a preview, which stores, reads and takes it all back — an application told belief changed and then that it changed back learned nothing and has probably already acted. Anything during recover / reindex, which relabel everything, so a feed through one would hand a reconnecting application the whole KB as newly believed. A datum the dependency-directed sweep deleted, which has no record left to describe (edit-with-consequences has the same gap, and preview is what answers "what would this removal take with it"). And a spelling an equality merge displaced: a merge supersedes on the assert path, where no relabel records it, so the displaced sentex loses belief with nothing in the region saying so — edit-with-consequences misses it identically, and preview is again what sees it.

Listeners run after the settle, never inside it. So f may read the KB freely, and may write: an assert from a listener is an ordinary assert that settles and produces its own event, delivered once the current round finishes. Listeners never nest, so a writing listener cannot see a half-relabelled KB — but one that writes on every event it receives is an infinite loop, and the delivery loop gives up after 64 rounds with a warning rather than hanging the writer. A listener that throws is logged and skipped; the settle is already committed and its neighbours still run.

f runs on the writing thread, synchronously, inside the write that caused it. That is what lets it read a settled KB and write like any other caller — and it is why a listener doing real work should hand the event to a queue and return: this engine has one writer, and a slow listener slows it.

Cost. A KB with no listener pays one deref per settle and accumulates nothing. A KB with one pays per relabelled region — never per stored sentex, and never a re-run of the goal — which is what lein perf's feed-listener-scaling holds it to. The entries are built once per event and shared, and a KB whose listeners are all standing queries never builds the full set at all.

A goal whose answer is not a function of the region is refused (:type :not-watchable) rather than watched for nothing: a conjunction, an aggregate, unknown, thereExists, an evaluable, an ist. Reach for those with query on a plain listener — the event says belief moved, and the query says what it is now.

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? A proof tree, as data:

{: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 :because [ <the same map, recursively, per antecedent> ]}]}

Recursion terminates at premises, which are marked :premise? true (with the assumption :strength they were asserted at) and carry no :support — a premise rests on nothing, so there is nothing below it.

Rule sentences are originalized, so variables read as the author wrote them (?x, not the canonical ?var0). The rule handle is lifted out of the justification's antecedents into :rule rather than recurred into as if it were a fact.

Cycles are guarded: the justification graph may contain them, and a handle already on the current path is emitted as {:cycle? true} instead of being expanded again.

A handle that is stored but not believed yields {:believed? false} — ask why-not for the reason. An unknown handle yields {:stored? false}.

why-not clj

(why-not kb handle)

(why-not kb sentence context)

Why does the KB not believe handle? The complement of why, as data:

{:handle h :sentence S :context C :believed? false :reason <keyword> ...}

:reason is one of

:not-stored no sentex has this handle :superseded an equality merge restated it under its terms' class representative, so this spelling is stored but not believed. It lost no argument and kept all of its support — retracting the equality gives it straight back. :superseded-by names the restatement (:sentence, :handle) and the :rewrites that produced it, as {old-term representative}. See docs/equality.md. :defeated the JTMS is forcing it OUT — contradiction resolution ruled against it (see conflicts / last-program) :unsupported nothing currently justifies it: it is not a premise, and every supporting justification has at least one antecedent that is itself OUT. :support lists them with the :missing antecedents; an empty :support means it never had a justification at all.

On :defeated, :contradicted-by lists the believed sentexes that directly contradict this one (its negation, or what it negates). Be aware of what that is and is not: the engine does not record which decision defeated a datum — the defeated set is a set of handles with no provenance, and settle erases the evidence it decided from (the loser stops matching, so the nogood is no longer derivable). So :contradicted-by is recomputed now, not read back from the decision, and it is empty when the winner has since been retracted. It is a strong hint, not a recorded verdict. last-program is the nearest thing to the actual record, and only for a tie that reached the solver.

A believed handle yields {:believed? true} and no :reason.

The sentence arity

(why-not kb sentence context) asks the same question of a proposition rather than a handle, and it exists because exceptWhen produces answers no handle can carry: a blocked conclusion is never created (docs/exceptions.md, "the exception is never stored"), so there is nothing to pass to the handle arity. It adds one reason:

:excepted a rule applies, its antecedents are believed, but its exceptWhen query holds — so it concluded nothing. Reported as {:reason :excepted :rule <handle> :exception <ground sentence> :via <antecedent handles>}: the argument that was built and then discarded, which is what makes an excepted conclusion explicable instead of merely absent.

A stored sentence delegates to the handle arity, except that a stored-but-disbelieved one is checked for an exception first — being excepted is the more specific answer than being unsupported. A sentence that is neither stored nor excepted is :not-stored.

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.

A plain assert settles the JTMS before returning (resolve contradictions, evaluate exceptWhen, refresh supersession); a bulk load therefore pays that reconciliation once per fact. Under this macro each assertion still stores and forward-chains, but the settle is deferred, and one settle runs after body. The result is identical belief — settle is computed from current state, not accumulated, and beliefs are order-independent — for one reconciliation instead of N. Returns body's value.

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

The taxonomy's depth potential is deferred with it (taxonomy/*defer-depths?*). Repairing it as each genl / genlContext edge arrives is proportional to that edge's descendants, so a batch that lifts high nodes re-walks their subtrees over and over — a cost that depends on the order the edges arrive in, which is exactly what a batch is entitled not to pay. A deferred insert lifts only the edge's own source instead (taxonomy/local-lift), which keeps the potential sound for the parent-before-child order a hierarchy usually arrives in; an order that does break it leaves the relation loose, and the closing settle repairs every depth in one pass.

Only the assert path is deferred: a retract! inside body settles eagerly (reviving a defeated default is not part of an assert batch). Nesting composes — an inner with-deferred-settle is a no-op wrapper and the outermost one settles. Not a transaction: a throw mid-batch leaves what was already stored in place; the KB is still consistent (settle only did not run), so re-running or settling by hand recovers a clean state. The depth potential is the one thing repaired even then — see below.