The Region Connection Calculus

Axioms, Theorems and Proofs

This page is maintained by Brandon Bennett. It is intended to support investigation into the 1st-order axiomatic theory of the Region Connection Calculus (RCC). A number of papers on the RCC theory are obtainable from the bibliography page of the Leeds University Qualitative Spatial Reasoning group.

At the moment the page is very much under construction. I have just thrown together some axioms which I have been using recently with Otter. I hope this page will gradually become more comprehensive and more systematic.

I give all axioms in syntax accaptable to the Otter theorem prover. The meanings of the logical symbols should be clear. Note however that the `|' sympol is used for disjunction. 

The KR-92 Axiom Set

The axiom set given in the KR-92 paper A Spatial Logic Based on Regions and Connection (get PostScript) is as follows:

C AXIOMS

  • (all x all y (C(x,y) -> C(y,x))).
  • (all x C(x,x)).

    • DEFINITIONS

  • (all x all y (DC(x,y) <-> -C(xy,y))).
  • (all x all y (P(x,y) <-> (all z (C(z,x) -> C(z,y))))).
  • (all x all y (PP(x,y) <-> (P(x,y) & -P(y,x)))).
  • (all x all y ( x=y <-> (P(x,y) & P(y,x)))).
  • (all x all y (O(x,y) <-> (exists z (P(z,x) & P(z,y))))).
  • (all x all y (PO(x,y) <-> (O(x,y) & -P(x,y) & -P(y,x)))).
  • (all x all y (DR(x,y) <-> -O(x,y))).
  • (all x all y (EC(x,y) <-> (C(x,y) & -O(x,y)))).
  • (all x all y (TPP(x,y) <-> (PP(x,y) & (exists z (EC(z,x) & EC(z,y)))))).
  • (all x all y (NTPP(x,y) <-> (PP(x,y) & -(exists z (EC(z,x) & EC(z,y)))))).
  • (all x all y (Pi(x,y) <-> P(y,x))).
  • (all x all y (PPi(x,y) <-> PP(y,x))).
  • (all x all y (TPPi(x,y) <-> TPP(y,x))).
  • (all x all y (NTPPi(x,y) <-> NTPP(y,x))).

    • QUASI-BOOLEAN FUNCTIONS

  • (sum(x,y) = (iota z (all w ( C(w,z) <-> (C(w,x) | C(w,y)))))).
  • (compl(x) = (iota y ((all z (C(z,y) <-> -NTPP(z,x))) & (all z (O(z,y) <-> -P(z,x)))))).
  • (prod(x,y) = (iota z (all u (C(u,z) <-> (exists v (P(v,x) & P(v,y) & C(u,v))))))).
  • (diff(x,y) = (iota w (all z (C(z,w) <-> C(z,prod(x,compl(y))))))).
  • (us = (iota x (all y C(y,x)))).


    • These definitions make use of an 'iota' operator. A term (iota x Psi(x)) is read as 'the x such that Psi(x)'.
    The KR-92 paper tells us that in the context of definitions such as that given for sum etc. the iota can be eliminated by replacing
    f(x...) = (iota y (Psi(f(x...)))) with (all x... (Psi(f(x...))))
    where x... stands for the sequence of variables which are the arguments of f.
    In fact this translation is too weak. One should replace the iota as follows:
    (all x... ( (y = f(x...)) <-> (Psi(y)))).
    after applying this transform the Quasi-Boolean definitions become:

  • (all x all y all z ((sum(x,y) = z) <-> (all w ( C(w,z) <-> (C(w,x) | C(w,y)))))).
  • (all x all y ((compl(x) = y) <-> (all z (C(z,y) <-> -NTPP(z,x))) & (all z (O(z,y) <-> -P(z,x))))).
  • (all x all y all z ((prod(x,y) = z) <-> (all u (C(u,z) <-> (exists v (P(v,x) & P(v,y) & C(u,v))))))).
  • (all x all y all z ((diff(x,y) = z) <-> (all w (C(w,z) <-> C(w,prod(x,compl(y))))))).
  • (all x ((us = x) <-> (all y C(y,x)))).


    • The following axiom links the Quasi-Boolean functions to the sort structure of the theory:

  • (all x all y ( NULL(prod(x,y)) <-> DR(x,y))).


    • Finally the NTPP axiom ensures that every region has an NTPP:

  • (all x (exists y NTPP(y,x))).


    • An axiom set proposed by Brandon Bennett

    This set is intended to be essentially the same as the KR-92 set but unsorted. To achieve this the function definitions have been replaced with existentional axioms which are intended to be equivalent (but may well be slightly different).

    C AXIOMS

    (all x all y ( (all z (C(z,x) <-> C(z,y))) -> (x = y))).
    (all x all y (C(x,y) -> C(y,x))).
    (all x C(x,x)).

    DEFINITIONS

    (all x all y (P(x,y) <-> (all z (C(x,z) -> C(y,z))))).
    (all x all y (O(x,y) <-> (exists z (P(z,x) & P(z,y))))).

    QUASI-BOOLEAN EXISTENTIAL AXIOMS

    These axioms are a modification of the function 'definitions' given in KR92. My axioms replace the functions by existential axioms. I have also modified the axioms so that they work in unsorted logic. The domain here is always non-null regions. [note: these axioms could be made simpler by introducing a null region into the domain (compl and prod would then be total functions)]

    sum existence
    (all x y (exists z (all w (C(w,z) <-> (C(w,x) | C(w,y)))))).

    complement existence
    (all x ( (exists y -C(x,y)) -> (exists z ( (all w (C(w,z) <-> -NTPP(w,x)) &(all w (O(w,z) <-> -P(w,x)) ) ) )).

    product existence
    (all x y ( O(x,y) <-> (exists z (all w (P(w,z) <-> (P(w,x) & P(w,y))))) )).

    universe existence
    (exists x (all y C(x,y)))

    Replacement for NTPP axiom
    (exists x exists y -(x = y)).
    It can be shown that the NTPP axiom must hold unless there is only a single region in the universe. Thus, by requiring that there are at least two distinct regions in the universe, one ought to be able to prove the NTPP axiom.

    Another axiom which may be helpful although not officially an axiom is the following
    non-descreteness
    (all x ( (exists y -C(x,y)) -> (exists z (C(z,x) & -O(z,x))))).
    Probably this can be proved by making use of the compl definition.

    A final axiom, which is almost certainly independent of the others and encodes a basic property of infinitely divisible space is the following:
    dense nesting
    (all x y (NTPP(x,y) -> (exists z (NTPP(x,z) & NTPP(z,y))).
     

    Some theorems proved by Dave Randell

    1) all x all y [PP(x,y) -> - Null(diff(y,x))]
    2) all x all y [PP(x,y) -> exists z[P(z,y) & -0(z,x)]]
    3) all x all y all z [P(z,prod(x,y)) <-> [P(z,x) & P(z,y)]]
    4) all x all y all z [C(z,diff(x,y)) <-> exists v [P(v,x) & -O(v,y) & C(z,v)]]
    5) all x EC(x,compl(x))
    6) all x compl(compl(x)) = x
    7) all x all y [P(x,y) <-> all z[O(z,x) -> O(z,y)]]
    8) all x all y [[PP(x,y) & Con(y)] -> EC(diff(y,x),x)]
    9) all x all y all z [[C(z,y) & -C(z,x)] -> exists w [Pwy & -O(w,x) & C(z,w)]]
    10) all x all y [PP(x,y) & Con(y) -> exists z [P(z,y) & EC(z,x)]]
    11) all x all y all z [C(z,diff(Y,x)) <-> exists v [P(v,y) & -O(v,x) & C(z,v)]]
    12) all x sum(x,compl(x)) = us
    13) all x all y O(y,x) or O(x,compl(y))
    14) all x all y [P(x,y) -> C(y,compl(x))]
    15) all x all y [NTPP(x,y) -> O(y,compl(x))]
    16) all x all y DR(x,y) <-> P(y,compl(x))]
    17) all x all y [PO(x,y) -> exists z [P(z,x) & -O(z,y)]]
    18) all x all y [-P(y,x) -> exists w [P(w,y) & -O(w,x)]]
    18) all x all y [O(z,compl(x)) -> -P(z,x)]
    - from C(z,compl(x)) <-> -NTPP(z,x) part of compl(x) defn only
    - no proof the other way though