vaelii.impl.inherit — com.vaelii/vaelii 0.24.0

Argument-position preservation — when a claim about one term licenses the same claim about another.

(largerThan dog cat) says something about two kinds. Whether it also says something about a golden retriever and a maine coon is not decidable from the sentence: it depends on whether the relation distributes over the kinds' members. Some relations do (disjoint — subtypes of disjoint types are disjoint) and some emphatically do not (a chihuahua is a dog, a maine coon is a cat, and the maine coon is bigger). So it is declared, per predicate, per argument position:

(transitiveInArg        P n R)   ; a stored (P … w …) licenses (P … a …) when (R w a)
(transitiveInArgInverse P n R)   ; …licenses it when (R a w)

R is any transitive relation — genl and genlCx through their cached closures, or a predicate declared (transitive R) walked over stored facts. A declaration over anything else is refused at assert (wff/arg-preserving-problems): the reach is walked to a fixpoint, so a relation that was never said to compose would have transitivity manufactured for it, and (arg transitiveInArg 3 transitive) cannot say so — arg is open-world, and an untyped relation cannot violate it. Naming the relation is what keeps this from being a genl special case: an argument can equally be preserved along partOf, connectedTo, or anything else transitive. transitiveInArg carries the claim along R's arrow and transitiveInArgInverse against it, the directions of Cyc's transitiveViaArg / transitiveViaArgInverse; the two names exist so neither direction requires declaring an inverse predicate that has no other purpose.

Several declarations may name one argument position; their reaches union, since each independently licenses the claim.

Preservation stays on one side of the type/instance line

genl relates types, so (largerThan dog cat) preserved along genl reaches golden_retriever and maine_coon and stops there. It says nothing about Rex and Whiskers, and that is not a gap here to fill: relation_kind is a disjoint_metatype over type_relation_predicate and instance_relation_predicate, so one predicate symbol relates kinds or instances and never both. A largerThan that inherited across the line would be a predicate of both kinds at once, which the KB's own meta-ontology refuses.

Preservation moves an argument along a relation, leaving the predicate and the level it lives at alone. Crossing the line is a different claim — it links two predicates and has a quantifier reading to pin down (every member? some member?) — and the vocabulary for it is (typeToInstancePred TypePred InstancePred), which records the pairing for a reader and is inferred from by nothing.

Specificity, and why it is not the deleted axis

The interesting case is a claim that inherits and a more specific claim that disagrees. (typicallyLargerThan dog cat) reaches [chihuahua maine_coon]; (typicallyLargerThan maine_coon chihuahua) is stated directly. The stated one wins, and the general one simply does not fire for that pair — undercutting, not defeat. Nothing is derived, so there is nothing to arbitrate.

That matters, because docs/nmtms.md deleted genl-based specificity as an arbitration axis on the grounds that it was inference about the knowledge rather than from it: it scored a type by the size of its up-closure, a numeric proxy that tied silently whenever the exception was not keyed on a narrower type. Nothing here reconstructs an ordering. Two claims are compared along the very relation the inheritance travels down — [maine_coon chihuahua] is below [cat dog] because (genl maine_coon cat) and (genl chihuahua dog) are edges the KB holds. Claims that are genuinely incomparable are not ranked at all; they come back :ambiguous, which is the same answer the engine gives every other unresolvable clash.

Strict versus typical, for free

A :monotonic claim is never undercut. Strength already propagates from a justification's antecedents, so (largerThan dog cat) asserted {:strength :monotonic} inherits as known-true and a contrary specific claim is a contradiction, while (typicallyLargerThan dog cat) at the default :default inherits defeasibly and yields to the specific claim. One declaration, both behaviours, and the difference is stated where it belongs: on the claim, not on the vocabulary.

A stored (not (P a b)), and a stored (P b a) under an asymmetric mark on P or above it, are paired with the inherited claim by discovery/preserving-nogoods, whose members are the general claim and everything the reading rests on, so decide/verdict weighs the set and the weakest member decides (clashing-claim and converse-claim below, docs/inherit.md for the readings).

