vaelii.impl.sentex — com.vaelii/vaelii 0.1.0

The sentex — Vaelii's unit of knowledge: a sentence paired with the context it holds in (sentence + context = sentex).

A sentence is a logical form written as a Clojure s-expression, e.g. (parentOf Tom Bob). Ground (all constants) or a pattern with variables like ?x. A context names the situation / assumption frame it is asserted within.

The structural connectives not, implies, and and are canonicalized into the record rather than left as data: a sentex carries a truth (:true / :false, with double negation eliminated), and — for a rule — a decomposed antecedent (vector of patterns) and consequent. So the connectives never reach the inverted term index (their heads are stripped, even nested inside a rule — see content-forms), and the positional trie key drops the implies / and rule frame; a negative literal keeps its not there as its polarity, so a rule concluding (flies ?x) and one concluding (not (flies ?x)) get distinct keys.

Beyond the connectives, a sentence is put into a canonical form so that logically identical knowledge is stored once:

• canonical variables — a rule's variables are renamed ?var0, ?var1, … by first occurrence in canonical order, and :varmap maps them back to what the author wrote ({?var0 ?x}), so display can restore the original names.
• canonical literal order — a rule's antecedents are sorted by a structural order (polarity, arity, ground arity, variable degree, shape), falling back to a lexical comparison of constants only as the last resort. Variables compare by their canonical index, never by name.
• symmetric arguments sorted — (siblingOf Bob Ann) and (siblingOf Ann Bob) canonicalize to one sentex when siblingOf is declared symmetric.
• comparison siblings folded — greaterThan is stored as lessThan with its arguments reversed, so only the < direction is ever stored.
• comparison chains collapsed — lessThan is variable-arity, and chained comparisons in a rule merge: (lessThan ?a ?b) + (lessThan ?b ?c) becomes the single literal (lessThan ?a ?b ?c). different gets neither fold: it is not transitive, so a merged chain would claim more than was asserted.

An exceptWhen exception does not touch the rule record: it is stored separately as a meta-sentex naming the rule by handle (see the RuleSentex field notes below).

:sentence holds the canonical, readable form for display and matching.

A sentex is one of two records — AtomicSentex (an atomic sentence: a fact, a metadata declaration, a query pattern) or RuleSentex (an implication) — so an atomic sentex does not carry the rule-only slots (there are 100M+ of them), and each still round-trips through nippy with its type intact.

*min-indexed-depth* clj

How deep inside a content literal a ground compound must sit to earn its own inverted-index key — 0 being the literal itself, 1 a subterm of it, and so on.

The default 1 drops each literal's own whole-compound key. That key is what makes the token dictionary fact-scaled instead of vocabulary-scaled: a fact's body is a subterm of itself, so it mints one key holding exactly one handle, per record. Over a 12,070-record corpus of 511 names, 12,054 of the 12,565 distinct tokens are those keys; in the shipped starter, 1,108 of 1,383 — against 4 compounds that are genuinely nested. At the floor and deeper the nesting is what a probe is for: (sentexHandle H) inside an exceptWhen meta, the sentence inside an (ist Ctx S).

2 and up also drop that wrapped sentence — the corpus where the nesting is itself per-record — at the cost of the read ist exists to serve, so the corpus decides. 0 keys every compound, the literal included.

It is read at write time, so moving it over a populated store changes what the next sentex is indexed under and leaves the keys already written where they are: a posting outside the new bound is stale rather than wrong (every read fetches the record, and a dead handle drops out there), and reindex is what applies a new setting wholesale. The token ids themselves are content-keyed and durable — a store keeps the ones it no longer mints, which is not a migration.

*symbol-pool-limit* clj

