RCC-8 qualitative spatial reasoning — a relation algebra over the generic constraint
network in vaelii.impl.qcn, alongside the cardinal directions of
vaelii.impl.orientation and the interval time of vaelii.impl.interval. This one is
topology: whether two regions touch, overlap or nest, saying nothing about which way
they lie.
The eight RCC-8 base relations between two regions are jointly exhaustive and pairwise disjoint, so exactly one of them holds of any pair:
:dc DC disconnected :ec EC externally connected (touching, no shared interior) :po PO partially overlapping :eq EQ equal :tpp TPP tangential proper part (x inside y, touching the boundary) :ntpp NTPP non-tangential proper part (x strictly inside y) :tppi TPPi the converse of TPP :ntppi NTPPi the converse of NTPP
Spatial knowledge is stored as ordinary sentexes — the eight named binary
predicates (nonTangentialProperPart, externallyConnected, …), plus six derived
predicates (partOfRegion, regionOverlaps, …) that each name a disjunction of
base relations. Regions are ordinary individuals; nothing about them is special.
region-network reads every asserted spatial relation visible from a context into a
qualitative constraint network — {[r1 r2] → #{possible base relations}}, an
unrecorded pair meaning "unknown", i.e. all eight — and qcn/path-consistent
tightens it to a fixpoint. the prover then answers a goal (P r1 r2) by
entailment: it holds iff every relation still possible between r1 and r2
satisfies P, possible ⊆ denotation(P). So (nonTangentialProperPart A B) and
(nonTangentialProperPart B C) entail both (nonTangentialProperPart A C) (the
composition table pins the pair to #{:ntpp}) and the weaker (partOfRegion A C)
and (regionOverlaps A C), whose denotations are supersets of it.
An emptied constraint anywhere means the asserted network is spatially inconsistent, and then no spatial goal is answered — an inconsistent theory should not be mined for conclusions.
Soundness. Path consistency is sound, and decides RCC-8 over its maximal
tractable subclass; on the full language it can leave a network path-consistent yet
globally unsatisfiable. So an entailment this prover reports is real, but a
non-entailment means "not provable", never "provably false". That is the same
open-world reading argIsa and exceptWhen take, and it is what story-scale
networks need.
The vocabulary ships as kb/upper/SpaceContext.txt, an upper context rather than
the vocabulary head: these fourteen predicates are about space, so CoreContext keeps
only the grammar they are declared in (binaryPredicate, comment) and a KB carries
the subject only if it loads the layer. The prover is opt-in on top of that —
register it with vaelii.core/add-prover — so a KB can store spatial facts and
retrieve them as ordinary facts without paying for the network.
RCC-8 qualitative spatial reasoning — a relation algebra over the generic constraint
network in `vaelii.impl.qcn`, alongside the cardinal directions of
`vaelii.impl.orientation` and the interval time of `vaelii.impl.interval`. This one is
topology: whether two regions touch, overlap or nest, saying nothing about which way
they lie.
The eight RCC-8 base relations between two regions are jointly exhaustive and
pairwise disjoint, so exactly one of them holds of any pair:
:dc DC disconnected
:ec EC externally connected (touching, no shared interior)
:po PO partially overlapping
:eq EQ equal
:tpp TPP tangential proper part (x inside y, touching the boundary)
:ntpp NTPP non-tangential proper part (x strictly inside y)
:tppi TPPi the converse of TPP
:ntppi NTPPi the converse of NTPP
Spatial knowledge is **stored as ordinary sentexes** — the eight named binary
predicates (`nonTangentialProperPart`, `externallyConnected`, …), plus six derived
predicates (`partOfRegion`, `regionOverlaps`, …) that each name a *disjunction* of
base relations. Regions are ordinary individuals; nothing about them is special.
`region-network` reads every asserted spatial relation visible from a context into a
qualitative constraint network — `{[r1 r2] → #{possible base relations}}`, an
unrecorded pair meaning "unknown", i.e. all eight — and `qcn/path-consistent`
tightens it to a fixpoint. the prover then answers a goal `(P r1 r2)` by
**entailment**: it holds iff every relation still possible between r1 and r2
satisfies P, `possible ⊆ denotation(P)`. So `(nonTangentialProperPart A B)` and
`(nonTangentialProperPart B C)` entail both `(nonTangentialProperPart A C)` (the
composition table pins the pair to `#{:ntpp}`) and the weaker `(partOfRegion A C)`
and `(regionOverlaps A C)`, whose denotations are supersets of it.
An emptied constraint anywhere means the asserted network is spatially inconsistent,
and then *no* spatial goal is answered — an inconsistent theory should not be mined
for conclusions.
**Soundness.** Path consistency is sound, and decides RCC-8 over its maximal
tractable subclass; on the full language it can leave a network path-consistent yet
globally unsatisfiable. So an entailment this prover reports is real, but a
*non*-entailment means "not provable", never "provably false". That is the same
open-world reading `argIsa` and `exceptWhen` take, and it is what story-scale
networks need.
The vocabulary ships as `kb/upper/SpaceContext.txt`, an *upper* context rather than
the vocabulary head: these fourteen predicates are *about* space, so CoreContext keeps
only the grammar they are declared in (`binaryPredicate`, `comment`) and a KB carries
the subject only if it loads the layer. The prover is **opt-in** on top of that —
register it with `vaelii.core/add-prover` — so a KB can store spatial facts and
retrieve them as ordinary facts without paying for the network.The eight jointly-exhaustive, pairwise-disjoint RCC-8 base relations — the universe of the algebra, and so the constraint on a pair nothing is known about.
The eight jointly-exhaustive, pairwise-disjoint RCC-8 base relations — the universe of the algebra, and so the constraint on a pair nothing is known about.
Base relation keyword → the binary predicate a fact about it is stored under.
Base relation keyword → the binary predicate a fact about it is stored under.
(compose s1 s2)The composition of two relation SETS: every base relation possible between x and z
when r(x,y) ∈ s1 and r(y,z) ∈ 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 x and z when r(x,y) ∈ `s1` and r(y,z) ∈ `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: #{:eq} on the diagonal, the recorded set,
else all eight (unknown).
The constraint set on `[i j]` in `net`: `#{:eq}` on the diagonal, the recorded set,
else all eight (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-relation kb context r1 r2)The single base relation between r1 and r2 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 `r1` and `r2` 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 spatial network visible from context unsatisfiable?
Is the spatial network visible from `context` unsatisfiable?
(possible-relations kb context r1 r2)The RCC-8 base relations still possible between regions r1 and r2 given everything
believed in context — #{} when the network is inconsistent.
The RCC-8 base relations still possible between regions `r1` and `r2` given everything
believed in `context` — `#{}` when the network is inconsistent.RCC-8 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 the
cardinal directions and the interval algebra run.
RCC-8 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 the cardinal directions and the interval algebra run.
RCC-8 as a vaelii.impl.qcn relation algebra.
RCC-8 as a `vaelii.impl.qcn` relation algebra.
The RCC-8 composition table: (get-in rcc8-composition [r1 r2]) is the set of base
relations possible between x and z given r1(x,y) and r2(y,z). The canonical
Randell–Cui–Cohn table; EQ is the identity element, and PO∘PO is unconstrained.
The RCC-8 composition table: `(get-in rcc8-composition [r1 r2])` is the set of base relations possible between x and z given `r1`(x,y) and `r2`(y,z). The canonical Randell–Cui–Cohn table; EQ is the identity element, and PO∘PO is unconstrained.
Each base relation's converse. DC/EC/PO/EQ are symmetric; TPP↔TPPi, NTPP↔NTPPi.
Each base relation's converse. DC/EC/PO/EQ are symmetric; TPP↔TPPi, NTPP↔NTPPi.
(region-network kb context)Every asserted spatial relation visible from context, as a constraint network.
Every asserted spatial relation visible from `context`, as a constraint network.
Every spatial predicate — the eight base ones and the six derived ones — mapped to
the set of base relations it denotes. A goal (P r1 r2) is entailed exactly when
the relations still possible between r1 and r2 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.
Every spatial predicate — the eight base ones and the six derived ones — mapped to the set of base relations it denotes. A goal `(P r1 r2)` is entailed exactly when the relations still possible between r1 and r2 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 predicates the RCC-8 prover claims — the keys of spatial-denotation.
The predicates the RCC-8 prover claims — the keys of `spatial-denotation`.
(spatial-prover)The RCC-8 entailment prover, to register with vaelii.core/add-prover.
The RCC-8 entailment prover, to register with `vaelii.core/add-prover`.
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 |