Ground goals only. An open argument is left to the fact and rule provers, in the shape different and the NAF operators already use — enumerating it would mean walking the inverse reach of every stored witness, which is a different and much larger question than the one a closed goal asks.

*deadline* clj

The System/nanoTime instant a claim walk stops at, bound only by provers/TransitiveInArgProver from budget/*deadline*. nil for every other reader of claims (the asymmetry check at assert, settle, forward chaining), which walk to the end whatever deadline an enclosing ask holds.

*memo* clj

A per-question cache for the two reads every layer here repeats — an atom of {[:positions pred context] -> …, [:reach rel along? x context] -> set}, or nil for no memoization.

Answering one ground goal asks for a predicate's declared positions from applicable?, verdict, surviving and claims, and for a term's reach once per preserved position and then again per pair of claims inside undercut?. Neither answer can change while the question is being answered — a query never mutates belief — so the memo is created fresh per top-level question and needs no invalidation protocol at all. with-memo reuses an outer one when a caller has already opened it, which is the discipline observe/*reach-memo* follows for the transitive closure.

*retrieval* clj

Which of the two paths finds the claims: :auto weighs the extent against the product per goal, :extent and :product force one. The forcing values exist so a test can hold the two against each other on the same KB — they answer the identical claim set by construction (both filter matches-visible by the same in-product?), and inherit_oracle_test is the claim that they do.

channels-read-arguments? clj

(channels-read-arguments? f)

Does moved-channels' answer for a sentence with functor f read its arguments? True for a declaration, transitive, asymmetric, a permuting mark and genl; every other functor's answer is a function of f alone.

claim-reach-extent clj

(claim-reach-extent kb sen pred)

The stored facts of the preserved predicate pred, in either polarity, whose tuple the claim sen (on pred or a sub-predicate of it, in either polarity) can reach by preservation from some context, as a superset: the handles holding at argument 1 one of sen's arguments or a term a believed declaration of pred licenses from one (licensed-terms, read at '?ctx). Every argument order the matcher reads a claim in holds its terms among these, and so does the converse an asymmetric predicate is denied by. nil when an argument is not a symbol or the terms outnumber pred's stored extent, for a caller to read the extent instead.

claim-reading clj

(claim-reading kb goal c context)

The handles of claim c's strongest-reading, c a surviving claim bearing on the ground goal, read at goal's arguments from context: the reading clashing-claim pairs a stored claim with. nil when no declaration reaches.

claims clj

(claims kb goal context)

(claims kb goal context strong?)

Every believed claim bearing on the ground goal (P a1 … an), each tagged with the argument tuple it is stated at and whether it argues :for or :against.

Against comes from two places: an explicit (not (P …)) at a tuple in range, and — when P is declared asymmetric — the converse (P … y … x …), since a relation that cannot hold both ways is denied by its own mirror. The converse is only read for a binary goal, which is the only arity for which asymmetric means anything.

Every probe is made, and one tuple can yield several claims. A tuple where both P and (not P) are believed is a contradiction the KB already reports through (contradictions kb); taking whichever probe answered first would have this read it as a clean :for and hand verdict a decision that the engine, looking at the same two sentexes, refuses to make. Collecting both sends it to verdict as the :ambiguous it is. The price is two probes per tuple rather than short-circuiting on the positive (three for an asymmetric predicate) — the two :against sources are kept separately rather than folded, since they can be believed at different strengths and undercut? reads that per claim.

The converse probe is skipped at a self tuple [a a], where it would read the very sentex the positive probe just read and file it as opposition. That is one fact disputing itself, not two claims disagreeing, and it is the one shape where collecting both polarities would manufacture the dilemma rather than report it. ((P a a) under an asymmetric P is wrong — asymmetry implies irreflexivity — but it is wrong in a way contradictions does not report either, so answering :ambiguous here would be this function inventing a verdict on its own.)

strong? reads the known-true statements alone, which are all a caller keeping only known-true claims needs: undercut? drops none of them, and a tuple's strongest statement is known-true whenever one of its statements is.

clashing-claim clj

(clashing-claim kb sentence context)

The known-true claim that reaches sentence's own tuple by preservation and denies it — {:sentence :context :claim handle :handles [handle …] :class} — or nil.

sentence is a stored fact of a preserved predicate, in either polarity; the claim looked for is the opposite one. A stored (not (P a b)) is denied by a (P w b) above it, and a stored (P a b) by a (not (P w b)) above it, since claims reads both polarities out of the reach.

Known-true, because that is the whole of what undercut? leaves standing. A :default general claim yields to a nearer contrary one: it is undercut, never fires for that tuple, and there is nothing for anybody to report (docs/inherit.md). A :monotonic one is not undercut, so it survives beside the stored claim and the pair is a nogood with no second stored member. This names it.

The claim's own tuple is excluded: a claim stated at the very tuple sentence is about is an ordinary P beside an ordinary (not P), both stored, which the negation family pairs (decide/note-candidate!). A claim stating sentence itself is excluded too: an asymmetric converse carried round a genl cycle to its own tuple is one sentence on both sides (docs/inherit.md).

:handles is the reading's support and not the claim: the declaration that permits each move, the relation edges the reach travelled, the (transitive R) a fact-relation reach is closed under, and the (symmetric …) behind a mirrored reading. One claim is named where several reach (strongest-claim). Asked from the vantage of context: a claim in a context that cannot see the general one is not denied by it.

converse-claim clj

(converse-claim kb sentence context)

The known-true claim that reaches the converse (P b a) of the stored sentence (P a b) by preservation, while an asymmetric mark on P or on a super-predicate of it holds at context — {:sentence (P b a) :context :claim handle :handles [handle …] :class} — or nil. The mark says the two tuples cannot both hold, so the inherited converse and the stored tuple are a nogood as clashing-claim's pair is. A claim stated at (P b a) itself is a stored converse, which the asymmetric family pairs (decide/note-candidate!), and is excluded. The reading and the choice among several claims are clashing-claim's (strongest-claim).

crossing-closure-cap clj

The most closure terms crossing-claim? reads the slot roster at. The closure is specs-global of a genl edge's lower term together with genls-global of its upper one. An edge whose closure holds more is not narrowed: every predicate preserved along genl is moved, read off the declarations' relation index with no index read. The closures are walked through tax/specs-global-within, which stops one term past the cap, so an edge under a type with 20,000 subtypes pays 513 steps and not 20,000.

The narrowing costs a slot-roster read per closure term per preserved position, and the fallback costs a full re-join of every rule on a predicate preserved along genl. The bound keeps the first from growing with the closure: (genl root_t top_t) over 20,000 leaves and one preserved position reads 20,000 slots without it.

declarations clj

The two declaration functors, mapped to the along? flag of the walk that serves them: true licenses a from w when (R w a) (along R's arrow, transitiveInArg), false when (R a w) (against it, transitiveInArgInverse).

declarations-exist? clj

(declarations-exist? kb)

Does this KB declare any preservation at all? One set-cardinality read per declaration functor, false for nearly every KB there is. The forward join's gate: chain/preserving-antecedent? asks it before positions, once per chaining run through chain/*declarations-cell*, so a KB that declares nothing pays O(1) and stops. moved-predicates, licensing-functors and preserved-pairs ask it first as well (declaration-index).

Neither belief-filtered nor context-scoped, for declared's reason — a false is exact whatever anyone believes, since a declaration would be in the root.

declared clj

(declared kb)

Every declaration's [P R] pair — the predicate that inherits, and the relation it inherits along — read off the predicate extents rather than through matches-visible.

Deliberately not context-scoped and not belief-filtered, because the callers are vaelii.impl.special's exception re-check triggers, and a trigger must be conservative in the direction the answer is: a declaration this edge cannot see still qualifies a rule in some context that can, and a missed trigger leaves a conclusion blocked (or unblocked) on evidence that has since moved. Over-queueing costs a level-6 query at the next settle; under-queueing is a wrong belief.

Costs one set-cardinality read per functor on a KB that declares none, which is nearly all of them, and a record fetch per stored declaration otherwise. A negated declaration is in the same predicate extent and drops out on its shape, as does one of another arity.

declared-about? clj

(declared-about? kb pred)

Could any stored declaration name pred? The declaration functors' roots intersected with the argument root at position 1, where a declaration's predicate sits — one set intersection per functor, against a root that is empty for nearly every KB and tiny for the rest.

This is a gate, not an answer: it is neither belief-filtered nor context-scoped, so a true says only that the real read is worth making. A false is exact, because a declaration naming pred would be in that intersection whatever anyone believes about it. That is also what makes it the right question for a conservative caller that wants no answer at all, only "could preservation be in play here": recheck/cross-argument-predicate? reads it to decide whether an exception conjunct's arguments may be compared with a trigger's, where an under-selection is a missed withdrawal.

The gate is for the query path rather than the assert path. positions is read by TransitiveInArgProver.applicable? and by provers/shadowing-channels, so it runs for every goal's functor in the KB, and each real read is two matches-visible calls. Ungated, one declaration anywhere made a genl goal cost 2.8x what it costs in a KB with none — a tax every query pays for a feature almost none of them use.

Two stages, because the two questions have different prices and different answers. The cardinality read is O(1) and false for nearly every KB there is, so it comes first and nothing else runs; the intersection is a real (if small) index read and only a KB that declares something ever pays it.

denial-readings clj

(denial-readings kb sentence)

Each reading of a claim that denies sentence by preservation, read from every context at once, as {:handles :contexts}: the claim and what the reading rests on (claim-supports), and the contexts those are stated in. Empty when nothing reaches sentence's tuple to deny it.

clashing-claim answers from one reader, and a reader that sees sentence but not the claim, or not an edge the reach travels, finds nothing. This is the question asked before any reader is chosen: which handles a reader would have to see for the clash to be in view. discovery/preserving-entry asks the clash from the most general contexts that see each reading with sentence and no except hiding one of them.

Read at '?ctx, which every layer here passes through as unscoped: the matcher reads every context, and the genl walk and the mark reads take every edge and every statement. Over-approximating in both directions it can: every class of claim, and claims undercut? would drop, since a claim undercut in the whole KB can survive in a reader that does not see the claim undercutting it. A reader asked because of a reading named here re-reads the clash on what it sees, so a reading that turns out to convict nothing costs one question.

The claim's own tuple is excluded, as clashing-claim excludes it: a claim stated at sentence's tuple is a stored pair, found by the partner reads that pair stored sentexes. The readings of converse-claim's converse are named too, each joined by an asymmetric statement that makes the converse deny sentence.

ground-goal? clj

(ground-goal? goal)

A closed positive literal this can speak about.

A negated goal is left alone: (not (P a b)) asks whether the claim is refuted, and an inheritance that only ever licenses claims has nothing to say about that — :against here means "not licensed", the open-world reading, not "licensed to be false".

licensing-functors clj

(licensing-functors kb preds)

The functors whose facts move what a preserved predicate in preds (a set, or a map keyed by predicate) licenses, or nil — moved-predicates' channels named as functors rather than asked of one sentence, for a caller that enumerates stored facts to hand to rejoin-rules.

The declaration functors, transitive and asymmetric, and each relation some P in preds is preserved along, with its sub-predicates, since a fact on one is a fact on the relation. A claim on P is not named: its functor is P or under it, and the caller reads those already. The permuting marks are not named either, since the engine lifts each into CxUniverse, where every reader sees it. Two predicate-extent counts for a KB that declares nothing (declaration-index).

The sub-predicate closure is global, for moved-predicates' reason: these name candidates for a re-join, over-selecting costs a join that derives what is already there, and a scoped closure would leave out a relation a context that sees more edges walks.

moved-channels clj

(moved-channels kb sen decls wanted)

moved-predicates' answer for sen over the [P R] pairs decls, split by channel: [claimed other], the predicates a claim on one of them or on a sub-predicate moves, and the predicates every other channel moves. A caller opens a with-memo, which indexes decls once.

moved-goal-test clj

(moved-goal-test kb sen)

A test (fn [goal] → boolean), false only for a goal on a preserved predicate whose verdict, and whether it is stated at its own tuple, sen arriving or leaving cannot move — or nil where no test is read and every goal may have moved: a declaration, transitive, asymmetric, a permuting mark, a genl edge into a predicate some declaration names or sits below, an argument that is not a symbol.

Two channels are read, at '?ctx and over the global genls, the union of what every context reads, since the firings re-decided live in any context. A claim moves only a goal whose product holds its tuple (claims), so every argument of the goal is one of the claim's or a term one of them licenses. A fact on a relation moves only a goal whose reach crosses it, and a walk from the goal's term reaches the fact's first term whether the fact is there or not, so some argument of the goal is an end of the fact or a term one licenses along it (docs/inherit.md).

moved-predicates clj

(moved-predicates kb sen)

(moved-predicates kb sen decls)

(moved-predicates kb sen decls wanted)

The preserved predicates whose licensed claims sen may have moved.

Four channels, and none of them is the predicate-keyed trigger a forward rule is ordinarily fired from:

• a claim on P (or on a sub-predicate of it) licenses a tuple nobody stated, and undercuts one somebody did;
• a fact on the relation R — a genl / genlCx edge included — moves every reach walked along it, with neither of its terms appearing anywhere near P. A genl edge moves only the P with a claim whose reach can cross it (crossing-claim?), reading the claim at every position a permuting mark lets it hold the preserved argument at; an edge whose closure is past crossing-closure-cap moves every P preserved along genl. Every declaration in a KB may preserve along genl, so without the narrowing each edge re-joins all of their rules;
• the declaration itself, which names P at argument 1;
• (transitive R), the licence usable-relation? reads at use, which names no P at all; (asymmetric P), which is what gives a converse the standing to deny an inherited claim; and a permuting mark — (symmetric P), (commutative P), (commutativeInArgs P …), (commutativeInArgAndRest P n) — which makes every permutation it licenses of a stored claim a claim, so arriving late it licenses tuples nobody re-joined for.

The reads are global and not belief-filtered, exactly as declared's are and for the same reason: over-selecting costs a join that derives what is already there, under-selecting is a conclusion that depends on when a sentence arrived. The pairs are declared's, indexed by predicate and by relation (declaration-index, cached on the declaration postings), so each channel reads the pairs it names and the answer costs no pass over every declaration; a KB that declares nothing pays two predicate-extent counts.

The three-argument form takes the [P R] pairs, for a caller holding them already and asking this per member of a settle's region. That caller opens a with-memo, so the pairs are indexed, and an edge in the region narrowed, once per settle however often they are asked about.

permuted-read-supports clj

(permuted-read-supports kb sentence tuple context)

The alternative sets of mark sentexes a read of the stored sentence at the argument list tuple rests on, each a vector of handles, or nil when tuple is the stored argument list or no believed mark licenses the rearrangement.

The matcher reads a stored fact in every arrangement its own functor's permuting marks license (res/raw-match), and a firing reached through one of those arrangements holds only while a mark does. So the reading names them, as claim-supports names the (symmetric …) a mirrored claim came through, and retracting the mark withdraws what only it licensed.

One alternative per minimal set of statements that licenses the rearrangement. A binary (P a b) read as (P b a) under both (symmetric P) and (commutative P) is licensed by either, and a firing naming both would go with the first retracted while the other still licenses it. Two commutativeInArgs statements whose components are both moved license the read together, and that set is one alternative. The statements are those stored on the fact's own functor, since the matcher permutes each fanned literal on its own declaration, and each is named by the believed sentexes stating it that context sees and no other covers, ordered on context name as general-supporters orders them. Where the CxUniverse copy is believed it is the one named: the engine lifts every statement into it, so it stands while any statement does, as the store's sort does. A firing is placed by its rule and the facts it matched and not by the statements named (chain/placement-antecedents), so the copy serves a fact in a context that cannot see it as well as one below it. Naming only a statement the fact's context sees would drop the firing when that statement is retracted while one the context cannot see still sorts the fact.

Read off the taxonomy's supporter sets (tax/prop-supporters, tax/commuting-supporters) rather than through general-supporters: this runs once per mirrored firing, firing_cost_test holds it to no index read, and the matcher reads a mark by its exact functor, so the sub-predicate fan a match would add names nothing.

permuting-mark? clj

(permuting-mark? f)

Is f one of permuting-marks? A set lookup: every placement asks it of its conclusion's functor (special/deduce-lifts).

permuting-marks clj

The marks under which the matcher reads a stored fact in more than one argument order: the functors whose arms install tax/props :symmetric and the :commuting table, which are what res/matches-hierarchical permutes a literal by (sx/commuting-arrangements). A late one moves what a rule's antecedent reaches over facts already stored, so moved-predicates and chain/permuting-rejoin-rules both key on it.

positions clj

(positions kb pred context)

[{:n :rel :along? :handle :in} …] — the preserved argument positions declared for pred, visible from context, whose relation is one this may actually walk. Empty (the overwhelmingly common case) means the predicate inherits nothing and every consumer here is a no-op.

Several declarations may name one position; they are not collapsed here, because their reaches union (reach) rather than compete.

Each carries the :handle of the declaration it was read off, which is what supports-for names when a firing rests on the move it licenses: the declaration is as much a reason for an inherited claim as the claim itself, and retracting it has to withdraw whatever was concluded.

:in is the context the declaration was asserted in, and it is here because move-supports orders the declarations that may license a move by content: [rel, along?, n] fixes the declaration's whole sentence, so two visible statements of it differ only in where they were said, and without :in the order would fall to matches-visible' answer set — handle order, which is arrival order. It costs one record fetch per declaration, paid inside the memo rather than per firing, over a list that is empty for nearly every predicate.

Realized rather than lazy, and memoized on [pred context]: four layers of one question ask for this, and each computation is two matches-visible calls.

Behind a root-intersection gate on any declaration naming pred at all, so a predicate nobody declared about — which is every predicate but a handful, in every KB — pays one intersection against an empty root rather than two index lookups. The same shape of gate special.clj puts in front of the exception re-check triggers, for the same reason.

preserved-pairs clj

(preserved-pairs kb)

Every stored declaration's [P R] pair (declared), off declaration-index, or nil when none is stored.

rejoin-rules clj

(rejoin-rules kb sen)

The forward rules to re-join in full because sen moved what a preserved predicate licenses — every rule carrying an antecedent on one — or nil.

Keyed on the antecedent index rather than on the arriving sentence's predicate, because the two are unrelated: (genl chihuahua dog) licenses a largerThan antecedent and no walk from genl reaches largerThan. That is the same shape the qualitative re-join has, for the same reason, and special/recheck-preserving-along reads the same declarations to close the exception side of the identical channel.

solve-with-support clj

(solve-with-support kb literal context)

Solve the antecedent literal literal by preservation: a seq of {:bindings :claim :handles}, one per reading of an inherited claim it matches, each carrying the claim it was read off and the handles the reading rests on. A tuple reached over routes stated in contexts neither of which sees the other has one reading per route (supports-for), and each becomes a firing placed where its route is seen.

A closed literal asks supports-for once. An open one enumerates: every believed claim of the predicate, the tuples it licenses, and then the same supports-for per tuple — so the tuples are found by the reach and admitted by the full semantics, and an antecedent can no more join on an undercut or disputed claim than ask can answer one.

The diagonal is dropped (supports-for), so a claim stated at the tuple it is asked about stays the ordinary matcher's to find. Nothing here replaces that matcher; the caller unions the two.

supports-for clj

(supports-for kb goal context)

What licenses the ground goal (P a1 … an) by preservation — a vector of {:claim handle :handles [handle …]}, each the claim it was read off and every sentex the reading rests on — empty when nothing does.

verdict answers whether; this answers from what, which is what a justification needs. The semantics are verdict's exactly: the surviving claims must agree, so a goal the KB also denies, or one two claims disagree about at incomparable specificity, licenses nothing here either.

A goal the KB states directly licenses nothing, and that is deliberate. witness-terms is reflexive, so a stored (P a b) is among the claims bearing on (P a b) — it is the diagonal, it rests on no edge, and the ordinary matcher already finds it with a justification of its own. Answering it here too would hand the same conclusion a second justification resting on nothing the first did not already name.

One reading per reader the others do not reach. Each surviving claim, and each other statement of its tuple (:also), contributes its readings (claim-supports), and a reading is dropped when another is at least as strong — the claim's defeat class — and is seen from every reader that sees it (tax/uncovered). A claim and a route stated in one context, beside a route stated in a sibling context, therefore license two readings, and a firing over each places the conclusion where that reading is seen. The survivors are taken on defeat class first and then on content — the tuple, the context and the sentence, all spellings rather than handles (one tuple can carry two sentences at one class and context, the matcher being type-aware, and the chosen handle lands in a recorded justification) — and of two readings that cover each other the earlier is kept.

surviving clj

(surviving kb goal context)

The believed claims bearing on goal that a strictly more specific one has not displaced, each carrying its :polarity and :class. The raw material both consumers read: the prover turns it into a verdict, and checks/asymmetry-problem asks the narrower question of whether any survivor is known-true.

usable-relation? clj

(usable-relation? tax rel context)

May a declaration's R be walked? Either the engine owns its closure, or the KB says it composes. Read at use and not only at assert, so retracting (transitive R) stops the inheritance it licensed the way retracting anything else here does — the declaration is stored, but a relation nobody currently says is transitive is one whose reach we have no right to close. Read from context, like the declaration itself: a transitivity claim some invisible context makes is not a licence this one holds.

verdict clj

(verdict kb goal context)

What the preserved claims say about the ground goal:

:for — some claim reaches it and nothing surviving disagrees :against — the surviving claims deny it :ambiguous — surviving claims disagree at incomparable specificity, which is a dilemma and is deliberately not decided here nil — nothing bears on it, or the predicate declares no preserved position

Claims displaced by a strictly more specific one drop out first; that is where a general default yields to a specific statement without either being defeated.

virtual-relations clj

The relations witness-terms walks from a cached closure of the engine's own rather than from stored (R a b) facts — the type hierarchy and the context hierarchy. Both are transitive by construction, so a (transitive R) declaration on them is inert (it never routes them to the generic prover); every other relation must carry one, which is what wff/arg-preserving-problems reads this set to decide. The same set the taxonomy names closure-relations.

with-memo clj macro

(with-memo & body)

Answer body under a memo, reusing the enclosing one when there is one.

body must be eager, the precondition observe/with-search-scope carries for the same reason: a lazy seq handed back from here realizes after the binding frame has popped, so every positions and reach its elements ask for is walked again from scratch. Nothing reports that — the answers are identical — so each seq-returning layer below realizes before it returns.

witness-terms clj

(witness-terms kb {:keys [rel along?]} x context)

The terms a claim's argument may be stated of for it to reach x at this position: {w : (rel x w)} for transitiveInArgInverse, {w : (rel w x)} for transitiveInArg. Reflexive, so x itself is always among them and a directly-stated claim is found by the same walk as an inherited one.

One declaration's reach. Callers want a position's, which is the union over the declarations made at it — reach.

The genl walk is scoped to context, exactly as fact-reach is: a claim travels along the edges the asking context can see and no others, or a context would inherit (largerThan dog cat) down to a subtype some invisible theory declared. genlCx stays global — the context closure is (docs/taxonomy.md, the stated exception), and a preservation along it is a claim about the topology, which is universal.

Memoized on [rel along? x context] for the life of one question. The virtual relations read a cached closure and would survive without it; a fact-relation is the one that must not be re-walked, since each walk costs a matches-visible per node and undercut? asks for the same term's reach once per pair of claims.