The most distinct symbols the pool holds before it is cleared wholesale. Sized well above any real vocabulary — the shipped ontology plus the whole of OpenCyc is ~188k constants — so a KB that only ever names things never reaches it and keeps every name shared, which is the entire point of the pool. A cap a normal load could touch would throw away the sharing it exists for; this one is reached only by a minter running per fact. Dynamic for the reason taxonomy/*scoped-memo-budget* is: the only way to exercise the flush is to make it happen.

aggregate-body clj

(aggregate-body form)

The query an aggregate reduces the solutions of.

aggregate-functors clj

The five aggregation operators, mapped to the reduction each names. Every one has the same shape — (<op> ?n ?v <body>), four elements — so one prover answers all five and one frame arm covers them everywhere a form is walked.

aggregate-value-var clj

(aggregate-value-var form)

The variable an aggregate reduces over — the one projected out. Nil when the slot holds something that is not a variable, which wff refuses separately.

aggregate? clj

(aggregate? form)

Is form an (<aggregate-op> ?n ?v <body>) literal?

and-functor clj

assumption-rule-wrapper clj

(set/assumptionRule (implies …)) — the rule's head is a choice offered to a solve, not a truth to derive. Canonicalizes into :assumption; the rule never forward-chains into belief and is consulted only when grounding a solve (docs/solving.md).

body clj

(body {:keys [sentence truth antecedent]})

The positive atomic form a sentex asserts (a fact's sentence without its not); nil for a rule.

canon clj

(canon x)

Canonicalize a sentence to a single sequential representation (PersistentList, recursively), interning every symbol through symbol-pool on the way. Substitution and reads produce lazy seqs / vectors that are = but freeze to different nippy bytes; canonicalizing before anything reaches a key or value keeps trie keys and dedup stable, and the interning collapses the repeated vocabulary to shared objects — the trie key reuses them for free, since it passes constant symbols through unchanged.

canonical-conjunction clj

(canonical-conjunction literals)

(canonical-conjunction literals start)

[canonical varmap] for a conjunction: every variable across all of literals renumbered ?var0 ?var1 … by first occurrence under one shared numbering, and the map from each canonical name back to the name it replaced.

One numbering across the whole conjunction, not one per literal — a variable shared between two literals is what joins them, and numbering them apart would break the join into two questions.

The point of canonicalizing a conjunction (rather than a rule, which canonicalize-rule already does at storage) is identity: two conjunctions that differ only in what their variables are called become the same value, so a search that reaches one twice can recognize it. varmap is how a solution found in canonical space is carried back to the names the caller used — applied with rename-vars, which is one pass because this map can be a permutation.

start numbers from ?var<start> instead of ?var0, which is how a form is renamed clear of another one whose variables are already numbered ?var0 … ?var<start-1>: the two namespaces become disjoint by construction rather than by inventing decorated names. A stored rule is spelled ?var0 ?var1 …, so unifying one against a conjunction spelled the same way needs exactly this before it can mean anything.

chained-comparisons clj

Variable-arity, transitive comparisons whose chains collapse into one literal: (lessThan ?a ?b) + (lessThan ?b ?c) ⇒ (lessThan ?a ?b ?c).

check-exception-closed clj

(check-exception-closed antecedents exception)

Throw unless the exceptWhen exception is closed over antecedents: every variable it mentions is bound before it runs, so it is a ground existence check rather than a search for bindings. The mirror of rules/check-range-restricted, pointed at the exception instead of the consequent.

This forbids an existential exception — "birds fly unless they have a sick child" is not expressible, because ?child would be unbound. docs/exceptions.md records that as a deliberate limit and the price of the ground check; the workaround is an antecedent that binds the witness.

check-naf-closed clj

(check-naf-closed antes conseq exc)

Throw unless a rule's negation-as-failure antecedents are usable — the mirror of check-exception-closed, pointed at unknown / thereExists:

• unknown is closed. Every free variable of an (unknown S) antecedent (the ones a nested thereExists does not bind) is bound by a generator antecedent — a positive literal that produces bindings, which a standalone thereExists becomes once desugared, but which unknown and the evaluables never are. unknown produces no bindings and consumes them, so reaching one before its inputs exist tests an open sentence and silently yields nothing; forbidding it makes the mistake a legible error instead.
• Every quantifier is local. A thereExists bound variable appears nowhere in the rule outside its own thereExists literal, so it cannot leak into the consequent (a range-restriction hole) or capture another literal's variable (a silent misjoin). Both read as working code, so both are refused here.
• An aggregate is closed and its reduction variable is local. Same two rules, for the same two reasons: (agg/count ?n ?v (ancestorOf ?v ?x)) groups by ?x, so ?x must be bound or the census is of the whole relation, and ?v is projected out, so a ?v in the consequent would be a range-restriction hole that range-problems cannot see (it reads occurrences, and ?v occurs).
• The reduction slot holds a variable. (agg/count ?n Ada Body) reduces over nothing — no prover claims it, so the rule stores and can never fire, which is the one outcome worse than an error.
• Every deferred literal's inputs are bound. A computed literal reaching the join without them cannot be answered or refuted, and the chainer throws rather than reporting a comparison that never ran as one that failed — mid-fixpoint, where a throw is exactly what the derivation path must not do. So the rule is refused here, before anything is stored.

What counts as bound is a generator antecedent's variables plus what the deferred literals themselves write: an aggregate's ?n and an evaluate's output. That is what lets a count be compared ((and (person ?x) (agg/count ?n ?c (childOf ?x ?c)) (lessThan 2 ?n))) — the reading that made aggregation worth having, and one the generator-only rule refused by counting the aggregate as a consumer only.

A written output binds only the literals written after it, because that is the order every chainer runs them in: canonical order holds a deferred literal in the author's position, so (and (evaluate ?z (+ ?q 1)) (evaluate ?q (+ 1 1))) is refused and always was. An aggregate is no exception — reordering the placement phase so a comparison could sit above its own count is something the forward chainer could do and the backward one could not, and two chainers disagreeing about one rule is worse than asking for the obvious writing order.

comparison-siblings clj

Comparison predicates that fold onto a canonical sibling by reversing their arguments, so (greaterThan A B) is stored as (lessThan B A). Add a pair here and both directions canonicalize to one literal.

constraint-rule-wrappers clj

(set/hardConstraint (implies …)) / (set/softConstraint (implies …)) — the rule's head is a contradiction marker and its body a conjunctive nogood over background facts and choice-head patterns. Canonicalizes into :constraint (:hard / :soft); like an assumptionRule the rule never forward-chains, and a solve grounds its body (docs/solving.md). A hard constraint renders as an ASPIF integrity constraint (models violating it are excluded); a soft one as a minimized violation.

content-forms clj

(content-forms sentex)

The connective-free literals a sentex is indexed and searchable by: a rule's antecedents and consequent, or a fact's positive body — each with its structural connective heads stripped, so not / implies / and never reach the term index.

An exceptWhen exception is a separate meta-sentex, findable by the rule handle it names (its (sentexHandle H) is a ground compound the term index keeps); a rule's own content never mentions it. The exception re-check index ([:exception-index <predicate>]) is what answers "which rules watch this predicate".

default-rule-wrapper clj

deferred-input-vars clj

(deferred-input-vars g)

The variables a deferred literal must have bound before it can run.

unknown and the aggregates read free-vars, which already knows to subtract a quantifier's own binder — an aggregate's ?v is projected out and its ?n is written, so neither is an input. Everything else reads every argument it does not write.

deferred-literal? clj

(deferred-literal? l)

Is this literal one of the deferred (evaluable) ones? Public because the storage canonicalization here and the query planner (vaelii.impl.plan) must hold back exactly the same set — if the two ever disagreed, a planner could hoist an evaluate above the literal binding its arguments, which yields no solutions rather than an error.

deferred-output-vars clj

(deferred-output-vars g)

The variables a deferred literal binds — evaluate's first argument, an aggregate's ?n, and nothing at all for a pure test like lessThan or different.

deferred-predicates clj

Predicates that consume bindings rather than produce them — evaluable tests and computations. Antecedent order is operational for these: (evaluate ?z (+ ?x ?y)) can only run once ?x/?y are bound, so they must stay after the literals that bind them. Canonical ordering therefore keeps them last, in the author's relative order (one computation may feed the next).

different is here for the same reason and no other. It is a ground-only test over the equality closure (vaelii.impl.provers), so a different antecedent sorted ahead of the literal that binds its variables is not merely slow — it is inapplicable, and the rule silently stops firing.

Being deferred is all different shares with the comparisons: it is deliberately absent from comparison-siblings and chained-comparisons below. The obvious analogy is wrong. lessThan merges chains because it is transitive — a<b and b<c give a<b<c for free — whereas different is not: A≠B and B≠C say nothing whatever about A and C, so merging (different A B) with (different B C) into (different A B C) would manufacture a pairwise claim nobody asserted. The only sound merge would be a clique (every pair present), which is more machinery than the feature is worth. And since different is never stored, there is nothing to canonicalize for: canonical form exists so that logically identical knowledge stores once, and this stores never. See docs/equality.md.

unknown is here for the same operational reason: (unknown S) is negation as failure — it holds exactly while S is not derivable — so it consumes the bindings its argument's free variables need and produces none. Reaching it before those bindings exist would test an open sentence, which is meaningless, so like different it is pinned after the generators that bind it (docs/naf.md). Its argument's quantified variables (a nested thereExists) are not among the ones that must be bound — that is the whole point of the quantifier — so the pinning and closure logic reads free-vars, not every variable. thereExists is deliberately absent: a standalone positive (thereExists ?x S) antecedent is desugared to S with ?x a local generator variable (see the constructor), so it never reaches the chainers as its own literal; only unknown does.

The quantity comparisons (sameQuantity / quantityLessThan / quantityGreaterThan / quantityLessThanOrEqual / quantityGreaterThanOrEqual) are deferred for the evaluate reason: QuantityProver (vaelii.impl.provers) computes them from two ground measure terms, so a comparison sorted ahead of the literal that binds its measure variable is inapplicable and the rule silently stops firing — pinning it after its binders is what a rule antecedent like (quantityGreaterThan ?q (QuantityFn 100 Kilogram)), whose ?q a (mass ?o ?q) produces, needs. Like different, being deferred is all they share with the arithmetic comparisons: they are absent from comparison-siblings and chained-comparisons above. sameQuantity is symmetric, not directional, so it folds onto no < sibling; and while quantityLessThan is transitive, a measure chain crosses units, so collapsing (quantityLessThan a b) + (quantityLessThan b c) into one variable-arity literal would smuggle in a normalization the prover has not run — the same over-eager analogy the different note warns against.

The aggregates are deferred for the sharpest version of the reason: an (agg/count ?n ?v (ancestorOf ?v ?x)) is a census taken of a group, and which group is decided by ?x, so running it before a generator binds ?x would count the whole relation instead of one node's share. Pinning it after its binders is also where GROUP BY comes from — the aggregate runs once per binding of the variables the generators supply, and yields one ?n each (docs/aggregate.md).

desugar-there-exists clj

(desugar-there-exists antes)

Rewrite a rule's antecedent list, replacing every standalone positive (thereExists ?x S) with its body S. A standalone existential antecedent is exactly S with ?x a fresh local variable that the match binds and that (by locality) reaches nothing else — so S alone is the faithful, native reading, and it needs no special matcher: it joins the store like any generator, one witness per solution. A thereExists under unknown is a NAF query, evaluated by the prover, and is not touched here.

do-form? clj

(do-form? form)

Is form a do/ imperative?

Used both to dispatch one at the top level of assert and to refuse one anywhere it would run inside a fixpoint — a rule antecedent, a rule consequent, an exceptWhen query, or anything derived. Forward chaining's defining property is that the same knowledge in any order yields the same beliefs; an imperative firing during it would run a number of times that depends on firing order, and would mutate the KB the fixpoint is still computing over. That breaks order independence and locality at once (docs/nmtms.md), so do/ is legal only where a caller put it: at the top level of an assert, once, after settling.

do-namespace clj

The namespace marking an imperative — a form given to assert that instructs the engine to do something rather than stating that something is true. (do/labeling Ctx) is the first (docs/labeling.md).

It parallels set/, which sets a field on the rule it wraps, and ist, which is likewise given to assert and likewise never stored. Nothing in the do/ namespace is ever a sentex: there is no fact to store, only an action to take.

dot-marker clj

except-functor clj

(except <handle>) — a meta-sentex removing visibility of the sentex the handle names from the context it is asserted in and that context's descendants (everything that sees it). A ground fact — the handle is ground — belief-following like any other, so retracting or defeating the except restores the hidden sentex.

except-wrapper clj

(exceptWhen <query> <rule>) — the rule does not conclude for a binding its exception holds of. Unlike the other wrappers this one takes two arguments and captures one: the query. The wrapper is split off at the assert layer and stored as a (exceptWhen <query> (sentexHandle <rule-id>)) meta-sentex naming the rule, rather than folded into the rule record (see exceptWhen-meta).

exception-conjuncts clj

(exception-conjuncts form)

Normalize an exceptWhen query to its one internal shape — a vector of literals, all of which must hold. A conjunction is written as a vector, the way core/prove spells one; a single literal may be written bare.

exception-query-conjuncts clj

(exception-query-conjuncts sentence)

The conjunct literals of an exceptWhen meta-sentence's query — the inner (and …) unwrapped, or a bare single literal as a one-element vector. The inverse of exceptWhen-meta.

exceptWhen-meta clj

(exceptWhen-meta conjuncts rule-id)

The exceptWhen meta-sentence for conjuncts (a seq of literals, all of which must hold) qualifying the rule at rule-id. A single literal is stored bare, several as an (and …) — canon-stable either way (a vector would flatten to a list and lose the shape).

exceptWhen-meta? clj

(exceptWhen-meta? sentence)

Is sentence a (exceptWhen <query> (sentexHandle <id>)) meta-sentex — the stored form, whose second argument is a handle (as opposed to the (exceptWhen <query> <rule>) wrapper, whose second argument is a rule form)?

exceptWhen-rule-handle clj

(exceptWhen-rule-handle sentence)

The rule handle an exceptWhen meta-sentence names.

exists-functor clj

free-vars clj

(free-vars form)

The variables of form that must be bound before it can be evaluated — every variable it mentions, minus any bound by a thereExists quantifier within it. unknown is transparent (it binds nothing), a thereExists subtracts its binder, and every other form contributes all of its variables. This is what the closure check and the planner read for a NAF literal instead of the raw variable set: the point of (unknown (thereExists ?x (parentOf ?x Tom))) is that ?x is not one of the variables an antecedent has to supply.

ground-term? clj

(ground-term? t)

True when t contains no pattern variable anywhere.

ground? clj

(ground? {:keys [sentence]})

True when the sentence contains no pattern variables (anywhere, nested).

handle-id clj

(handle-id form)

The sentex id a handle names, or nil when form is not a handle.

head-exists-body clj

(head-exists-body form)

The consequent C inside a head (exists <vars> C).

head-exists-vars clj

(head-exists-vars form)

The existential variables a head (exists <vars> C) introduces, as a set — a single variable or a sequence of them (quantified-vars reads either shape).

head-exists? clj

(head-exists? form)

Is form a head existential (exists <var-or-vars> C)?

implies? clj

(implies? form)

Is form a rule form (implies <ante> <conseq>)?

index-terms clj

(index-terms sentex)

The distinct terms that make a sentex findable: the atoms of its connective-free content at every depth, plus each ground compound between *min-indexed-depth* and max-indexed-compound. The sentex's context is added separately by the index.

indexable-term? clj

(indexable-term? t)

A subterm worth an inverted-index entry: a non-variable symbol (predicate, individual, type, context) or a fully-ground compound. Numbers, strings, and variables are dropped — useless lookup keys that only bloat the index.

intern-deep clj

(intern-deep x)

x with every symbol replaced by its pooled instance, preserving shape — a list stays a list and a vector a vector. canon is the other half of the same pair and flattens both to a list, which is right for a sentence and wrong for anything already canonical that is being rebuilt from bytes: a rule's :antecedent is a vector and a [::subterm k] marker must stay one.

So this is what every path back into memory uses — the record frames (vaelii.impl.disk.codec) and the index snapshot's token dictionary (vaelii.impl.disk.index-snapshot). Without it a thawed structure holds a private copy of every name it mentions, which on a store whose whole point is that the vocabulary is written once is the one cost that must not be paid per record.

intern-sym clj

(intern-sym s)

The pooled instance of symbol s (or s unchanged when it is not a symbol). Interning changes identity, never equality, so a pooled ?var0 still matches a fresh one as a binding key.

The size check rides the miss path, so a repeated name pays a bare .get and only a genuinely new one consults the count. A reader whose .get loses a race with a concurrent clear falls back to its own instance: a missed sharing, never a wrong symbol, which is the same reason the wholesale clear is safe at all.

ist clj

(ist context sentence)

The reified (ist <context> <sentence>) term — like ist in the literature. It embeds a sentence (and its terms) inside another sentex; with the term index the wrapped sentence is findable from a sentence.

ist-functor clj

key-stream clj

(key-stream body)

The structural token stream for a fact body: the functor at the top level (no leading marker, so the [pred …] prefix and the [:functor-root pred] functor root stay the trie's first level), then each argument linearized. Deterministic and compound-blind, so it composes with α-rename and dedup unchanged — an atom body degenerates to [body].

max-indexed-compound clj

Largest ground compound subterm (node count) the inverted term index gives its own key — the ceiling *min-indexed-depth* is the floor of. Indexing a huge one stores a key holding the entire subtree (O(size) bytes, a full WAL frame on disk), so a deep ground term would cost O(depth²) index bytes and a wide one a key per level. Above the bound the whole-compound key is dropped and every symbol it contains is still indexed individually (atoms are never capped), so the term stays findable — find-sentexes pays a read for it instead. Scoped to [:term-index]: indexable-term? (which also drives the [:argument-root] argument roots) is untouched.

mentions? clj

(mentions? sentex term)

Does sentex's connective-free content hold term as a subterm? The question the term index answers wherever it has a key, asked of the record instead — the verify half of a compound probe, which turns probe-atoms' superset into the exact answer.

mirror-literal clj

(mirror-literal form)

The argument-swapped twin of a binary literal, for symmetric lookup.

not-functor clj

originalize clj

(originalize form varmap)

Restore the author's variable names in form using a sentex's :varmap ({?var0 ?x}), for display. rename-vars under the name the display path calls it.

path clj

(path sentex)

The full trie path for a sentex: its (connective-free, α-renamed, structurally linearized) key tokens with the context appended as the final level.

peel-rule-wrapper clj

(peel-rule-wrapper form)

Strip the virtual rule wrappers, returning [direction defeasible exception assumption constraint inner]. Wrappers may nest in any order — a defeasible forward rule with an exception, an assumption rule, a hard constraint — and two exceptWhens conjoin. exception is nil or a vector of literals; assumption is true or nil; constraint is :hard / :soft or nil.

positive-body clj

(positive-body sentence)

The double-negation-eliminated positive body of a sentence, or nil when the sentence is genuinely negative. Constraint checks use this rather than the full canonical form: they must see the predicate and argument order the author wrote, not a folded sibling (greaterThan ⇒ lessThan) or sorted symmetric arguments, or an argIsa would be enforced against the wrong position.

probe-atoms clj

(probe-atoms term)

The keys a compound probe narrows by: the indexable atoms it contains. Every sentex holding the compound holds all of them — atoms are keyed at every depth under every bound — so their intersection is a superset of the answer, whatever key the compound itself does or does not earn. A compound holding no indexable atom — no symbol anywhere in it — has nothing to narrow by and probes by its own key: at the default floor it can only occur nested, which is where it has one.

quantified-vars clj

(quantified-vars form)

The variables a thereExists binder introduces, as a set — its second element is a single variable or a sequence of them. A written vector [?x ?y] is accepted, but so is the list (?x ?y) it becomes once canon / variable numbering / goal rewriting have normalized every sequential to a PersistentList — so this must not key on vector?, or a binder would silently stop binding the moment the form was canonicalized. Non-variables are dropped (a malformed binder binds nothing), which makes free-vars treat a bad quantifier as vacuous rather than throwing during a pure construction; the well-formedness check refuses it separately.

rename-vars clj

(rename-vars form m)

form with every variable m names replaced by the name it maps to — one pass, each position rewritten at most once. Unmapped terms are left alone, and a vector stays a vector so a conjunction keeps its shape.

One pass is the whole point, and it is what separates a renaming from a substitution. res/substitute chases: it looks a variable up, then looks its value up, until it reaches something unbound — right for a unifier, whose bindings form an acyclic chain to a term (the occurs check is what guarantees that). A renaming is a permutation, and permutations have cycles: applying {?var0 ?var1, ?var1 ?var0} to (P ?var0 ?var1) must give (P ?var1 ?var0), where chasing would follow ?var0 → ?var1 → ?var0 and never stop. So the two maps look alike and cannot share a function.

This is the operation that carries a form between two canonical namings — the map canonical-conjunction hands back, a rule's :varmap, a cache's rename-back.

rule-antecedents clj

(rule-antecedents form)

The antecedent patterns of a rule form (unwrapping a leading and; a single antecedent needs no and).

rule-consequent clj

(rule-consequent form)

The consequent pattern of a rule form.

rule-direction-wrappers clj

rule-functor clj

rule-sentence clj

(rule-sentence antes conseq)

Build the rule form from antecedent patterns + a consequent pattern — a single antecedent needs no and. This is the spelling the constructor stores (it rebuilds the sentence from the canonical antecedents below), so it is the one builder: rules/rule-sentence delegates here, so a rule reaches the constructor in exactly one surface spelling rather than two that only canonicalization converges.

sentex clj

(sentex sentence)

(sentex sentence context)

(sentex sentence
        context
        {:keys [symmetric?] :or {symmetric? (constantly false)}})

Construct a sentex — an AtomicSentex or a RuleSentex — canonicalizing the structural connectives into the record and the sentence into canonical form (see the namespace docstring). Context defaults to 'default; id defaults to nil until the record store assigns a handle.

opts may carry :symmetric? — a predicate telling whether a functor is declared symmetric, so its arguments can be sorted. Without it no predicate is treated as symmetric (a pure, KB-free construction).

sentex-handle clj

(sentex-handle n)

The handle term naming the sentex stored at id n.

sentex-handle-functor clj

sentex-handle? clj

(sentex-handle? form)

Is form a (sentexHandle <id>) term?

some-symbol? clj

(some-symbol? pred form)

Does any symbol anywhere in form satisfy pred? Short-circuits on the first.

A direct walk rather than some over tree-seq, for the reason chain's free-consequent-vars is one: this runs per stored sentex on paths that ask it of every match in an answer set, the form is usually (pred a b), and the lazy seq tree-seq builds costs several times the three cond arms it describes. Nothing is allocated on the overwhelmingly common false answer.

sort-conjuncts clj

(sort-conjuncts literals)

Put a conjunction of literals into canonical order and drop duplicates, using the same structural comparator the rule canonicalizer uses. An exceptWhen exception's conjuncts are independent ground checks, so their written order (and a repeat) is not their identity — sorting makes two spellings of one exception the same meta-sentex.

subterm-arity clj

(subterm-arity m)

subterm-mark clj

(subterm-mark k)

subterm-mark? clj

(subterm-mark? x)

subterms clj

(subterms sentence)

Every subterm of a sentence — each atom and each compound subterm, recursively, the whole sentence included.

symbols-where clj

(symbols-where pred form)

The set of symbols anywhere in form satisfying pred, or nil when none does. The collecting form of some-symbol?, and nil rather than #{} so a caller can gate on it without allocating for the common empty answer.

symmetric-literal? clj

(symmetric-literal? form symmetric?)

A binary literal whose predicate is declared symmetric (and not a dotted form).

there-exists-antecedent? clj

(there-exists-antecedent? form)

A standalone positive thereExists antecedent — one not wrapped in unknown. These desugar to their body (the quantifier's variable becoming a local matched variable); a thereExists inside an unknown is left intact for the NAF prover.

there-exists-functor clj

there-exists? clj

(there-exists? form)

Is form a (thereExists <var-or-vars> S) existential?

underlying-body clj

(underlying-body sentence)

The body a sentence's not wrappers enclose, whatever its polarity — S for both S and (not S).

Its neighbour above answers the constraint question, where a genuinely negative sentence has no body to constrain and nil is the right answer. This answers the content question: (not (penguin X)) is content about penguin, so a trigger keyed on a predicate has to see it arrive and leave, and a re-check that only ever saw the positive polarity would miss every withdrawal a negation causes.

unknown-functor clj

unknown? clj

(unknown? form)

Is form an (unknown S) NAF literal?

variable? clj

(variable? x)

A pattern variable is a symbol whose name starts with '?', plus the anonymous wildcard _. Variables act as wildcards during index lookup and as logic variables during unification.