Glossary

Terms used across the vaelii docs and code. When a term has both an English and a KB-symbol meaning, both are covered.

Each entry is tagged with its subsystem: knowledge representation & ontology · query & rules · truth maintenance · ASP & contradiction solving · qualitative reasoning · storage & indexes.

A

abduciblePredicate : The grant that makes a (P …) assumable by abduce, and the only thing that does — a belief-following taxonomy prop like transitive, but read from the asking context's up-cone rather than universally, because abducibility is a policy of the microtheory granting it. See abduction.md.

Abduction : abduce — what would have to be true for a goal to be provable. Runs the DFS backward chainer, observes the subgoals it could neither match nor expand (res/*dead-end*), and mints the gated ones as :default premises in a scratch microtheory hung below the asking context, so an ignored call leaves the KB as it found it and every answer names its assumptions. See abduction.md.

Aggregation : The five query operators agg/count / agg/sum / agg/min / agg/max / agg/avg — namespaced like set/*Rule, the bare words being ordinary vocabulary. (agg/count ?n ?v Body) binds ?n to a reduction over the distinct ?v satisfying Body, evaluated at level 6. ?v is projected out, one answer or none, nothing stored. In a rule antecedent the aggregate runs once per binding the generators supply, which is where GROUP BY comes from. See aggregate.md.

Allen's interval algebra : The calculus of 13 base relations between two stretches of time — before, meets, overlaps, starts, during, finishes, equal and the six converses. vaelii.impl.interval, registered as :allen. See time.md.

and : The conjunction connective. (and S1 S2 …) holds when every conjunct holds; it is canonicalized into a rule's antecedent vector rather than stored as data. See canonicalization.md.

Antecedent : The premise side of a rule sentex, stored as a vector of literals. Empty for a fact. Canonically ordered and variable-renamed so rules identical up to antecedent order dedup to one handle. See inference.md.

Anytime inference : Resource-bounded query (ask-within / prove-within / resume): realize a lazy answer stream under a budget (:max-ms / :max-results / :max-cost / :max-depth) and report whether it ran to :complete or was cut short. The unrealized tail is the resumable continuation. See anytime.md.

argIsa : An argument-type constraint. (argIsa pred n type) requires the n-th argument of every pred fact to have a type whose genl closure reaches type. Open-world and context-scoped. See taxonomy.md. interArgIsa is the conditional form — (interArgIsa pred n T m U) requires argument m to be a U only when argument n is a T — and it reads open-world in both directions at once: an unestablished trigger leaves it dormant, an unreachable target convicts. See argtypes.md.

argPreserving : (argPreserving P n R) licenses carrying a claim about P's n-th argument across an R-related pair — what makes "the part of a wooden table is wooden" derivable without a rule per predicate. argPreservingInverse reads it the other way. See inherit.md.

ask : The pluggable prover-engine query. It runs the cheapest complete prover alone, else unions the applicable provers cheapest-first by cost tier. See inference.md.

ASP : Answer-set programming — the backend the edge solver renders a contested Program into, solved with clingo (in-process JNA) or clasp (subprocess). Opt-in, with a deterministic stub fallback. See asp.md.

ASPIF : The intermediate text format a Program is emitted to before a clingo/clasp solve. Contested assumptions become choice atoms and nogoods become weak constraints. See asp.md.

AtomicSentex : The sentex record for an atomic sentence — a fact, a metadata declaration, or a query pattern — holding only [sentence context id truth strength]. Split from RuleSentex so a fact does not carry the rule-only slots. See canonicalization.md.

B

Backward chaining : Proving a goal by expanding rules whose consequent unifies with it. Two chainers: prove (a recur DFS over a goal stack with a per-path seen guard, terminating on the data, and prove-seq to drive it a solution at a time) and the node engine (a frontier of whole conjunctions, terminating on a depth bound). Both are type- and context-aware. Nothing in the prover registry backchains. See inference.md.

Bare rule : A plain implies rule. It confers :monotonic justification strength — adding no defeasibility of its own — capped by its weakest antecedent. Contrast a default rule. See nmtms.md.

Base relation : One of a calculus's atomic relations. They are jointly exhaustive and pairwise disjoint, so exactly one holds of any two terms and a set of them is the constraint on a pair — the whole universe meaning "unknown", #{} meaning "impossible". See qcn.md.

Belief : Whether a datum is IN or OUT. A node is IN if it is a premise or has a valid justification, unless it is defeated (forced OUT). Belief is computed from current state, never accumulated, so the same knowledge in any order yields the same beliefs. See nmtms.md.

Brave / cautious : The two readings of a tie the solver leaves open. A conclusion is cautious when it holds in every optimal answer set and brave when it holds in at least one; the committed labeling believes the cautious ones and leaves the merely brave ones OUT. See labeling.md.

Budget : The consumer-side bound on a lazy answer stream that makes inference anytime — carrying :max-ms, :max-results, :max-cost, and :max-depth. See anytime.md.

C

Calculus : A relation algebra plus the predicates that denote its base relations — {:name :algebra :denotation}, what qcn-kb needs to read facts into a network and read entailments back out. Six ship; core/calculi is them as data. See qcn.md.

Candidate : A [sentence context opts] entry read out of English — the shape edit takes, carrying the span of text it came from in its provenance, checked by check-edit and never asserted. Nothing in the engine can say a candidate means what the text said, which is why a reviewer sits between the pipeline and the store. See reading.md.

Canonical form : The normalized shape a sentence is stored in so logically identical knowledge stores once — canonical variables, canonical literal order, symmetric-argument sorting, and comparison folding. See canonicalization.md.

comment : A documentation sentex — (comment <term> "…") — that lets the CoreContext vocabulary document itself in its own representation, read back by core-context/comment-of. See inference.md.

Composition table : r1 ∘ r2 → the base relations still possible between x and z given r1(x,y) and r2(y,z). The one thing a calculus cannot derive from anything else. Three are transcribed and three computed. See qcn.md.

Congruence : Equality's substitutivity: when two names merge, every occurrence of the retired name at any nesting depth is rewritten under the representative. Free here because the term index finds the occurrence and migration rewrites it. See equality.md.

Consequent : The conclusion side of a rule sentex. A rule concluding a conjunction is polycanonicalized into one rule per conjunct. See inference.md.

Constraint network : {[a b] → #{base relations}} over a set of nodes — a value, not a store, read out of the believed facts visible from a context. core/qualitative-network is the public reading of one. See qcn.md.

Context : The microtheory a sentex holds in — every sentex is in exactly one. Contexts form a genlContext hierarchy: a sub-context sees its supers. Names end in Context. See contexts.md.

Contradiction : A believed P and (not P) visible from a common context. A defeasible tie is a represented dilemma — both sides stay believed at :default and the pair is reported by contradictions, not arbitrated. See nmtms.md.

CoreContext : The vocabulary head — the most general context, seen by every other. Loaded by core-context/load-into: every special predicate the engine interprets, each documented by a comment sentex. See contexts.md.

D

decontextualizedPredicate : Metadata deducing every (P …) — asserted or rule-concluded — into UniverseContext, so the fact is visible from every microtheory instead of belonging to one. The target is fixed, not named: the definitional checks are context-scoped and only cover the copy when the stating context sees where it lands. forcedDecontextualizedPredicate is the stronger variant that stores it there by force. See contexts.md.

Default rule : A rule wrapped in set/defaultRule, marking it defeasible. It fires from the same agenda as any rule but confers :default justification strength. See nmtms.md.

Defeasible : Able to be withdrawn when stronger or contradicting knowledge arrives. Default conclusions are defeasible at the edges; monotonic content is not. See nmtms.md.

Defeat-class : The strength tier an IN node sits at — exactly two, :monotonic > :default. A nogood is resolved by defeating the strictly weaker side. See nmtms.md.

Deferred literal : A literal whose position is operational, not logical, so canonicalization holds it in the author's order: the fifteen sentex/deferred-predicates (evaluate, lessThan, greaterThan, different, unknown, the five quantity comparisons and the five aggregation operators) and a recursive rule's recursive literal. See canonicalization.md.

different : Provable exactly when no two arguments share an equivalence class — negation as failure over the equality closure, keeping the unique-name assumption. Variable-arity, ground-only, and not assertible. See equality.md.

Direction : Whether a rule chains :forward, :backward, :inert, or :both. Written with a set/*Rule wrapper that canonicalizes into the record's :direction field; the chainers read the field. See inference.md.

disjoint / disjointMetatype : Declare types share no instance, closed under genl. A metatype's members are pairwise disjoint by being consulted, not by storing the clique. Belief-following. See taxonomy.md.

E

Edge solver : The pluggable Solver that arbitrates only the contested edges of a soft contradiction; known-true content is the fixed background and is never sent. Deterministic stub by default, ASP backend opt-in. See solving.md.

equals : An equality relation feeding the one equivalence closure, sameAs without OWL's individuals restriction. A functional clash derives an equals. See equality.md.

Equational rewriting : An (equals L R) carrying variables, oriented into a rewrite L → R by a reduction order so normalization terminates. Stored and queried terms meet at one normal form, so two spellings of a term reach the same answers without storing both. See equational.md.

Equivalence closure : The cached partition (member → class, class → members and representative) that rewriteOf, sameAs, and equals all feed. Belief-following, content-keyed representative. See equality.md.

evaluate : Symbolic evaluation — (evaluate ?sum (+ 1 2)) binds ?sum to 3 via a safe whitelist, not eval. A deferred literal. See inference.md.

exceptWhen : A wrapper letting a rule state its own exception. For a binding the closed level-6 query holds of, the rule blocks — it does not conclude, so there is nothing to arbitrate. Undercutting defeat. See exceptions.md.

Extent : The set of sentexes at a secondary root — a context, a functor, or an argument position — each set's cardinality being its own stored count. See indexing.md.

F

Feed (change feed) : watch — a listener called with the belief a settle added and took away, in preview's entry shapes, instead of an application re-asking. One settle is one event, so a batch is one call; a standing query is a filter over the moved region and never a re-run of its goal. Silent under preview and recover, and refuses a goal the region cannot answer. See feed.md.

Fork : core/fork — a private, writable KB over another's stores. Reads resolve fork-first and fall through to the base, writes land only in the fork, and the base is never written, so several forks share one base and evolve independently. Implemented by the store decorator in overlay.md.

Forward chaining : The semi-naive fixpoint over one agenda for bare and defeasible rules alike. A new fact fires rules keyed by its predicate and supertypes; a new rule joins over existing facts. Each full match records a justification. See inference.md.

functional : (functional P) plus two symbol values for one first argument derives (equals V1 V2), justified by both facts and the declaration. Two non-symbols stay a hard rejection. See equality.md.

Functor root : The secondary index root [:functor-root pred] — every fact by functor, any arity, either polarity — read via sentexes-with-functor / count-with-functor. See indexing.md.

G

genl / genlContext : The two transitively-closed relations — genl between unary types, genlContext between contexts. Cached as reflexive-transitive up/down closures, recomputed on edge change, belief-following. See taxonomy.md.

H

Handle : The integer id a stored sentex or justification is referenced by, allocated in assertion order. Belief tie-breaks never key on it, or arrival order would leak in. See storage.md.

I

Index (count-aware trie) : The trie a sentex is indexed by: its key tokens then context as the final level, connective-free and α-renamed. Each node carries a count, a child-label set, and the handles at that node. See indexing.md.

ist : "Is true in" — (ist Ctx S) finds-or-creates S in Ctx and returns its handle. Not stored as data; in a rule consequent it places S into the named context. See contexts.md.

J

JTMS : The non-monotonic justification-based truth maintenance system, governed by order independence and locality — every relabel scoped to the affected region, tie-breaks keyed on content. See nmtms.md.

Justification : The stored link from antecedent handles + informant to a conclusion, carrying the strength it confers and the bindings of the firing that produced it. A conclusion is IN if it has a valid justification and is not defeated. The record store holds it; the JTMS holds only the part belief is computed from (jtms/graph-just, which drops the bindings). See nmtms.md.

L

Labeling : Materializing one optimal answer set as belief — every datum in the settled tie assigned :true, :false or :unknown, checked against the brave/cautious classification of the same tie. See labeling.md.

lessThan / greaterThan : Evaluable arithmetic comparators, variable-arity — a ground chain (lessThan 1 2 3) is checked end to end. greaterThan is stored as reversed lessThan. See inference.md.

Levels : The lookup-to-query stack — eight levels (lookup), each adding exactly one mechanism to the one below, from raw index handles to full backchaining. escalate finds the cheapest level that answers. See levels.md.

Locality : The JTMS invariant that no operation recomputes the whole graph — every relabel is scoped to the affected region with the rest held fixed as a boundary. A least fixpoint over the region equals the global one. See nmtms.md.

M

Metatype : A type of types — its members are types themselves, reified under the predicate meta-ontology. A disjointMetatype's members are pairwise disjoint. See taxonomy.md.

Metric time : Numeric bounds on durations and distances between instants, closed by all-pairs shortest paths rather than by a composition table — a simple temporal problem, deliberately not a relation algebra. vaelii.impl.stp, registered as :metric-time. See stp.md.

Migration : The equality-merge step that gives every sentex containing a retired term a rewritten twin under the representative, derived and justified by the original plus the equality, and re-canonicalized rather than textually substituted. See equality.md.

N

Naming invariants : The role conventions — predicates camelCase, individuals CapitalCamelCase, types snake_case (unary predicates), contexts ending in Context. assert rejects a bad name. See naming.md.

NART / NAUT : The two readings of a non-atomic term (F a…). Under (reifiableFunction F) it denotes an object and is reified into an opaque nat/-namespaced constant before it reaches the index — a NART. Under (unreifiableFunction F) it stays a compound to be evaluated — a NAUT. See nat.md.

Negation as failure (NAF) : Closed-world negation. (unknown S) holds iff S is not derivable; (thereExists ?x S) existentially closes and projects. Ground/closed only, never stored, and a negative stratification edge in a rule body. See naf.md.

Nogood : A believed (not X) alongside a believed X wherever some context sees both. Resolved softly by settle on defeat-class, never thrown. See nmtms.md.

not : First-class negation. A (not S) becomes S stored at :truth :false, double negation eliminated; a negative literal keeps its not in the index as polarity. See canonicalization.md.

O

Order independence : The JTMS invariant that the same knowledge asserted in any order yields the same beliefs — belief is computed from state, and every tie-break keys on content, never on handle id. See nmtms.md.

P

Path consistency : The fixpoint that tightens a constraint network: for every triple, intersect the constraint on a pair with the composition of the two constraints reaching it through the third, until nothing narrows. A greatest fixpoint, so it removes rather than adds, and it is order-independent. See qcn.md.

Placement context : Where a forward-derived sentex lands — the maximal contexts that see the firing rule and all its antecedent facts (maximal-common-descendant-contexts). Possibly several, possibly none. See contexts.md.

Plan (conjunctive query planning) : Ordering a conjunction's literals cheapest-first, each estimated under the variables bound by the time it runs (sideways information passing), with the cartesian factors (those sharing no variable with the rest, and matching more than once, so they multiply it) held to the back on structure rather than on an estimate. The cost model is the count-aware trie itself. See inference.md.

Polycanonicalization : Splitting a rule whose consequent is a conjunction into one rule per conjunct, so (implies A (and C1 C2)) stores as two rules and assert returns the vector of handles. See canonicalization.md.

Premise : An asserted datum held IN unconditionally (subject to defeat/supersession), as opposed to a derived conclusion resting on a justification. Carries an assumption strength. See nmtms.md.

Provenance : The per-handle open map kept beside a record — :creator / :created and any application fields — so the record shapes stay fixed. Belief never reads it. See storage.md.

Prover : A registered answering strategy declaring applicable?, est-bindings, a cost tier, completeness, and solve. Transitivity, disjointness, the predicate metadata and the evaluables are all provers; add-prover extends the set. None of them expands a rule — which is what lets a closed-world reader run the registry from inside a relabel loop, and what makes ask's cost a property of the goal rather than of the rule graph. See inference.md.

Q

Query : query / query? — the front door for answering a goal, returning binding maps. One dial: :max-depth says how far to expand rules, and without one the read answers from what the registry reaches and expands nothing. There is no default depth, since a bound decides which derivations exist. Takes a sentence or a vector of them (a conjunctive query joining on shared variables) at any depth. The believed-literal match is sentexes-matching, which is a different question and returns sentexes. See api.md, inference.md.

R

Range restriction : The rule well-formedness rule (rules/check-range-restricted) that every consequent variable must also appear in the antecedent, so a conclusion binds nothing free. A head existential (exists ?y C) exempts the variables it marks and nothing else, so a deliberate ∃ is allowed where a typo is still caught. See inference.md, skolem.md.

RCC-8 : The region-connection calculus of 8 base topological relations between two regions — disconnected, externally connected, partially overlapping, equal, and the two proper-part relations with their converses. vaelii.impl.space, registered as :rcc8. See space.md.

recover : Rebuild the taxonomy and JTMS from the durable stores after a restart, ending in a settle so belief is applied consistently either side of a restart. See storage.md.

Region : The forward consequence closure of what changed — the scope a relabel is confined to, with everything outside held fixed as a boundary. See nmtms.md.

reindex : Rebuild the index store (the trie, secondary roots, rule index, and term index) wholesale from the records, then recover — the repair for a stale on-disk index layout. See indexing.md.

Relation algebra : {:universe :identity :compose :converse} — the base relations, the diagonal, the composition table and the converse map. A parameter to one engine rather than a reasoner of its own, which is why a new calculus is a table and a prover. See qcn.md.

Representative : The elected head of an equivalence class — the head of the rewriteOf chain, else the lexicographically smallest symbol. Content-keyed, so it cannot depend on arrival order. See equality.md.

Rete / TREAT : The opt-in alpha network that keeps facts in RAM indexed by argument value, answering a non-trigger antecedent's join by hash lookup instead of a trie rescan. Off by default behind chain/*matcher*. See inference.md.

rewriteOf : A directional equality — (rewriteOf P D) marks D deprecated and migrates onto P. It names the representative and, being about spelling, may relate any terms. See equality.md.

Rule index : The predicate index keying rules by their antecedent and consequent predicates — both sets complete whatever the direction — so "what could conclude P?" is answerable without a scan. See indexing.md.

RuleSentex : The sentex record for a sentence that is an implication, adding the rule-only slots [antecedent consequent varmap direction defeasible assumption constraint]. Indexed additionally by antecedent/consequent predicates. See inference.md.

S

sameAs : The OWL equality over individuals — reflexive, symmetric, transitive — feeding the one equivalence closure; neither name is deprecated. See equality.md.

Scenario : One concrete arrangement consistent with a network — a single base relation per pair, where the network holds sets. Found by backtracking search over the tightened network, and a function of the facts alone, so it is repeatable. core/qualitative-scenario / qualitative-scenarios. See scenario.md.

Secondary roots : The three single-level index roots the trie's left-to-right narrowing cannot supply — context [:context-root], functor [:functor-root], and argument-position [:argument-root] — each a set whose cardinality is its own count. See indexing.md.

Semi-naive : The forward- chaining evaluation strategy — only newly-derived facts trigger the next round of rule firings, rather than rejoining the whole KB each pass. See inference.md.

Sentence : A Clojure s-expression, ground or a pattern with ?x variables — the sentence half of a sentex. The readable form kept for display and matching. See canonicalization.md.

Sentex : The unit of knowledge — a sentence plus the context it holds in. Every sentex is in exactly one context; a rule is a sentex too. See contexts.md.

settle : The post-chaining fixpoint that relabels belief, resolves each nogood on defeat-class, and re-evaluates queued exceptWhen exceptions until the blocked set stops moving. See nmtms.md.

Sideways information passing : Costing each conjunct under the bindings the already-chosen literals will produce, so the plan reflects the fan-out a literal actually runs with. See inference.md.

Skolemization : Replacing a rule conclusion's existential variable with a term built from the variables the antecedent bound, so the same binding names the same witness twice and a re-derivation does not mint a second one. See skolem.md.

Stratification : The well-formedness rule that a rule set must have no cycle through negation — wff refuses an exceptWhen (or a genl/genlContext edge) that closes one. A purely positive cycle is ordinary recursion. See exceptions.md.

Strength : The assumption strength of a premise / the class a justification confers — exactly two, :monotonic > :default. It propagates from the antecedents: a conclusion is never stronger than what it rests on. See nmtms.md.

Superseded : The TMS state an equality merge puts a stale spelling in — stored but not believed and not matching, subtracting from reported belief rather than forced OUT, so its justified twin survives. See equality.md.

Symmetric arguments : A ground fact of a symmetric predicate stores with its arguments sorted, so both orders dedup to one sentex; a pattern is never reordered, and order-insensitive lookup probes both orders at match time. See canonicalization.md.

T

Taxonomy : The in-memory cache of the genl / genlContext closures, the equality partition, the predicate metadata, and the disjointness caches — all belief-following, reconciled each settle. See taxonomy.md.

Term index : The inverted index [:term-index term] -> #{handles} over every indexable subterm of a sentex's connective-free content, so any sentex is findable by any term it contains (find-sentexes). Numbers, strings, and variables are dropped. Every symbol is a key at every depth; a ground compound is one between *min-indexed-depth* and max-indexed-compound, and outside those it costs find-sentexes a narrowing on its atoms plus a verify rather than a key. See indexing.md.

Term roster : The set of names the term index is keyed by — the KB's vocabulary — held as one index key beside the postings, so terms / term-count / find-terms cost the size of the vocabulary rather than a walk over every record. A name enters with the first sentex to mention it and leaves with the last. See indexing.md.

thereExists : The existential closer — (thereExists ?x S) projects ?x out, so (unknown (thereExists ?x S)) reads "there is no x such that S". A standalone positive one desugars to S with ?x a local matched variable. See naf.md.

thing : The root of the genl type hierarchy — every type reaches thing upward. See taxonomy.md.

Transitivity : The lifeblood of common sense, done by cached closures rather than rules for genl / genlContext, and by metadata-driven provers for a (transitive P) predicate. See taxonomy.md.

U

underlying-body : The body a sentence's not wrappers enclose, whatever its polarity — the content question, where positive-body answers the constraint one and is nil for a genuinely negative sentence. What a belief-reading re-check trigger has to key on, since a defeat stores and removes nothing. See aggregate.md.

Unification : Matching a pattern against a sentence, binding variables — unify / substitute, both handling a dotted rest pattern (?pred . ?args). Type-aware: a sub-predicate or subtype fact satisfies the antecedent. See inference.md.

Unique-name assumption (UNA) : Distinct symbols denote distinct things until an equality sentex says otherwise — preserved even under the equality closure and made provable by different. See equality.md.

UniverseContext : The mid anchor of the context spindle, free for lifted universal facts and the target of decontextualizedPredicate justifications. See contexts.md.

unknown : The negation-as- failure prover — (unknown S) holds iff S is not derivable over the level-6 prover list. Ground/closed only and never stored. See naf.md.

V

Varmap : A rule's map from its canonical variables (?var0, ?var1, …) back to what the author wrote, so sentex/originalize can restore the original names for display. Facts carry none. See canonicalization.md.

violations : The accumulating ledger of conclusions dropped on the derivation path — a failed argIsa / disjoint / functional check, a placement-less firing, or a derived cycle through negation — recorded rather than thrown. See inference.md.

Visibility (genlContext up-closure) : Which sentexes a context can use — those asserted in it or in any context it sees (its genlContext up-closure). Constraint checks and matching are visibility- scoped. See contexts.md.

W

WellContext : The bottom anchor of the context spindle, transitively seeing the whole ontology; the test-world's individuals and fables hang below it. See contexts.md.

WFF (well-formedness) : The structural checks assert runs before storing — that genl/genlContext, disjoint, argIsa, and the equality relations are shaped right and acyclic, plus rule stratification. See naming.md.

why / why-not : Introspection. why returns the proof tree of a believed handle down to premises; why-not explains a stored-but-OUT datum (:defeated / :superseded / :unsupported) or a blocked conclusion. See nmtms.md.