The KB glue every relation algebra over vaelii.impl.qcn shares — reading believed
facts into a network, and reading entailments back out as prover solutions.
qcn itself knows nothing about a KB: an algebra is a parameter and a network is a
value. This namespace is the other half of that boundary, and it is the same half for
every calculus, so it is written once here rather than three times over. A calculus
bundles what actually differs:
{:name a keyword, naming the cache and the parity oracle
:algebra the qcn relation algebra
:denotation {predicate -> #{base relations}} — base ones are the singletons,
derived ones the wider disjunctions
:narrowing an optional second reader (below), nil for a calculus that has none}
Everything else — the reader, the two caches, the four goal shapes, the cost and
completeness declarations — follows from those three. vaelii.impl.space,
vaelii.impl.orientation and vaelii.impl.interval each define an algebra and a
vocabulary and call calculus; a fourth would be the same.
A narrowing is a second reader of the same network. Stored facts of the calculus
are one source of constraint on a pair, and they need not be the only one: the interval
algebra takes a second from vaelii.impl.stp, where a metric bound between two
intervals' endpoints rules Allen relations out that no stored fact mentions. A
narrowing answers {:net … :support …} in exactly the shape build-network
accumulates, so folding it in is one intersection per pair and one support union — and
everything downstream (the pass, the entailment reading, the support, the delta join) is
unchanged, because what it consumes is still one network value. Sound for the same
reason intersecting two stored facts is: a narrowing only ever removes relations the
constraints it read exclude, and a pair it leaves at the universe it does not record.
Both polarities are read and both are answered. A believed (not (P a b)) narrows the
pair by the complement of P's denotation, and a goal (not (P a b)) is answered by
refutation — possible ∩ denotation(P) = ∅, where the positive goal needs the
stronger possible ⊆ denotation(P). Both are licensed by the base relations being
jointly exhaustive and pairwise disjoint, which is what makes "not P" a constraint
here rather than an absence of information.
Three caches, and they answer different questions:
:qcn atom, keyed [calculus context]
and stamped with observe/change-clock — so it is read out of the KB once and then
reused until the engine actually mutates something. Building it is one
belief-filtered read per predicate of the calculus per polarity (twenty-eight of them
for RCC-8), and it is asked for constantly: a rule joining a qualitative antecedent
asks per binding, and every settle re-checks entailment-withdrawn? once per firing
of every rule that mentions the calculus. Those are stretches in which nothing
mutates at all, which is exactly what the clock recognises.Beside those, and not a cache at all, the resident atom carries the join baseline:
the network a calculus's forward rules were last re-joined over, which is what lets the
next re-join run over the pairs that moved instead of over every pair the network
entails (join-delta). It deliberately outlives a clock tick — its job is to describe a
moment the clock has moved past — and it is safe to lose, since losing it costs a full
re-join and nothing else.
The KB glue every relation algebra over `vaelii.impl.qcn` shares — reading believed
facts into a network, and reading entailments back out as prover solutions.
`qcn` itself knows nothing about a KB: an algebra is a parameter and a network is a
value. This namespace is the other half of that boundary, and it is the *same* half for
every calculus, so it is written once here rather than three times over. A **calculus**
bundles what actually differs:
{:name a keyword, naming the cache and the parity oracle
:algebra the `qcn` relation algebra
:denotation {predicate -> #{base relations}} — base ones are the singletons,
derived ones the wider disjunctions
:narrowing an optional second reader (below), nil for a calculus that has none}
Everything else — the reader, the two caches, the four goal shapes, the cost and
completeness declarations — follows from those three. `vaelii.impl.space`,
`vaelii.impl.orientation` and `vaelii.impl.interval` each define an algebra and a
vocabulary and call `calculus`; a fourth would be the same.
**A narrowing is a second reader of the same network.** Stored facts of the calculus
are one source of constraint on a pair, and they need not be the only one: the interval
algebra takes a second from `vaelii.impl.stp`, where a metric bound between two
intervals' endpoints rules Allen relations out that no stored fact mentions. A
narrowing answers `{:net … :support …}` in exactly the shape `build-network`
accumulates, so folding it in is one intersection per pair and one support union — and
everything downstream (the pass, the entailment reading, the support, the delta join) is
unchanged, because what it consumes is still one network value. Sound for the same
reason intersecting two stored facts is: a narrowing only ever removes relations the
constraints it read exclude, and a pair it leaves at the universe it does not record.
Both polarities are read and both are answered. A believed `(not (P a b))` narrows the
pair by the **complement** of P's denotation, and a goal `(not (P a b))` is answered by
**refutation** — `possible ∩ denotation(P) = ∅`, where the positive goal needs the
stronger `possible ⊆ denotation(P)`. Both are licensed by the base relations being
jointly exhaustive and pairwise disjoint, which is what makes "not P" a constraint
here rather than an absence of information.
Three caches, and they answer different questions:
* the **network is resident**, on the KB's own `:qcn` atom, keyed `[calculus context]`
and stamped with `observe/change-clock` — so it is read out of the KB once and then
reused until the engine actually mutates something. Building it is one
belief-filtered read per predicate of the calculus per polarity (twenty-eight of them
for RCC-8), and it is asked for constantly: a rule joining a qualitative antecedent
asks per binding, and every settle re-checks `entailment-withdrawn?` once per firing
of every rule that mentions the calculus. Those are stretches in which nothing
mutates at all, which is exactly what the clock recognises.
* the **path-consistency pass** is memoized on the network *value*, in an atom the
calculus owns. That is sound across queries because the network is derived from the
believed facts: any change to them yields a different map and so a different key.
* the **support-carrying pass** — which stored sentexes an entailed relation rests on —
is memoized separately, on the same network value, so an ordinary query never pays to
propagate support nobody asked for.
Beside those, and not a cache at all, the resident atom carries the **join baseline**:
the network a calculus's forward rules were last re-joined over, which is what lets the
next re-join run over the pairs that moved instead of over every pair the network
entails (`join-delta`). It deliberately outlives a clock tick — its job is to describe a
moment the clock has moved past — and it is safe to lose, since losing it costs a full
re-join and nothing else.(calculi-triggered-by kb pred)Every registered calculus whose network a sentence on pred moves, or nil — for each,
one of whose :trigger-predicates (every predicate calculus-for matches, plus the ones
a narrowing reads) is pred or a super-predicate of it. The re-check and re-join
triggers ask this, because what has to be put in front of a settle is a rule joining on
a relation the network entails, and a metric constraint moves that network without
being a predicate any such rule mentions. A caller holding (genl sub super) asks it
of super, since the edge moves what a fact on super moves.
The global genls closure, since the network reads a sub-predicate's facts through the
matcher's fan in whichever context sees the edge, and a trigger that over-selects costs
a re-join that derives nothing.
All of them, not the first: one predicate can move two networks. An instant fact is answered by the point calculus and read by the Allen one's narrowing, so answering only the first registered would re-join the Allen rules or not depending on registration order, and a firing on them on which of rule and fact arrived last.
Asked per asserted sentence: nil off the registry with no calculus registered, else a closure read and a membership test per supertype and calculus.
Every registered calculus whose network a sentence on `pred` moves, or nil — for each, one of whose `:trigger-predicates` (every predicate `calculus-for` matches, plus the ones a narrowing reads) is `pred` or a super-predicate of it. The re-check and re-join triggers ask this, because what has to be put in front of a settle is a rule joining on a relation the network entails, and a metric constraint moves that network without being a predicate any such rule mentions. A caller holding `(genl sub super)` asks it of `super`, since the edge moves what a fact on `super` moves. The global `genls` closure, since the network reads a sub-predicate's facts through the matcher's fan in whichever context sees the edge, and a trigger that over-selects costs a re-join that derives nothing. All of them, not the first: one predicate can move two networks. An instant fact is answered by the point calculus and read by the Allen one's narrowing, so answering only the first registered would re-join the Allen rules or not depending on registration order, and a firing on them on which of rule and fact arrived last. Asked per asserted sentence: nil off the registry with no calculus registered, else a closure read and a membership test per supertype and calculus.
(calculus nm algebra denotation)(calculus nm algebra denotation narrowing)Bundle an algebra and its vocabulary into the value every function here takes.
denotation maps each stored predicate to the set of base relations it denotes, so its
keys are the predicates the prover claims.
narrowing is the optional second reader — nil for a calculus that has none:
{:fn (fn [kb context] → {:net … :support …} | nil) :over-nodes (fn [nodes] → {:net … :support …} | nil) :node? which terms are nodes, when not every node is a symbol :sources every predicate whose arrival or departure moves what it answers :contexts the subset that puts a NODE in the network, so names a reader context}
:fn reads the KB; :over-nodes reads nothing but the node set, so it constrains pairs
by what the node terms themselves say — the point network orders the points of one
thing, and calendar moments by their fields (vaelii.impl.timepoint). Because it needs
no KB, it is also run over the nodes a goal names and no fact does
(with-goal-nodes), so a question about a calendar moment nobody stated is still
ordered against the ones they did. Either key may be absent.
The two predicate sets differ, and deliberately. A conversionFactor moves what a
metric bound comes to and so must re-check the rules concerned, but a context holding
one and nothing else has an empty interval network, and enumerating it as a reader
would cost a network build per goal to entail nothing. Both are folded once here rather
than per call: calculi-triggered-by runs per asserted sentence, and computing a union
there would allocate a set per assert.
The value carries the two caches its passes fill, so it is also registered in
built-calculi on the way out — that is how a reader can be told what they hold
without every calculus namespace having to say so itself.
Bundle an algebra and its vocabulary into the value every function here takes.
`denotation` maps each stored predicate to the set of base relations it denotes, so its
keys are the predicates the prover claims.
`narrowing` is the optional second reader — nil for a calculus that has none:
{:fn (fn [kb context] → {:net … :support …} | nil)
:over-nodes (fn [nodes] → {:net … :support …} | nil)
:node? which terms are nodes, when not every node is a symbol
:sources every predicate whose arrival or departure moves what it answers
:contexts the subset that puts a NODE in the network, so names a reader context}
`:fn` reads the KB; `:over-nodes` reads nothing but the node set, so it constrains pairs
by what the node terms themselves say — the point network orders the points of one
thing, and calendar moments by their fields (`vaelii.impl.timepoint`). Because it needs
no KB, it is also run over the nodes a **goal** names and no fact does
(`with-goal-nodes`), so a question about a calendar moment nobody stated is still
ordered against the ones they did. Either key may be absent.
The two predicate sets differ, and deliberately. A `conversionFactor` moves what a
metric bound comes to and so must re-check the rules concerned, but a context holding
one and nothing else has an *empty* interval network, and enumerating it as a reader
would cost a network build per goal to entail nothing. Both are folded once here rather
than per call: `calculi-triggered-by` runs per asserted sentence, and computing a union
there would allocate a set per assert.
The value carries the two caches its passes fill, so it is also registered in
`built-calculi` on the way out — that is how a reader can be told what they hold
without every calculus namespace having to say so itself.(calculus-for kb pred)The registered calculus claiming pred, or nil. Predicates belong to exactly one
calculus, so the first hit is the only hit.
What a calculus answers, which is what a rule antecedent is discharged by
(chain/qualitative-antecedent). A predicate that merely moves the network is
calculi-triggered-by's question, and answering it here would have the join try to
discharge a temporalDistance antecedent off the interval algebra.
The registered calculus claiming `pred`, or nil. Predicates belong to exactly one calculus, so the first hit is the only hit. What a calculus *answers*, which is what a rule antecedent is discharged by (`chain/qualitative-antecedent`). A predicate that merely moves the network is `calculi-triggered-by`'s question, and answering it here would have the join try to discharge a `temporalDistance` antecedent off the interval algebra.
(closure-with-support calc kb context)The support-carrying pass over the network of calc visible from context, every pair
at once: {:network … :support …}, or {:inconsistent [i j] :culprits #{handle}}. A
caller reading many pairs of the network's own nodes reads them here: support extends
the network by its goal's nodes on each call, which walks every pair of it.
The support-carrying pass over the network of `calc` visible from `context`, every pair
at once: `{:network … :support …}`, or `{:inconsistent [i j] :culprits #{handle}}`. A
caller reading many pairs of the network's own nodes reads them here: `support` extends
the network by its goal's nodes on each call, which walks every pair of it.(constraint calc net i j)The constraint set on [i j] in net: the identity on the diagonal, the recorded
set, else the universe (unknown).
The constraint set on `[i j]` in `net`: the identity on the diagonal, the recorded set, else the universe (unknown).
(definite calc kb context a b)The single base relation between a and b when path consistency pins it down;
:inconsistent when the network contradicts itself, :unknown when two or more
remain possible.
The single base relation between `a` and `b` when path consistency pins it down; `:inconsistent` when the network contradicts itself, `:unknown` when two or more remain possible.
(inconsistency-culprits calc kb context){:pair [i j] :support #{handle}} for an unsatisfiable network — the pair whose
constraint emptied and the sentexes behind it — or nil when the network is satisfiable.
Which pair is blamed for an inconsistency only composition finds depends on the order
the fixpoint reaches it, so this is a diagnosis rather than a canonical explanation.
The verdict itself does not depend on order; only the blame does. For that reason it is
the ledger's unsatisfiable-pairs — a function of the network alone — that
report-inconsistency! records, and this that a caller asks for on demand.
`{:pair [i j] :support #{handle}}` for an unsatisfiable network — the pair whose
constraint emptied and the sentexes behind it — or nil when the network is satisfiable.
Which pair is blamed for an inconsistency only *composition* finds depends on the order
the fixpoint reaches it, so this is a diagnosis rather than a canonical explanation.
The verdict itself does not depend on order; only the blame does. For that reason it is
the ledger's `unsatisfiable-pairs` — a function of the network alone — that
`report-inconsistency!` records, and this that a caller asks for on demand.(inconsistent? calc kb context)Is the network of calc visible from context unsatisfiable? The question
possible answers only obliquely, by going empty for every pair at once.
Is the network of `calc` visible from `context` unsatisfiable? The question `possible` answers only obliquely, by going empty for every pair at once.
(join-baseline kb calc context)What a re-join is measured against: the handles the network of calc in context was
read out of, and the network they close to. Both are resident reads, so taking one
inside a pinned step costs two map lookups.
What a re-join is measured against: the handles the network of `calc` in `context` was read out of, and the network they close to. Both are resident reads, so taking one inside a pinned step costs two map lookups.
(join-delta kb calc context){:moved … :baseline …} for calc in context — the pairs that may license a firing
the last re-join did not, and the baseline to hand back to note-joined once this
re-join is done.
:moved is :all — join over everything — whenever the delta cannot be trusted: no
baseline recorded yet, either side unsatisfiable, or a handle gone from the network's
input. Otherwise it is the set of pairs, both directions, whose closed constraint
differs, and empty without a pair read when the baseline's handles and closed network
are the resident objects themselves (read-network).
`{:moved … :baseline …}` for `calc` in `context` — the pairs that may license a firing
the last re-join did not, and the baseline to hand back to `note-joined` once this
re-join is done.
`:moved` is `:all` — join over everything — whenever the delta cannot be trusted: no
baseline recorded yet, either side unsatisfiable, or a handle gone from the network's
input. Otherwise it is the set of pairs, both directions, whose closed constraint
differs, and empty without a pair read when the baseline's handles and closed network
are the resident objects themselves (`read-network`).(network kb calc context)Read every believed relation of calc visible from context into a constraint
network {[a b] → #{base relations}}, both directions stored. Each asserted (P a b)
intersects the (a b) constraint with P's denotation and the (b a) constraint with its
converse; each believed (not (P a b)) intersects them with the complement of that
denotation and of its converse. So several facts about one pair narrow it together,
whatever their polarity — an unrecorded pair stays the full (unknown) set, and a pair
narrowed to nothing is a contradiction tighten reports.
Intersection is commutative and associative, so the network is a function of the
believed facts alone, never of the order they were asserted or read in — negatives
included, since a complement is a fixed function of the denotation. Resident on the
KB between reads (read-network).
context is one reader, and a variable is not one: it reads every context's facts
into a single network, which is a diagnostic view of everything stored rather than
anything anybody can see — two incomparable contexts compose in it and for no
reader. A goal is therefore never answered off that network; the prover fans over
reader-contexts instead, so "in some context" is the union of what the readers
answer.
Read every believed relation of `calc` visible from `context` into a constraint
network `{[a b] → #{base relations}}`, both directions stored. Each asserted `(P a b)`
intersects the (a b) constraint with P's denotation and the (b a) constraint with its
converse; each believed `(not (P a b))` intersects them with the **complement** of that
denotation and of its converse. So several facts about one pair narrow it together,
whatever their polarity — an unrecorded pair stays the full (unknown) set, and a pair
narrowed to nothing is a contradiction `tighten` reports.
Intersection is commutative and associative, so the network is a function of the
believed facts alone, never of the order they were asserted or read in — negatives
included, since a complement is a fixed function of the denotation. Resident on the
KB between reads (`read-network`).
`context` is one **reader**, and a variable is not one: it reads every context's facts
into a single network, which is a diagnostic view of everything stored rather than
anything anybody can see — two incomparable contexts compose in it and for no
reader. A goal is therefore never answered off that network; the prover fans over
`reader-contexts` instead, so "in some context" is the union of what the readers
answer.(network-support kb calc context)The asserted support of that network: {[a b] → #{handle}}, the sentexes whose
denotations were intersected into each pair. What qcn/path-consistent-with-support
starts from, and what an entailed relation's support is ultimately unioned out of.
The **asserted** support of that network: `{[a b] → #{handle}}`, the sentexes whose
denotations were intersected into each pair. What `qcn/path-consistent-with-support`
starts from, and what an entailed relation's support is ultimately unioned out of.(nodes net)Every term named by a constraint in net.
Every term named by a constraint in `net`.
(note-joined kb calc context baseline)Record baseline as the network every rule mentioning calc has now been joined over
in context. Only a caller that re-joins all of them may say so — a single rule's
own full join (a rule arriving) does not, or the next delta would claim the others were
covered too.
The baselines live in :qcn-joined, their own map beside the resident network
cache rather than inside it: the cache clears wholesale at its bound, and a
baseline is bookkeeping, not a memo — losing one silently degrades every later
delta join for that calculus and context to a full re-join. The map is bounded by
(calculi × reader contexts), which no eviction is needed for.
Record `baseline` as the network every rule mentioning `calc` has now been joined over in `context`. Only a caller that re-joins *all* of them may say so — a single rule's own full join (a rule arriving) does not, or the next delta would claim the others were covered too. The baselines live in `:qcn-joined`, their own map beside the resident network cache rather than inside it: the cache clears wholesale at its bound, and a baseline is bookkeeping, not a memo — losing one silently degrades every later delta join for that calculus and context to a full re-join. The map is bounded by (calculi × reader contexts), which no eviction is needed for.
(possible calc kb context a b)The base relations still possible between a and b given everything believed in
context — #{} when the network is inconsistent.
The base relations still possible between `a` and `b` given everything believed in
`context` — `#{}` when the network is inconsistent.(prover calc)The entailment prover for calc, to register with vaelii.core/add-prover.
The entailment prover for `calc`, to register with `vaelii.core/add-prover`.
(prover-for? nm pr)Is pr the prover of the calculus named nm? How a caller asks which calculus a
registered prover speaks for: the calculi share one record type, so a class test says
only that some calculus is registered.
Is `pr` the prover of the calculus named `nm`? How a caller asks which calculus a registered prover speaks for: the calculi share one record type, so a class test says only that some calculus is registered.
(reader-contexts kb calc)Every context worth reading a network of calc at: the contexts holding one of its
facts — or one of its narrowing's node-bearing facts, since a pair the metric layer
pins down is as much a constraint as a stored one — and the contexts where two or more
of those meet (tax/meet-closure, which a calculus whose facts all sit in one context
closes without reading a closure).
The contexts are read from the store rather than from belief, which over-approximates in the safe direction: a context whose only fact of this calculus is defeated is enumerated, reads an empty network there, and entails nothing.
Resident on the KB's :qcn atom, stamped with the change clock exactly as the
networks it names are. Collecting the fact contexts is a record fetch per stored fact
of the calculus — the same walk as reading one network, and answering the same
question about the same content — so a caller asking per goal would pay the whole
extent per goal. Chaining keeps a per-run memo in front of this and is unaffected;
the prover fanning a variable-context goal has no such run to memoize in, and is
exactly the caller that would.
Every context worth reading a network of `calc` at: the contexts holding one of its facts — or one of its narrowing's node-bearing facts, since a pair the metric layer pins down is as much a constraint as a stored one — and the contexts where two or more of those meet (`tax/meet-closure`, which a calculus whose facts all sit in one context closes without reading a closure). The contexts are read from the store rather than from belief, which over-approximates in the safe direction: a context whose only fact of this calculus is defeated is enumerated, reads an empty network there, and entails nothing. **Resident** on the KB's `:qcn` atom, stamped with the change clock exactly as the networks it names are. Collecting the fact contexts is a record fetch per stored fact of the calculus — the same walk as reading one network, and answering the same question about the same content — so a caller asking per goal would pay the whole extent per goal. Chaining keeps a per-run memo in front of this and is unaffected; the prover fanning a variable-context goal has no such run to memoize in, and is exactly the caller that would.
(registered-calculi kb)The calculi whose prover is registered on kb. Registration is the opt-in: with no
prover, a calculus's facts are ordinary facts, matched and chained like any other.
Memoized against the registry's identity (registry-calculi); a miss is a scan rather
than an absence — an instance? test per prover in the registry plus a fresh vector.
calculus-for is the only caller and the paths that ask it
(chain/qualitative-antecedent per antecedent literal,
special/recheck-on-qualitative per asserted sentence) each say what a miss costs
them.
The calculi whose prover is registered on `kb`. Registration is the opt-in: with no prover, a calculus's facts are ordinary facts, matched and chained like any other. Memoized against the registry's identity (`registry-calculi`); a miss is a scan rather than an absence — an `instance?` test per prover in the registry plus a fresh vector. `calculus-for` is the only caller and the paths that ask it (`chain/qualitative-antecedent` per antecedent literal, `special/recheck-on-qualitative` per asserted sentence) each say what a miss costs them.
(reported-sources kb calc context)unsatisfiable-sources as a report names them: no :stand-in, and :support as a
sorted vector of handles. nil when no source is unsatisfiable.
`unsatisfiable-sources` as a report names them: no `:stand-in`, and `:support` as a sorted vector of handles. nil when no source is unsatisfiable.
(solve-with-support calc kb goal context)(solve-with-support calc kb goal context pairs)Entailed solutions for goal in context, each paired with the handles it rests on —
a seq of [bindings #{handle}].
solve-goal answers which pairs the network entails; support answers what stored
facts each one rests on. Forward chaining needs both, and needs them together: the
bindings extend the join, and the handles become the conclusion's antecedents, so
retracting any fact behind the entailment withdraws whatever was concluded from it.
A pair whose support is empty is dropped rather than answered with a groundless
justification. That is not a hypothetical: the diagonal of a reflexive denotation
((partOfRegion ?x ?x)) is entailed by the algebra's identity alone, with no stored
fact behind it, and a conclusion drawn from it would rest on the rule and nothing else
while looking as though it rested on the network.
pairs narrows the enumeration to those pairs (solve-goal), which is what a re-join
over a delta passes. It adds no work here: a pair with no support was never going to
be answered, and a pair whose support is what changed is in the delta by construction.
goal is a positive literal (P a b), where solve-goal takes either polarity.
That is the boundary's shape rather than a shortcut: what a refutation rests on is the
whole network rather than a support list, so a negated antecedent is not answered by
entailment at all and chain/qualitative-antecedent claims only the positive shape.
Entailed solutions for `goal` in `context`, each paired with the handles it rests on —
a seq of `[bindings #{handle}]`.
`solve-goal` answers *which* pairs the network entails; `support` answers what stored
facts each one rests on. Forward chaining needs both, and needs them together: the
bindings extend the join, and the handles become the conclusion's antecedents, so
retracting any fact behind the entailment withdraws whatever was concluded from it.
A pair whose support is empty is dropped rather than answered with a groundless
justification. That is not a hypothetical: the *diagonal* of a reflexive denotation
(`(partOfRegion ?x ?x)`) is entailed by the algebra's identity alone, with no stored
fact behind it, and a conclusion drawn from it would rest on the rule and nothing else
while looking as though it rested on the network.
`pairs` narrows the enumeration to those pairs (`solve-goal`), which is what a re-join
over a delta passes. It adds no work here: a pair with no support was never going to
be answered, and a pair whose support is what changed is in the delta by construction.
`goal` is a **positive** literal `(P a b)`, where `solve-goal` takes either polarity.
That is the boundary's shape rather than a shortcut: what a *refutation* rests on is the
whole network rather than a support list, so a negated antecedent is not answered by
entailment at all and `chain/qualitative-antecedent` claims only the positive shape.(support calc kb context a b)The handles of the stored sentexes the relation between a and b rests on: the
facts a reader intersected into that pair's constraint, plus — transitively — the facts
behind every composition that narrowed it. #{} when the pair is unconstrained (there
is nothing to support "unknown") and when the network is inconsistent (an impossible
theory entails nothing to support).
This is the answer to "why does the network say that?", and it is the piece a
justification would need: an entailed relation has no handle of its own, so a datum
resting on it must rest on these instead. It names one derivation and
over-approximates that one, exactly as a justification names one support list —
see qcn/path-consistent-with-support for both halves of that claim.
The handles of the stored sentexes the relation between `a` and `b` rests on: the
facts a reader intersected into that pair's constraint, plus — transitively — the facts
behind every composition that narrowed it. `#{}` when the pair is unconstrained (there
is nothing to support "unknown") and when the network is inconsistent (an impossible
theory entails nothing to support).
This is the answer to "why does the network say that?", and it is the piece a
justification would need: an entailed relation has no handle of its own, so a datum
resting on it must rest on these instead. It names **one** derivation and
over-approximates *that* one, exactly as a justification names one support list —
see `qcn/path-consistent-with-support` for both halves of that claim.(tighten kb calc context net extra)pass over net, reporting an unsatisfiable network through report-inconsistency! on
the way past — the pass has just proved it, and the alternative is a query that silently
answers nothing. A cache hit of either kind does not re-record, so a query loop reports
once and a change of belief reports again.
net is a network as network reads it, never one with-goal-nodes extended:
newly-seen? holds one value per KB, calculus and context, so two networks alternating
under one key would each report as new. A goal is tightened through tighten-for-goal.
`pass` over `net`, reporting an unsatisfiable network through `report-inconsistency!` on the way past — the pass has just proved it, and the alternative is a query that silently answers nothing. A cache hit of either kind does not re-record, so a query loop reports once and a change of belief reports again. `net` is a network as `network` reads it, never one `with-goal-nodes` extended: `newly-seen?` holds one value per KB, calculus and context, so two networks alternating under one key would each report as new. A goal is tightened through `tighten-for-goal`.
(unsatisfiable-as-written kb calc context)qcn/unsatisfiable-pairs of the network of calc in context, less the stand-in pairs
of its unsatisfiable sources: the pairs whose stored facts no model satisfies.
`qcn/unsatisfiable-pairs` of the network of `calc` in `context`, less the stand-in pairs of its unsatisfiable sources: the pairs whose stored facts no model satisfies.
(unsatisfiable-somewhere? calc kb)Is the network of calc unsatisfiable for some context? Asked of the
governing-contexts alone: a context sees the facts one of them at or above it sees,
less what a defeat or an except withdraws below it, and a network over fewer facts
is never tighter — so no context is unsatisfiable where all of them are satisfiable
(docs/exceptions.md, "Two withdrawals a firing carries").
Is the network of `calc` unsatisfiable for some context? Asked of the `governing-contexts` alone: a context sees the facts one of them at or above it sees, less what a defeat or an `except` withdraws below it, and a network over fewer facts is never tighter — so no context is unsatisfiable where all of them are satisfiable (docs/exceptions.md, "Two withdrawals a firing carries").
(unsatisfiable-sources kb calc context)The unsatisfiable sources a narrowing of calc read in context, each
{:source kw :pairs [[p q] …] :support #{handle} :stand-in #{[a b]}}, a :metric source
adding :cycle [instant …]. :stand-in is the pair of this network the narrowing
emptied for the source and no stored fact emptied. nil when no source is unsatisfiable.
The unsatisfiable sources a narrowing of `calc` read in `context`, each
`{:source kw :pairs [[p q] …] :support #{handle} :stand-in #{[a b]}}`, a `:metric` source
adding `:cycle [instant …]`. `:stand-in` is the pair of this network the narrowing
emptied for the source and no stored fact emptied. nil when no source is unsatisfiable.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 |