Allen's interval algebra — a relation algebra over the generic constraint network in
vaelii.impl.qcn, and the third alongside the RCC-8 topology of vaelii.impl.space
and the cardinal directions of vaelii.impl.orientation. Those two say where things
are; this one says when they are, and about intervals rather than instants: an
interval has extent, so two of them can meet, overlap, or nest, and not merely precede
one another.
The thirteen base relations are jointly exhaustive and pairwise disjoint, so exactly
one holds of any two intervals. Each is a claim about the four ways their endpoints
can compare — writing an interval as [start end] with start < end:
:before a-end < b-start :meets a-end = b-start :overlaps a-start < b-start < a-end < b-end :finished-by a-start < b-start, a-end = b-end :contains a-start < b-start, a-end > b-end :starts a-start = b-start, a-end < b-end :equal a-start = b-start, a-end = b-end :started-by a-start = b-start, a-end > b-end :during a-start > b-start, a-end < b-end :finishes a-start > b-start, a-end = b-end :overlapped-by b-start < a-start < b-end < a-end :met-by a-start = b-end :after a-start > b-end
Six of them pair off with their converses (:before/:after, :meets/:met-by,
:overlaps/:overlapped-by, :starts/:started-by, :during/:contains,
:finishes/:finished-by); :equal is its own converse and the algebra's identity.
Intervals are stored as ordinary sentexes — the thirteen named binary predicates
(before, meets, during, …), plus seven derived predicates (precedes,
subintervalOf, sharesTimeWith, …) that each name a disjunction of them.
Intervals are ordinary individuals; nothing about them is special, and nothing here
reasons about clocks, dates or durations — only about order and containment.
The calculus reads every asserted interval relation visible from a context into a
qualitative constraint network — {[i j] → #{possible base relations}}, an unrecorded
pair meaning "unknown", i.e. all thirteen — and qcn/path-consistent tightens it to a
fixpoint. the prover then answers a goal (P i j) by entailment: it holds iff
every relation still possible between i and j satisfies P, possible ⊆ denotation(P).
So (before A B) and (before B C) entail (before A C), and (during A B) with
(during B C) entails (during A C) and the weaker (subintervalOf A C) with it.
An emptied constraint anywhere means the asserted relations are unsatisfiable, and then no interval goal is answered — an inconsistent theory should not be mined for conclusions.
Soundness. Path consistency is sound but not in general complete: it decides the
maximal tractable subclass of the interval algebra and no more, so an entailment
reported here is real while a non-entailment means "not provable", never "provably
false" — the same open-world reading argIsa and exceptWhen take.
The vocabulary ships as kb/upper/TimeContext.txt, an upper context rather than the
vocabulary head: these twenty predicates are about time, so CoreContext keeps only the
grammar they are declared in. The prover is opt-in on top of it: register it with
vaelii.core/add-prover, and until then a KB stores and retrieves interval relations as
ordinary facts without paying for the network.
Allen's interval algebra — a relation algebra over the generic constraint network in
`vaelii.impl.qcn`, and the third alongside the RCC-8 topology of `vaelii.impl.space`
and the cardinal directions of `vaelii.impl.orientation`. Those two say where things
are; this one says *when* they are, and about intervals rather than instants: an
interval has extent, so two of them can meet, overlap, or nest, and not merely precede
one another.
The thirteen base relations are jointly exhaustive and pairwise disjoint, so exactly
one holds of any two intervals. Each is a claim about the four ways their endpoints
can compare — writing an interval as `[start end]` with `start < end`:
:before a-end < b-start
:meets a-end = b-start
:overlaps a-start < b-start < a-end < b-end
:finished-by a-start < b-start, a-end = b-end
:contains a-start < b-start, a-end > b-end
:starts a-start = b-start, a-end < b-end
:equal a-start = b-start, a-end = b-end
:started-by a-start = b-start, a-end > b-end
:during a-start > b-start, a-end < b-end
:finishes a-start > b-start, a-end = b-end
:overlapped-by b-start < a-start < b-end < a-end
:met-by a-start = b-end
:after a-start > b-end
Six of them pair off with their converses (`:before`/`:after`, `:meets`/`:met-by`,
`:overlaps`/`:overlapped-by`, `:starts`/`:started-by`, `:during`/`:contains`,
`:finishes`/`:finished-by`); `:equal` is its own converse and the algebra's identity.
Intervals are **stored as ordinary sentexes** — the thirteen named binary predicates
(`before`, `meets`, `during`, …), plus seven derived predicates (`precedes`,
`subintervalOf`, `sharesTimeWith`, …) that each name a *disjunction* of them.
Intervals are ordinary individuals; nothing about them is special, and nothing here
reasons about clocks, dates or durations — only about order and containment.
The calculus reads every asserted interval relation visible from a context into a
qualitative constraint network — `{[i j] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all thirteen — and `qcn/path-consistent` tightens it to a
fixpoint. the prover then answers a goal `(P i j)` by **entailment**: it holds iff
every relation still possible between i and j satisfies P, `possible ⊆ denotation(P)`.
So `(before A B)` and `(before B C)` entail `(before A C)`, and `(during A B)` with
`(during B C)` entails `(during A C)` and the weaker `(subintervalOf A C)` with it.
An emptied constraint anywhere means the asserted relations are unsatisfiable, and then
*no* interval goal is answered — an inconsistent theory should not be mined for
conclusions.
**Soundness.** Path consistency is sound but not in general complete: it decides the
maximal tractable subclass of the interval algebra and no more, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `argIsa` and `exceptWhen` take.
The vocabulary ships as `kb/upper/TimeContext.txt`, an *upper* context rather than the
vocabulary head: these twenty predicates are *about* time, so CoreContext keeps only the
grammar they are declared in. The prover is **opt-in** on top of it: register it with
`vaelii.core/add-prover`, and until then a KB stores and retrieves interval relations as
ordinary facts without paying for the network.The thirteen jointly-exhaustive, pairwise-disjoint interval relations — the universe of the algebra, and so the constraint on a pair nothing is known about.
The thirteen jointly-exhaustive, pairwise-disjoint interval relations — the universe of the algebra, and so the constraint on a pair nothing is known about.
Allen's interval algebra as a vaelii.impl.qcn-kb calculus — the algebra, the
vocabulary, and the two caches. Everything below delegates to the shared glue, which
is the same code RCC-8 and the cardinal directions run.
Allen's interval algebra as a `vaelii.impl.qcn-kb` calculus — the algebra, the vocabulary, and the two caches. Everything below delegates to the shared glue, which is the same code RCC-8 and the cardinal directions run.
Allen's interval algebra as a vaelii.impl.qcn relation algebra.
Allen's interval algebra as a `vaelii.impl.qcn` relation algebra.
The canonical Allen composition table: (get-in allen-composition [r1 r2]) is the set
of base relations possible between A and C given r1(A,B) and r2(B,C). :equal is
the identity element on both sides.
Only three entries are the whole universe, and each is the same shape: two intervals positioned against a third that constrains neither against the other. A before B and C after B says nothing (both sit on the far side of B, in either order); so does A during B with B containing C, where A and C are both loose inside B.
interval_test derives all 169 entries independently, by enumerating every ordering of
six endpoints and reading off which outer relation each admits, and asserts the derived
table equals this one — so a mis-transcribed entry is a test failure, not a wrong
answer.
The canonical Allen composition table: `(get-in allen-composition [r1 r2])` is the set of base relations possible between A and C given `r1`(A,B) and `r2`(B,C). `:equal` is the identity element on both sides. Only three entries are the whole universe, and each is the same shape: two intervals positioned against a third that constrains neither against the other. A before B and C after B says nothing (both sit on the far side of B, in either order); so does A during B with B containing C, where A and C are both loose inside B. `interval_test` derives all 169 entries independently, by enumerating every ordering of six endpoints and reading off which outer relation each admits, and asserts the derived table equals this one — so a mis-transcribed entry is a test failure, not a wrong answer.
Each base relation's converse — reading the claim backwards. Six pairs and one
self-converse, since :equal is the identity.
Each base relation's converse — reading the claim backwards. Six pairs and one self-converse, since `:equal` is the identity.
(allen-prover)The interval-algebra entailment prover, to register with vaelii.core/add-prover.
The interval-algebra entailment prover, to register with `vaelii.core/add-prover`.
Base relation keyword → the binary predicate a fact about it is stored under.
:equal is spelled intervalEqual: it is a claim about extent in time, not about the
identity of two terms, so it must not be confused with the equality closure's equals.
Base relation keyword → the binary predicate a fact about it is stored under. `:equal` is spelled `intervalEqual`: it is a claim about extent in time, not about the identity of two terms, so it must not be confused with the equality closure's `equals`.
(compose s1 s2)The composition of two relation SETS: every base relation possible between A and C
when r(A,B) ∈ s1 and r(B,C) ∈ s2 — the union of the table entries, since a
disjunction on either side admits every combination.
The composition of two relation SETS: every base relation possible between A and C when r(A,B) ∈ `s1` and r(B,C) ∈ `s2` — the union of the table entries, since a disjunction on either side admits every combination.
(constraint net i j)The constraint set on [i j] in net: #{:equal} on the diagonal, the recorded set,
else all thirteen (unknown).
The constraint set on `[i j]` in `net`: `#{:equal}` on the diagonal, the recorded set,
else all thirteen (unknown).(converse-set rels)The converse of a relation set — how an asserted (P a b) constraint is read
backwards as the constraint on (b a).
The converse of a relation set — how an asserted `(P a b)` constraint is read backwards as the constraint on `(b a)`.
(definite-allen-relation kb context i1 i2)The single base relation between i1 and i2 when path consistency pins it down;
:inconsistent when the network contradicts itself, :unknown when two or more
relations remain possible.
The single base relation between `i1` and `i2` when path consistency pins it down; `:inconsistent` when the network contradicts itself, `:unknown` when two or more relations remain possible.
(inconsistent? kb context)Is the interval network visible from context unsatisfiable?
Is the interval network visible from `context` unsatisfiable?
Every interval predicate — the thirteen base ones and the seven derived ones — mapped
to the set of base relations it denotes. A goal (P i j) is entailed exactly when the
relations still possible between i and j are a subset of P's denotation, so a derived
predicate with a wide denotation is entailed by more networks than a base one, and the
base predicates are the singletons.
The derived seven are the disjunctions worth asking about: the two orderings that do not care whether the intervals touch, the three part-of relations, and the pair that says whether two intervals share any time at all.
Every interval predicate — the thirteen base ones and the seven derived ones — mapped to the set of base relations it denotes. A goal `(P i j)` is entailed exactly when the relations still possible between i and j are a *subset* of P's denotation, so a derived predicate with a wide denotation is entailed by more networks than a base one, and the base predicates are the singletons. The derived seven are the disjunctions worth asking about: the two orderings that do not care whether the intervals touch, the three part-of relations, and the pair that says whether two intervals share any time at all.
(possible-allen-relations kb context i1 i2)The Allen base relations still possible between intervals i1 and i2 given
everything believed in context — #{} when the network is inconsistent.
This is the algebra read directly rather than through a goal, so a caller that needs to
know how much is pinned down — rather than whether one named relation is entailed —
asks here. vaelii.impl.duration is the one in tree.
The Allen base relations still possible between intervals `i1` and `i2` given
everything believed in `context` — `#{}` when the network is inconsistent.
This is the algebra read directly rather than through a goal, so a caller that needs to
know *how much* is pinned down — rather than whether one named relation is entailed —
asks here. `vaelii.impl.duration` is the one in tree.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 |