One file per subsystem, read alongside the code. This page is the map, and between them
these files document the whole engine. A subsystem is described in exactly one place; the
model the pages assume is the README, and the vocabulary is
glossary.md.
Sentexes live in a record store, keyed by integer handle, and 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.
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
contexts, 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).
| I want to… | Start at | Then |
|---|
| load a KB and look at it | kbs.md | web.md, catalog.md |
| assert facts and query them from Clojure | api.md | naming.md, levels.md |
| find out why my query answers nothing | troubleshooting.md | contexts.md |
| make a rule fire, and see what it concluded | inference.md | levels.md, contexts.md |
| say "usually, but not when…" | exceptions.md | nmtms.md, inherit.md |
| understand why the KB believes something | nmtms.md | preview.md, feed.md |
| understand why a subsystem is designed the way it is | defenses.md | nmtms.md |
| resolve a contradiction | nmtms.md | solving.md, asp.md, labeling.md |
| keep a KB across restarts | storage.md | overlay.md |
| know what a word in these docs means | glossary.md | |
| build a type hierarchy that behaves | taxonomy.md | argtypes.md, inherit.md |
| reason about time, space or distance | qcn.md | time.md, space.md, stp.md |
| drive a KB from a shell or over a network | operations.md | api.md |
| judge whether a KB's knowledge is any good | quality.md | taxonomy.md, inference.md |
| read another system's KB in | foreign.md | kbs.md |
| write for this engine when I already think in another one | arriving.md | from-cyc.md, from-asp.md, from-prolog.md, from-production-rules.md |
| turn English into sentexes | reading.md | llm.md |
| find the code behind a subsystem | namespaces.md | dependencies.md |
| understand what a query costs | indexing.md | density.md, anytime.md |
| find out what shape of question my KB is asked | profile.md | indexing.md |
| know what a change cost the index, per assert | profile.md | indexing.md |
| see what this KB is for | commonsense.md | |
Every page opens with three bullets — Covers, Not here, Assumes — so a wrong
page costs a sentence rather than a section.
- 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. - troubleshooting.md — indexed by symptom rather than subsystem: an empty query, a rule that will not fire, a refused
assert, a KB holding facts nobody asserted. - 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.
- arriving.md — the way in for a reader with a prior: which orientation page belongs to which background, and the facts that hold whatever you arrived from.
arriving.md routes; these four are the mappings, each one-way orientation
rather than a compatibility claim.
- from-cyc.md — the OpenCyc and ResearchCyc vocabulary:
Mt to context, collections as unary predicates, the four privileged contexts you already have names for, and the argument-type check that gates on the way in. - from-asp.md — answer set programming: choice rules, integrity and weak constraints, the three negations, and the two structural differences — no grounding step, and belief is one labeling rather than a set of models.
- from-prolog.md — Prolog and Datalog: the capitalization that means nearly the opposite here, clause order that is not control, the cut that does not exist, and retraction that reaches what rested on the premise.
- from-production-rules.md — CLIPS, Jess and Drools: a consequent that concludes rather than acts, the conflict resolution that is absent on purpose, and the alpha network that is opt-in with no beta network behind it.
- 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
genlCx spindle (head / mantle / collector), ist reification, justification placement. - taxonomy.md — the
genl type hierarchy, isa?, disjoint / disjointMetatype. - inherit.md — argument-position preservation:
(transitiveInArg P n R) / (transitiveInArgInverse 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.md — rules as sentexes, rule direction, forward/backward chaining, predicate subsumption, incremental matching, the prover engine.
- generators.md — a rule whose consequent is a rule: the hole/own-variable split that needs no declaring, what a firing stamps out, why a mint retracts like any conclusion, and the nesting that lets a level further out fill a functor.
- 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 context — 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.
- defenses.md — the design defenses: why a non-obvious decision across the engine is shaped the way it is and why the tempting alternative is worse, collected out of the subsystem docs so each states the mechanism and links the argument.
- 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 constants before the index, unreifiable applications kept structural.
- quantity.md — the measure-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.
- 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.
- 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. - quality.md —
kb-quality: five readings about the knowledge rather than the engine — which rules never fire, how skewed the predicate extents are, how deep the rule graph's chains reach, how much of the taxonomy reaches a root, which argument declarations name a position their predicate does not have — each off state that already exists, and none of them a gate. - profile.md — the workload instrument: which shapes of question a KB is asked, which index families answer them, what a trie walk costs in node probes, and what one assert or one retraction costs each family — off by default and a deref when off. Also the count-based gate built on it, which fails the suite when a change adds an index operation to either write path, the class
lein perf's ratios cannot see. - 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.
- dependencies.md — which
project.clj dependencies lein antq last reported as outdated, written by scripts/update-badges.sh --deps.