Metric time as a simple temporal problem: bounds lo ≤ t(Q) − t(P) ≤ hi on the gaps
between instants, closed by all-pairs shortest paths, unsatisfiable on a negative cycle.
The algorithm half is pure data; the KB half reads temporalDistance measures, answers
them through TemporalDistanceProver (opt-in, :metric-time), and bridges the bounds
onto Allen's intervals through startOf / endOf for vaelii.impl.interval and
vaelii.impl.duration. See docs/stp.md.
Metric time as a **simple temporal problem**: bounds `lo ≤ t(Q) − t(P) ≤ hi` on the gaps between instants, closed by all-pairs shortest paths, unsatisfiable on a negative cycle. The algorithm half is pure data; the KB half reads `temporalDistance` measures, answers them through `TemporalDistanceProver` (opt-in, `:metric-time`), and bridges the bounds onto Allen's intervals through `startOf` / `endOf` for `vaelii.impl.interval` and `vaelii.impl.duration`. See docs/stp.md.
(allen-narrowing kb context)allen-narrowing-with-support's relation sets alone.
`allen-narrowing-with-support`'s relation sets alone.
Every predicate the metric narrowing of the interval algebra reads: the constraints, the
endpoint predicates and the unit table. vaelii.impl.interval declares these as the
narrowing's :sources.
Every predicate the metric narrowing of the interval algebra reads: the constraints, the endpoint predicates and the unit table. `vaelii.impl.interval` declares these as the narrowing's `:sources`.
(allen-narrowing-with-support kb context)What the metric constraints pin down about the interval relations, as
{:net {[i j] → #{base relations}} :support {[i j] → #{handle}}} — qcn-kb/build-network's
shape. A pair's support is both intervals' endpoint facts and the chains behind the four
endpoint-gaps. Only narrowed pairs are recorded. nil with no constraints or fewer
than two intervals with both endpoints. An inconsistent network answers
unsatisfiable-narrowing, supported by every constraint read, its source described by
inconsistency-source.
What the metric constraints pin down about the interval relations, as
`{:net {[i j] → #{base relations}} :support {[i j] → #{handle}}}` — `qcn-kb/build-network`'s
shape. A pair's support is both intervals' endpoint facts and the chains behind the four
`endpoint-gaps`. Only narrowed pairs are recorded. nil with no constraints or fewer
than two intervals with both endpoints. An inconsistent network answers
`unsatisfiable-narrowing`, supported by every constraint read, its source described by
`inconsistency-source`.The thirteen Allen base relations, read off endpoint-signature because
vaelii.impl.interval requires this namespace and not the reverse.
The thirteen Allen base relations, read off `endpoint-signature` because `vaelii.impl.interval` requires this namespace and not the reverse.
(close net nodes)close-state's :net, or :inconsistent. The caller passes every node net
mentions; extra nodes are isolated and change nothing.
`close-state`'s `:net`, or `:inconsistent`. The caller passes every node `net` mentions; extra nodes are isolated and change nothing.
(close-state net nodes)All-pairs shortest paths over net across nodes, as a closed state
{:net {[p q] → [lo hi]} :node-vec [instant …] :d ^doubles}, or :inconsistent on a
constraint unsatisfiable as given or a negative cycle. :d is written once; every
function taking a state copies it before an update.
All-pairs shortest paths over `net` across `nodes`, as a closed state
`{:net {[p q] → [lo hi]} :node-vec [instant …] :d ^doubles}`, or `:inconsistent` on a
constraint unsatisfiable as given or a negative cycle. `:d` is written once; every
function taking a state copies it before an update.(close-state-from net prior nodes)close-state, warm-started off prior, a closed state for a network net tightens
(tightening-of?): each moved constraint is relaxed in, and only moved bounds are read
back. At n or more moved edges it runs the full pass instead.
nodes must name every instant of prior as well as of net. A prior that net does
not tighten gives a wrong network, not an error.
`close-state`, warm-started off `prior`, a closed state for a network `net` tightens (`tightening-of?`): each moved constraint is relaxed in, and only moved bounds are read back. At `n` or more moved edges it runs the full pass instead. `nodes` must name every instant of `prior` as well as of `net`. A `prior` that `net` does not tighten gives a wrong network, not an error.
(closed-network kb context)The closed metric network visible from context: nil when problem is, else closure's
answer.
The closed metric network visible from `context`: nil when `problem` is, else `closure`'s answer.
(closure kb context {:keys [net] :as prob} extra-nodes)The closed network of prob across its nodes and extra-nodes, or :inconsistent.
Memoized on [net provers/*quantity-tolerance*], and resident per context and tolerance:
extra-nodes are isolated and stay out of the key, so contexts and KBs holding one
network share one pass. Warm-started (close-state-from) when the network last
resident for context is one this network tightens. An inconsistency is reported once per KB, context and network
(observe/newly-seen?), never on the memoized path.
The closed network of `prob` across its nodes and `extra-nodes`, or `:inconsistent`. Memoized on `[net provers/*quantity-tolerance*]`, and resident per context and tolerance: `extra-nodes` are isolated and stay out of the key, so contexts and KBs holding one network share one pass. Warm-started (`close-state-from`) when the network last resident for `context` is one this network tightens. An inconsistency is reported once per KB, context and network (`observe/newly-seen?`), never on the memoized path.
(constraint net p q)The bound on t(q) − t(p) in net: [0 0] on the diagonal whatever is recorded there,
else the recorded interval, else unbounded.
The bound on `t(q) − t(p)` in `net`: `[0 0]` on the diagonal whatever is recorded there, else the recorded interval, else unbounded.
(endpoint-gaps [a-start a-end] [b-start b-end])The four instant pairs an Allen relation between intervals [a-start a-end] and
[b-start b-end] is decided by, keyed as endpoint-signature keys them. The narrowing
and its support both read these.
The four instant pairs an Allen relation between intervals `[a-start a-end]` and `[b-start b-end]` is decided by, keyed as `endpoint-signature` keys them. The narrowing and its support both read these.
The two predicates naming an interval's bounding instants.
The two predicates naming an interval's bounding instants.
Each Allen base relation as the ordering it forces on each of the four endpoint
comparisons, keyed [which-of-A which-of-B]. The thirteen signatures are distinct.
Each Allen base relation as the ordering it forces on each of the four endpoint comparisons, keyed `[which-of-A which-of-B]`. The thirteen signatures are distinct.
(endpoints-with-support kb i context)Interval i's [[start end] handles] from the believed, visible startOf / endOf
facts and those facts' handles. nil when either is missing or names two different
instants; one instant restated in several visible contexts is one reading, all its
handles named.
Interval `i`'s `[[start end] handles]` from the believed, visible `startOf` / `endOf` facts and those facts' handles. nil when either is missing or names two different instants; one instant restated in several visible contexts is one reading, all its handles named.
(intervals-with-endpoints kb context){interval [[start end] #{handle}]} for every interval endpoints-with-support reads.
`{interval [[start end] #{handle}]}` for every interval `endpoints-with-support` reads.
(narrow net p q lo hi)Intersect the constraint on [p q] with [lo hi], writing the converse [q p] with it.
Commutative and associative, so a network is a function of its constraints' set.
Intersect the constraint on `[p q]` with `[lo hi]`, writing the converse `[q p]` with it. Commutative and associative, so a network is a function of its constraints' set.
(negative-cycle-nodes d node-vec)The instants whose self-distance in the closed matrix d is below zero by more than
provers/*quantity-tolerance*.
The instants whose self-distance in the closed matrix `d` is below zero by more than `provers/*quantity-tolerance*`.
(nodes net)Every instant named by a constraint in net.
Every instant named by a constraint in `net`.
(overlap-bounds-from-endpoints closed ea eb)How long two intervals overlap, as [lo hi], read off a closed network and their
[start end] instants (docs/stp.md, "Sharpening an overlap").
How long two intervals overlap, as `[lo hi]`, read off a closed network and their `[start end]` instants (docs/stp.md, "Sharpening an overlap").
(overlap-window-with-support kb context i1 i2)The metric bound on how long intervals i1 and i2 overlap, as
[[[dimension unit] lo hi] handles] — hi possibly infinite — with the endpoint facts
and the chains behind the four overlap-gaps as its support. nil when there is nothing
to read, the network is inconsistent, or the bound is the vacuous [0 ∞].
The metric bound on how long intervals `i1` and `i2` overlap, as `[[[dimension unit] lo hi] handles]` — `hi` possibly infinite — with the endpoint facts and the chains behind the four `overlap-gaps` as its support. nil when there is nothing to read, the network is inconsistent, or the bound is the vacuous `[0 ∞]`.
(point-possibilities [lo hi])The vaelii.impl.point base relations a bound [lo hi] on t(q) − t(p) leaves open:
:before while the gap can be positive, :equal while it can be zero, :after while it
can be negative, each read to provers/*quantity-tolerance*. Never empty.
The `vaelii.impl.point` base relations a bound `[lo hi]` on `t(q) − t(p)` leaves open: `:before` while the gap can be positive, `:equal` while it can be zero, `:after` while it can be negative, each read to `provers/*quantity-tolerance*`. Never empty.
(problem kb context)Every temporalDistance believed and visible from context, as
{:dimension :unit :net :support}. nil when nothing is stated, and nil — reported once
per KB and context — when the constraints span more than one dimension. Resident on the
KB's :qcn atom, stamped with the change clock and keyed on the tolerance the
magnitudes are snapped to.
Every `temporalDistance` believed and visible from `context`, as
`{:dimension :unit :net :support}`. nil when nothing is stated, and nil — reported once
per KB and context — when the constraints span more than one dimension. Resident on the
KB's `:qcn` atom, stamped with the change clock and keyed on the tolerance the
magnitudes are snapped to.(relations-from-endpoints closed ea eb)The Allen relations the closed network closed still permits between intervals with
[start end] instants ea and eb: those whose every signature ordering is still
possible. The reading is sound but not sharp (docs/stp.md).
The Allen relations the closed network `closed` still permits between intervals with `[start end]` instants `ea` and `eb`: those whose every signature ordering is still possible. The reading is sound but not sharp (docs/stp.md).
(separation kb context p q)The tightest [lo hi] on t(q) − t(p) visible from context, as
[[dimension unit] lo hi] in the base unit; [-∞ ∞] for a pair nothing reaches. nil
when nothing is stated or the network is inconsistent.
The tightest `[lo hi]` on `t(q) − t(p)` visible from `context`, as `[[dimension unit] lo hi]` in the base unit; `[-∞ ∞]` for a pair nothing reaches. nil when nothing is stated or the network is inconsistent.
The metric predicate a constraint is stated with, and the prover claims.
The metric predicate a constraint is stated with, and the prover claims.
(stp-prover)The metric temporal prover — (vaelii.core/add-reasoner kb :metric-time).
The metric temporal prover — `(vaelii.core/add-reasoner kb :metric-time)`.
(tightening-of? net prior)Is every bound prior records at least as wide as the one net records for the same
pair? The precondition for close-state-from.
Is every bound `prior` records at least as wide as the one `net` records for the same pair? The precondition for `close-state-from`.
The constraint on a pair nothing is known about: the whole real line.
The constraint on a pair nothing is known about: the whole real line.
(unsatisfiable-narrowing intervals support source)The narrowing an unsatisfiable source answers over intervals: the pair of the two
first under nm/print-key emptied both ways, support behind it. An empty pair is
unsatisfiable as given, so the interval network it is folded into is unsatisfiable and
answers nothing. nil for fewer than two intervals.
:unsatisfiable-sources carries source, the description of the clash in the source
network, with the emptied pair as its :stand-in: the pair stands in for the source's
clash and is not one any interval fact contradicts (qcn-kb/unsatisfiable-sources).
An unsatisfiable source admits no endpoint ordering, so reading it pair by pair would empty every pair; one emptied pair gives the same verdict. Answering nil instead would widen the interval network when a fact arrives, and an entailment drawn through the narrowing would stop holding while the firing that rested on it stayed believed (docs/qcn.md, "A network can have a second reader").
The narrowing an unsatisfiable source answers over `intervals`: the pair of the two first under `nm/print-key` emptied both ways, `support` behind it. An empty pair is unsatisfiable as given, so the interval network it is folded into is unsatisfiable and answers nothing. nil for fewer than two intervals. `:unsatisfiable-sources` carries `source`, the description of the clash in the source network, with the emptied pair as its `:stand-in`: the pair stands in for the source's clash and is not one any interval fact contradicts (`qcn-kb/unsatisfiable-sources`). An unsatisfiable source admits no endpoint ordering, so reading it pair by pair would empty every pair; one emptied pair gives the same verdict. Answering nil instead would widen the interval network when a fact arrives, and an entailment drawn through the narrowing would stop holding while the firing that rested on it stayed believed (docs/qcn.md, "A network can have a second reader").
(unsatisfiable-pairs net)The pairs of net that are unsatisfiable as written; empty when the network is
unsatisfiable only through a cycle.
The pairs of `net` that are unsatisfiable as written; empty when the network is unsatisfiable only through a cycle.
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 |