Vaelii docs

Per-subsystem notes, one file apiece — read alongside the code. This is the map, and between them these files document the whole engine.

The one-paragraph model

The unit of knowledge is a sentex: a sentence (a Clojure s-expression) plus the one context it holds in. Sentexes live in a record store, keyed by integer handle; they are found through an index store — derived from the records and rebuildable from them — that holds six indexes over the same sentexes: a positional trie, secondary roots (context / functor / argument), a rule index, an exception re-check index, an inverted term index, and the term roster beside it. Two transitive relations — genl over types and genlContext over contexts — are cached as closures and drive type reasoning and context placement. Rules are sentexes too. Belief is maintained by a JTMS with dependency-directed retraction.

What ships is schema: vaelii.impl.starter loads the upper and middle contexts from resources/kb/, and nothing contingent — no cast, no facts of a story — comes with it. Two worked KBs below that schema exercise all this (no doc of their own), and they are test-world data under test/vaelii/: vaelii.world-fables (children's stories as microtheories, each moral derived by a rule rather than stored as a string) and vaelii.world-narrative (a story-understanding ontology layered over the fables — causal / temporal / goal reasoning via predicate metadata and a goal-achievement rule).

Start here

• kbs.md — the four knowledge bases you can load and the route to each: what ships here, what the plugin ships, what you supply, and where a KB has to sit to be found.
• api.md — the public API: every fn on vaelii.core, with what it takes and returns, and the five thin entry-point namespaces beside it.
• glossary.md — every term used across these docs and the code, tagged by subsystem.
• commonsense.md — the questions this KB is asked, one per reasoning subsystem, what the schema had to grow to answer them, and the outside judge that reads the answers back.

Core model & storage

• namespaces.md — the file map: what lives in each namespace under src/.
• canonicalization.md — the canonical form: how sentences and rules identical up to variable names, literal order, symmetric arguments or comparison direction dedup to one handle.
• naming.md — the KB naming invariants (predicates, individuals, types, contexts).
• storage.md — record + index stores, the protocols, nippy serialization, the single-writer contract.
• indexing.md — the count-aware trie, the secondary roots and retrieval from them, the rule index, the inverted term index.
• density.md — the dense backends behind those protocols: tiered int postings, the columnar int-token trie, int-keyed roots, and the record-side codec — what each is measured to buy, and what the measurements refuted.
• overlay.md — forks: a private writable overlay over a shared read-only base, so any number of forks in one JVM share one frozen KB while each keeps its own divergent copy.
• contexts.md — contexts, the genlContext spindle (head / mantle / collector), ist reification, justification placement.
• taxonomy.md — the genl type hierarchy, isa?, disjoint / disjointMetatype.
• inherit.md — argument-position preservation: (argPreserving P n R) / (argPreservingInverse P n R), whether a claim about two kinds reaches their subkinds, the specificity that lets a stated claim undercut an inherited default, the (asymmetric P) that lets a strict one conflict instead, and how a forward rule fires on an inherited claim by naming what the claim was read from.
• argtypes.md — argIsa / argGenl read as entailments as well as constraints: the type an argument declaration says a term has, minted as a derived justified sentex, both arrival directions, and why only a locally-written declaration entails. Off by default.

Inference & belief

• inference.md — rules as sentexes, rule direction, forward/backward chaining, predicate subsumption, incremental matching, the prover engine.
• anytime.md — resource-bounded / anytime inference: the budget, the resumable partial-result contract, the qualitative cost tier.
• levels.md — the lookup-to-query stack: eight named levels from a raw index read to full backchaining.
• abduction.md — abduce: what would have to be true for a goal to be provable, minted as a defeasible hypothesis in a scratch microtheory — the dead-end observer, the grant that gates it, and the isolation that makes an ignored call free.
• exceptions.md — exceptWhen: how a rule states its own exception, and why the exception is never stored.
• naf.md — negation as failure: unknown / thereExists, evaluated at level 6, storing nothing (and why the JTMS out slot stays reserved).
• aggregate.md — aggregation as a query operator: the five reductions over a query's solutions, where GROUP BY comes from, and how a firing that rests on a count is maintained.
• nmtms.md — the non-monotonic TMS: assumption strengths, soft prioritized contradictions, the solver seam.
• preview.md — preview: the belief a batch would add and take away, read off and then rolled back at the same handles.
• equality.md — rewriteOf / sameAs / equals over one belief-following partition, and the different that keeps the unique-name assumption.
• equational.md — symbolic (schematic) equational reasoning: oriented term rewriting by a Knuth-Bendix order, normalizing store and query to one belief-following normal form.
• nat.md — non-atomic terms: reifiable functions reified to opaque NART constants before the index, unreifiable NAUTs kept structural.
• quantity.md — the NAUT-evaluating quantity prover: measure comparison over a dimensionOf / conversionFactor table, with an epsilon float policy.
• skolem.md — head existentials (exists ?y C) skolemized to deterministic NAT constants on forward firing, and the occurs-check in unify.
• qcn.md — the generic qualitative-constraint-network engine behind all six relation algebras: an algebra as a parameter, a network as a value, arc-queue path consistency, entailment and refutation, the support a derived relation carries, and the prover shape every calculus over it shares.
• space.md — the four spatial algebras over it: RCC-8 topology, cardinal direction, relative direction (whose frame of reference is the context) and qualitative distance (whose composition is the triangle inequality over the class bounds).
• time.md — the two temporal algebras over it: Allen's thirteen interval relations, with the composition table written twice so a transcription error is a test failure, and the three-relation point algebra over instants.
• duration.md — the quantitative half of interval reasoning: totalDuration / overlapDuration computed over stored lengths and the unit table, on [lo hi] bounds so an over-approximation renders as an interval and says so.
• stp.md — metric time over the same instants: bounds on the gap between two timepoints, closed by all-pairs shortest paths, with startOf / endOf bridging the numbers back onto Allen's intervals and sharpening an overlap into a figure.
• scenario.md — scenario extraction over any constraint network: one consistent base relation per pair, by fewest-possibilities-first backtracking — lazy, because the count is exponential, and deterministic, because every tie breaks on content.

Contradiction solving (ASP)

• asp.md — the ASP backend behind the solver seam: the ASPIF encoding, clingo/clasp, determinism.
• solving.md — assumptionRules and persistent, inert labeling contexts.
• labeling.md — do/ imperatives and brave/cautious solve.

Interface

• feed.md — watch: an application told that belief moved instead of asking again, off the settle that already computed it — one settle one event, standing queries as a filter over the moved region rather than a re-run, and what is refused because the region cannot answer it.
• operations.md — the operational surface: the cli driver, the headless EDN-over-HTTP daemon that is the single writer, and the zero-dep client threading an explicit connection.
• web.md — the reitit-ring browser for terms, sentexes, and justifications; a term page opens with its shape drawn, server-side and inside a read budget.
• catalog.md — the KB catalog: what a process can load (shipped, generated, corpus, dump, on-disk store), loading one in the background with progress and cancellation, and switching which one every page reads.
• llm.md — the pluggable LLM that reads a KB through generated tools and proposes an edit batch, graded by the engine's own well-formedness checks.
• reading.md — English in: a candidate generator with a reviewer between it and the store, resolving the document's own words against the KB's vocabulary before anything is asked, carrying the span each candidate came from, reporting what it could not translate — and scored against the hand-written fables.
• foreign.md — the formats we read and do not write: no reader ships here, and a bridge is a plugin that declares itself in one edn resource on the classpath.