Argument-position preservation: (transitiveInArg P n R) and
(transitiveInArgInverse P n R) license a stored claim about the term at argument n
of P for every term R's reach names from it. This namespace reads the declared
positions and their reaches, finds the claims bearing on a ground goal and decides
which a more specific one undercuts, names what an inherited reading rests on for a
justification or a nogood, and answers which rules and stored facts a sentence moves.
See docs/inherit.md.
**Argument-position preservation**: `(transitiveInArg P n R)` and `(transitiveInArgInverse P n R)` license a stored claim about the term at argument `n` of `P` for every term `R`'s reach names from it. This namespace reads the declared positions and their reaches, finds the claims bearing on a ground goal and decides which a more specific one undercuts, names what an inherited reading rests on for a justification or a nogood, and answers which rules and stored facts a sentence moves. See docs/inherit.md.
The consequent predicate of the forward rule whose antecedent is being joined, or nil.
positions leaves out the self relation of a pred the rule concludes on or below
(chain/walks-its-own-conclusion? draws the same line for the transitive walk): such a
rule stores its conclusions inside the closure the self relation walks.
The consequent predicate of the forward rule whose antecedent is being joined, or nil. `positions` leaves out the self relation of a `pred` the rule concludes on or below (`chain/walks-its-own-conclusion?` draws the same line for the transitive walk): such a rule stores its conclusions inside the closure the self relation walks.
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.
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.
True while chain reads a preserved antecedent: a :default claim that denies the
goal is left out before the survivors are read, so a firing it alone undercuts is made,
and stored with a defeat of its conclusion resting on that claim (contraries,
design ruling 25). The prover reads every claim.
True while `chain` reads a preserved antecedent: a `:default` claim that denies the goal is left out before the survivors are read, so a firing it alone undercuts is made, and stored with a defeat of its conclusion resting on that claim (`contraries`, design ruling 25). The prover reads every claim.
A per-question cache, an atom of {[:positions pred context concluding] -> …, [:reach rel along? x context] -> set, …}, or nil for no memoization. A question
moves no belief, so the memo needs no invalidation (docs/inherit.md, "What one
question costs").
A per-question cache, an atom of `{[:positions pred context concluding] -> …,
[:reach rel along? x context] -> set, …}`, or nil for no memoization. A question
moves no belief, so the memo needs no invalidation (docs/inherit.md, "What one
question costs").Which retrieval path finds the claims: :auto weighs the extent against the product
per goal, and :extent and :product force one, so inherit_oracle_test can hold the
two against each other on one KB.
Which retrieval path finds the claims: `:auto` weighs the extent against the product per goal, and `:extent` and `:product` force one, so `inherit_oracle_test` can hold the two against each other on one KB.
(answers? kb goal context)Does the prover answer goal (goal-verdict)? A negation needs a surviving denial
other than a :separated? membership. The separation that undercuts a claim does not
apply the soundness rule res/separation-denials applies to a refutation, and
provers/DisjointnessNegationProver answers a denial that meets it.
Does the prover answer `goal` (`goal-verdict`)? A negation needs a surviving denial other than a `:separated?` membership. The separation that undercuts a claim does not apply the soundness rule `res/separation-denials` applies to a refutation, and `provers/DisjointnessNegationProver` answers a denial that meets it.
(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.
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 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-reach, 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.
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-reach`, 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-reach-separated kb sen pred)The stored memberships (S x) the claim sen, on the preserved pred or a
sub-predicate of it, can deny by reaching (pred x) from some context
(separated-claims), as a superset: the unary facts at an argument of sen or at a
term a believed declaration of pred licenses from one (licensed-reach, read at
'?ctx) whose type is one of separated-types, or the stored extents of those types
when the terms outnumber them. The unary facts are read in every context, a candidate
set each asker reads again from its own.
The stored memberships `(S x)` the claim `sen`, on the preserved `pred` or a sub-predicate of it, can deny by reaching `(pred x)` from some context (`separated-claims`), as a superset: the unary facts at an argument of `sen` or at a term a believed declaration of `pred` licenses from one (`licensed-reach`, read at `'?ctx`) whose type is one of `separated-types`, or the stored extents of those types when the terms outnumber them. The unary facts are read in every context, a candidate set each asker reads again from its own.
(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.
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 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 three places: an explicit (not (P …)) at a tuple in range; for a
binary goal on an asymmetric P, the converse (P … y … x …); and, for a unary goal
(P x) with a preserved position, a membership (S x) of a type a separation holds
apart from P at context (separated-denials), at the goal's own tuple, tagged
:separated?.
Every probe is made, so a tuple believed in both polarities yields both claims and
verdict answers :ambiguous. The converse is not read at a self tuple [a a]
(docs/inherit.md, "Four things that follow from reading claims out of belief").
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. It reads no separated
membership: each strong? caller pairs a stored claim with a claim at another tuple.
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 three places: an explicit `(not (P …))` at a tuple in range; for a binary goal on an `asymmetric` `P`, the converse `(P … y … x …)`; and, for a unary goal `(P x)` with a preserved position, a membership `(S x)` of a type a separation holds apart from `P` at `context` (`separated-denials`), at the goal's own tuple, tagged `:separated?`. Every probe is made, so a tuple believed in both polarities yields both claims and `verdict` answers `:ambiguous`. The converse is not read at a self tuple `[a a]` (docs/inherit.md, "Four things that follow from reading claims out of belief"). `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. It reads no separated membership: each `strong?` caller pairs a stored claim with a claim at another tuple.
(claims-stored? kb pred)Does the store hold a sentex whose functor is pred or a predicate below it
(tax/specs-global), in either polarity, in any context, believed or not? False means
claims of pred is empty for every goal and every reader, since every claim is a
stored statement on a predicate the matcher fans pred over. The closure is unscoped
because it answers for every reader: a scoped fan is a subset of it. One index count
per predicate in the closure, memoized on pred.
Does the store hold a sentex whose functor is `pred` or a predicate below it (`tax/specs-global`), in either polarity, in any context, believed or not? False means `claims` of `pred` is empty for every goal and every reader, since every claim is a stored statement on a predicate the matcher fans `pred` over. The closure is unscoped because it answers for every reader: a scoped fan is a subset of it. One index count per predicate in the closure, memoized on `pred`.
(clashing-claim kb sentence context)The known-true claim that reaches sentence's own tuple by preservation and denies
it, as {: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. Known-true, because undercut? leaves no :default
general claim beside a nearer contrary one (docs/inherit.md, "A contrary claim against
a known-true one is a contradiction, and is reported"). A claim stated at
sentence's own tuple is excluded, since the negation family pairs two stored
sentexes (decide/note-candidate!), and so is a claim stating sentence itself.
:handles is the reading's support and not the claim: the declaration permitting 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 context.
The known-true claim that reaches `sentence`'s own tuple by preservation and denies
it, as `{: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. Known-true, because `undercut?` leaves no `:default`
general claim beside a nearer contrary one (docs/inherit.md, "A contrary claim against
a known-true one is a contradiction, and is reported"). A claim stated at
`sentence`'s own tuple is excluded, since the negation family pairs two stored
sentexes (`decide/note-candidate!`), and so is a claim stating `sentence` itself.
`:handles` is the reading's support and not the claim: the declaration permitting 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 `context`.(contraries kb goal context)The surviving claims (surviving, every claim read) that do not argue for goal in
context: what keeps a :for verdict from it. A firing over goal whose contraries
are all :default is stored with a defeat resting on each (design ruling 25).
The surviving claims (`surviving`, every claim read) that do not argue for `goal` in `context`: what keeps a `:for` verdict from it. A firing over `goal` whose contraries are all `:default` is stored with a defeat resting on each (design ruling 25).
(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).
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`).The most closure terms crossing-claim? reads the slot predicate set at. The closure is
specs-global of a genl edge's lower term together with genls-global of its upper
one, each walked by tax/specs-global-within, which stops one term past the cap. An
edge whose closure holds more is not narrowed: it moves every predicate preserved along
genl, read off the declarations' relation index with no index read.
The most closure terms `crossing-claim?` reads the slot predicate set at. The closure is `specs-global` of a `genl` edge's lower term together with `genls-global` of its upper one, each walked by `tax/specs-global-within`, which stops one term past the cap. An edge whose closure holds more is not narrowed: it moves every predicate preserved along `genl`, read off the declarations' relation index with no index read.
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).
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? kb)Does this KB store any declaration? One set-cardinality read per declaration
functor, neither belief-filtered nor context-scoped, so false is exact.
chain/preserving-antecedent? and declaration-index read this presence check first.
Does this KB store any declaration? One set-cardinality read per declaration functor, neither belief-filtered nor context-scoped, so false is exact. `chain/preserving-antecedent?` and `declaration-index` read this presence check first.
(declared kb)Every stored declaration's [P R] pair, read off the declaration functors' extents
with no context scope and no belief filter: the callers (special's exception
re-checks, declaration-index) are triggers, which must over-select. A negated
declaration, or one of another arity, drops out on its shape. One set-cardinality
read per functor, and a record fetch per stored declaration.
Every stored declaration's `[P R]` pair, read off the declaration functors' extents with no context scope and no belief filter: the callers (`special`'s exception re-checks, `declaration-index`) are triggers, which must over-select. A negated declaration, or one of another arity, drops out on its shape. One set-cardinality read per functor, and a record fetch per stored declaration.
(declared-about? kb pred)Could any stored declaration name pred? The declaration functors' extents are
counted, and a non-empty one is intersected with the argument root at position 1,
where a declaration's predicate sits. A presence check, neither belief-filtered nor
context-scoped: true says only that positions is worth reading, and false is exact.
recheck/cross-argument-predicate? reads it as a conservative test
(docs/inherit.md, "Reading it back").
Could any stored declaration name `pred`? The declaration functors' extents are counted, and a non-empty one is intersected with the argument root at position 1, where a declaration's predicate sits. A presence check, neither belief-filtered nor context-scoped: true says only that `positions` is worth reading, and false is exact. `recheck/cross-argument-predicate?` reads it as a conservative test (docs/inherit.md, "Reading it back").
(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. discovery/preserving-entry asks clashing-claim from
the most general contexts that see a reading with sentence and no except hiding one of
them.
Read at '?ctx, unscoped throughout, and over-approximating: 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. The claim's own tuple and a claim
stating sentence are excluded, as clashing-claim excludes them. The readings of
converse-claim's converse are named too, each joined by an asymmetric statement,
and those of separated-claims' claims, each joined by a way to see the separation
(separation-supports).
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. `discovery/preserving-entry` asks `clashing-claim` from
the most general contexts that see a reading with `sentence` and no except hiding one of
them.
Read at `'?ctx`, unscoped throughout, and over-approximating: 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. The claim's own tuple and a claim
stating `sentence` are excluded, as `clashing-claim` excludes them. The readings of
`converse-claim`'s converse are named too, each joined by an `asymmetric` statement,
and those of `separated-claims`' claims, each joined by a way to see the separation
(`separation-supports`).(edge-reach kb a b pred)The stored facts whose questions the genl edge (genl a b) can move for pred, a
predicate preserved along genl, as a superset: the facts of pred, in either
polarity, holding a term of the edge's closure (specs-global of a with
genls-global of b, the joint reaches at a position walking a second relation) at a
position pred is preserved at along genl or at the other position of a binary
converse, and, when a claim of pred is stored (claims-stored?), the unary facts at
such a term whose type is one of separated-types. The facts of pred are its stored
extent when the closure reads would outnumber it. nil when pred names no position
along genl or a commuting mark stands on pred or below it, for the caller to
re-open the extent. Read unscoped.
The stored facts whose questions the `genl` edge `(genl a b)` can move for `pred`, a predicate preserved along `genl`, as a superset: the facts of `pred`, in either polarity, holding a term of the edge's closure (`specs-global` of `a` with `genls-global` of `b`, the joint reaches at a position walking a second relation) at a position `pred` is preserved at along `genl` or at the other position of a binary converse, and, when a claim of `pred` is stored (`claims-stored?`), the unary facts at such a term whose type is one of `separated-types`. The facts of `pred` are its stored extent when the closure reads would outnumber it. nil when `pred` names no position along `genl` or a commuting mark stands on `pred` or below it, for the caller to re-open the extent. Read unscoped.
(goal-verdict goal)[verdict literal] for a goal the prover answers: [:for g] for a ground-goal? g,
[:against g] for (not g) over one, else nil. answers? compares the first member
with verdict of the literal, so a surviving denial answers the negation as a surviving
claim answers the positive (docs/inherit.md, "Reading it back").
`[verdict literal]` for a goal the prover answers: `[:for g]` for a `ground-goal?` `g`, `[:against g]` for `(not g)` over one, else nil. `answers?` compares the first member with `verdict` of the literal, so a surviving denial answers the negation as a surviving claim answers the positive (docs/inherit.md, "Reading it back").
(ground-goal? goal)A closed positive literal this can speak about. A forward join reads claims on a
positive antecedent alone; goal-verdict reads a (not …) over one for the prover.
A closed positive literal this can speak about. A forward join reads claims on a positive antecedent alone; `goal-verdict` reads a `(not …)` over one for the prover.
(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,
for a caller that enumerates stored facts to hand to rejoin-rules.
The declaration functors, transitive, asymmetric, and each relation some P in
preds is preserved along with its sub-predicates over the global closure. A claim on
P is not named, since the caller reads those already, and the permuting marks are not
named, since the engine lifts each into CxUniverse. Where a separation holds a P
apart from some type, the separated-types, disjoint, the
tax/separation-functors and the disjoint metatypes are named too. Two predicate-extent
counts for a KB that declares nothing.
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, for a caller that enumerates stored facts to hand to `rejoin-rules`. The declaration functors, `transitive`, `asymmetric`, and each relation some `P` in `preds` is preserved along with its sub-predicates over the global closure. A claim on `P` is not named, since the caller reads those already, and the permuting marks are not named, since the engine lifts each into `CxUniverse`. Where a separation holds a `P` apart from some type, the `separated-types`, `disjoint`, the `tax/separation-functors` and the disjoint metatypes are named too. Two predicate-extent counts for a KB that declares nothing.
(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-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 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 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.
Read at '?ctx over the global genls. A claim moves only a goal whose every argument
is one of the claim's or a term one of them licenses. A fact on a relation moves only
a goal with some argument that is an end of the fact or a term one licenses over the
relations at a position walking it. A fact on a predicate with a self relation is read
on both channels. A membership, a separation or a genl edge moves the goals
separation-moved names.
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 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. Read at `'?ctx` over the global `genls`. A claim moves only a goal whose every argument is one of the claim's or a term one of them licenses. A fact on a relation moves only a goal with some argument that is an end of the fact or a term one licenses over the relations at a position walking it. A fact on a predicate with a self relation is read on both channels. A membership, a separation or a `genl` edge moves the goals `separation-moved` names.
(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, over five
channels (docs/inherit.md, "Forward chaining on a claim nobody stored"):
P or a sub-predicate of it;R some P is preserved along, a genl or genlCx edge
included; a genl edge moves only the P crossing-claim? names, unless its closure
passes crossing-closure-cap;P at argument 1;(transitive R), (asymmetric P), and a permuting mark (permuting-marks);P, and a separation or genl
edge that moves which types those are (separation-moved).The reads are global and not belief-filtered: over-selecting costs a join that derives
what is already there. The pairs are declared's, indexed (declaration-index); a KB
that declares nothing pays two predicate-extent counts. The three-argument form takes
the [P R] pairs, for a caller asking per member of a settle's region under one
with-memo; wanted names the predicates whose genl narrowing the caller acts on.
The preserved predicates whose licensed claims `sen` may have moved, over five channels (docs/inherit.md, "Forward chaining on a claim nobody stored"): * a claim on `P` or a sub-predicate of it; * a fact on a relation `R` some `P` is preserved along, a `genl` or `genlCx` edge included; a `genl` edge moves only the `P` `crossing-claim?` names, unless its closure passes `crossing-closure-cap`; * the declaration itself, which names `P` at argument 1; * `(transitive R)`, `(asymmetric P)`, and a permuting mark (`permuting-marks`); * a membership of a type a separation holds apart from `P`, and a separation or `genl` edge that moves which types those are (`separation-moved`). The reads are global and not belief-filtered: over-selecting costs a join that derives what is already there. The pairs are `declared`'s, indexed (`declaration-index`); a KB that declares nothing pays two predicate-extent counts. The three-argument form takes the `[P R]` pairs, for a caller asking per member of a settle's region under one `with-memo`; `wanted` names the predicates whose `genl` narrowing the caller acts on.
(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 (docs/inference.md,
"A fact read in another argument order names the mark that licenses the order").
One alternative per minimal set of statements licensing the rearrangement, read off the
marks stored on the fact's own functor (tax/prop-supporters,
tax/commuting-supporters), with no index read (firing_cost_test). Each statement is
named by the believed sentexes stating it that context sees and no other covers, the
CxUniverse copy where it is believed. The groups are read unscoped, a superset.
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 (docs/inference.md, "A fact read in another argument order names the mark that licenses the order"). One alternative per minimal set of statements licensing the rearrangement, read off the marks stored on the fact's own functor (`tax/prop-supporters`, `tax/commuting-supporters`), with no index read (`firing_cost_test`). Each statement is named by the believed sentexes stating it that `context` sees and no other covers, the CxUniverse copy where it is believed. The groups are read unscoped, a superset.
(permuting-mark? f)Is f one of permuting-marks? A set lookup: every placement asks it of its
conclusion's functor (special/deduce-lifts).
Is `f` one of `permuting-marks`? A set lookup: every placement asks it of its conclusion's functor (`special/deduce-lifts`).
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.
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 kb pred context)[{:n :rel :along? :handle :in} …]: the preserved argument positions declared for
pred visible from context whose relation usable-relation? admits, and the self
relation (self-positions) at each of them. Empty when pred inherits nothing.
Several declarations at one position stay apart, since their reaches compose (reach).
:handle is the declaration's, which supports-for names; :in is its asserting
context, on which move-supports orders two statements of one declaration. Read only
past declared-about?; realized, and memoized on [pred context *concluding*].
`[{:n :rel :along? :handle :in} …]`: the preserved argument positions declared for
`pred` visible from `context` whose relation `usable-relation?` admits, and the self
relation (`self-positions`) at each of them. Empty when `pred` inherits nothing.
Several declarations at one position stay apart, since their reaches compose (`reach`).
`:handle` is the declaration's, which `supports-for` names; `:in` is its asserting
context, on which `move-supports` orders two statements of one declaration. Read only
past `declared-about?`; realized, and memoized on `[pred context *concluding*]`.(preserved-pairs kb)Every stored declaration's [P R] pair (declared), off declaration-index, or nil
when none is stored.
Every stored declaration's `[P R]` pair (`declared`), off `declaration-index`, or nil when none is stored.
(rejoin-rules kb sen)The forward rules to re-join in full because sen moved what a preserved predicate
licenses (every rule with an antecedent on a moved-predicates member), or nil. Keyed
on the antecedent index, since (genl chihuahua dog) moves a largerThan antecedent
whose predicate no walk from genl reaches.
The forward rules to re-join in full because `sen` moved what a preserved predicate licenses (every rule with an antecedent on a `moved-predicates` member), or nil. Keyed on the antecedent index, since `(genl chihuahua dog)` moves a `largerThan` antecedent whose predicate no walk from `genl` reaches.
(separated-claims kb sentence context)The known-true claims that reach (P x) by preservation, for each P the taxonomy
separates at context from the type S of the stored membership sentence (S x)
(separated-preserved), as clashing-claim answers: one {:sentence (P x) :context :claim :handles :class} per P some claim reaches. A claim stated at (P x) itself
is a stored membership the disjoint family pairs with sentence, and is excluded.
The separating declarations are not among :handles: each asker reads the separation
again, as converse-claim's reads the asymmetric mark.
The **known-true** claims that reach `(P x)` by preservation, for each `P` the taxonomy
separates at `context` from the type `S` of the stored membership `sentence` `(S x)`
(`separated-preserved`), as `clashing-claim` answers: one `{:sentence (P x) :context
:claim :handles :class}` per `P` some claim reaches. A claim stated at `(P x)` itself
is a stored membership the `disjoint` family pairs with `sentence`, and is excluded.
The separating declarations are not among `:handles`: each asker reads the separation
again, as `converse-claim`'s reads the `asymmetric` mark.(separated-preserved kb s context)The predicates a stored declaration names (declared) that the taxonomy separates from
the type s at context (tax/separation-test) and that some stored claim states
(claims-stored?), sorted: a membership (s x) denies (P x) for each. At '?ctx
the read is unscoped and exempts no pair, the union of what every reader separates. A
type no separation reaches reads no declaration. Memoized on [s context].
The predicates a stored declaration names (`declared`) that the taxonomy separates from the type `s` at `context` (`tax/separation-test`) and that some stored claim states (`claims-stored?`), sorted: a membership `(s x)` denies `(P x)` for each. At `'?ctx` the read is unscoped and exempts no pair, the union of what every reader separates. A type no separation reaches reads no declaration. Memoized on `[s context]`.
(separated-types kb pred)The types the unscoped taxonomy, exempting no pair, separates from pred: each type at
or below one tax/separating-partners names. The functors of the stored memberships a
claim of pred can deny (separated-claims), read as a superset over every reader,
since the callers re-open candidates each asker reads again.
The types the unscoped taxonomy, exempting no pair, separates from `pred`: each type at or below one `tax/separating-partners` names. The functors of the stored memberships a claim of `pred` can deny (`separated-claims`), read as a superset over every reader, since the callers re-open candidates each asker reads again.
(separation-moved-predicates kb sen)The preserved predicates whose goals' separated-denials sen arriving or leaving can
move (separation-moved), for the exception re-check; empty when the KB declares no
preservation.
The preserved predicates whose goals' `separated-denials` `sen` arriving or leaving can move (`separation-moved`), for the exception re-check; empty when the KB declares no preservation.
(solve-with-support kb literal context)Solves the antecedent literal by preservation: a seq of {:bindings :claim :handles}, one per reading of an inherited claim it matches (supports-for). A closed
literal asks supports-for once; an open one enumerates every believed claim of the
predicate and the tuples it licenses, and asks supports-for per tuple. The diagonal is
dropped, so the caller unions this with the ordinary matcher (docs/inherit.md,
"Forward chaining on a claim nobody stored").
Solves the antecedent `literal` by preservation: a seq of `{:bindings :claim
:handles}`, one per reading of an inherited claim it matches (`supports-for`). A closed
literal asks `supports-for` once; an open one enumerates every believed claim of the
predicate and the tuples it licenses, and asks `supports-for` per tuple. The diagonal is
dropped, so the caller unions this with the ordinary matcher (docs/inherit.md,
"Forward chaining on a claim nobody stored").(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. The semantics are verdict's: the
surviving claims must agree.
A goal the KB states directly licenses nothing: the stored claim is the diagonal of the reflexive reach, and the ordinary matcher already justifies it.
Each surviving claim, and each other statement of its tuple (:also), contributes its
readings (claim-supports). A reading is dropped when another is at least as strong
(the claim's defeat class) and seen from every reader that sees it (tax/uncovered), so
routes stated in sibling contexts license one reading each. The survivors are ordered
on defeat class, then the tuple, the context and the sentence, all spellings; of two
readings that cover each other the earlier is kept.
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. The semantics are `verdict`'s: the
surviving claims must agree.
A goal the KB states directly licenses nothing: the stored claim is the diagonal of the
reflexive reach, and the ordinary matcher already justifies it.
Each surviving claim, and each other statement of its tuple (`:also`), contributes its
readings (`claim-supports`). A reading is dropped when another is at least as strong
(the claim's defeat class) and seen from every reader that sees it (`tax/uncovered`), so
routes stated in sibling contexts license one reading each. The survivors are ordered
on defeat class, then the tuple, the context and the sentence, all spellings; of two
readings that cover each other the earlier is kept.(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. Under
*default-contraries-set-aside* a :default claim against the goal is not read.
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**. Under `*default-contraries-set-aside*` a `:default` claim against the goal is not read.
(usable-relation? tax rel context)May a declaration's R be walked from context? True for a virtual-relations
member, and for an R whose (transitive R) context sees. Read at use, so
retracting (transitive R) withdraws the reach (docs/inherit.md, "The transitivity
has to have been declared").
May a declaration's `R` be walked from `context`? True for a `virtual-relations` member, and for an `R` whose `(transitive R)` `context` sees. Read at use, so retracting `(transitive R)` withdraws the reach (docs/inherit.md, "The transitivity has to have been declared").
(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
nil — nothing bears on it, or the predicate declares no preserved position
Claims a strictly more specific one displaces drop out first (surviving).
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 `nil` — nothing bears on it, or the predicate declares no preserved position Claims a strictly more specific one displaces drop out first (`surviving`).
The relations witness-terms reads from the engine's cached closures
(tax/closure-relations) rather than from stored (R a b) facts. A declaration along
any other relation needs (transitive R) (wff/arg-preserving-problems,
usable-relation?).
The relations `witness-terms` reads from the engine's cached closures (`tax/closure-relations`) rather than from stored `(R a b)` facts. A declaration along any other relation needs `(transitive R)` (`wff/arg-preserving-problems`, `usable-relation?`).
(with-memo & body)Answers body under a memo, reusing the enclosing one when there is one. body must
be eager: a lazy seq handed back realizes after the binding pops, and walks every
positions and reach read again with the same answers (laziness_test).
Answers `body` under a memo, reusing the enclosing one when there is one. `body` must be eager: a lazy seq handed back realizes after the binding pops, and walks every `positions` and `reach` read again with the same answers (`laziness_test`).
(witness-terms kb {:keys [rel along?]} x context)The terms a claim's argument may be stated of for it to reach x under one
declaration: {w : (rel x w)} for transitiveInArgInverse, {w : (rel w x)} for
transitiveInArg. Reflexive, so x is always a member. The genl and fact-relation
walks are scoped to context, and genlCx is read globally (docs/inherit.md, "From
whose vantage"). A position's reach over all its declarations is reach. Memoized
on [rel along? x context].
The terms a claim's argument may be stated of for it to reach `x` under one
declaration: `{w : (rel x w)}` for `transitiveInArgInverse`, `{w : (rel w x)}` for
`transitiveInArg`. Reflexive, so `x` is always a member. The `genl` and fact-relation
walks are scoped to `context`, and `genlCx` is read globally (docs/inherit.md, "From
whose vantage"). A position's reach over all its declarations is `reach`. Memoized
on `[rel along? x context]`.cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |