the Region Connection Calculus

[dr.mt...@gmail.com]

This is a research area about the relations between regions.  It looks like set theory in part because it is built on a single relation c (is connected) which mirrors Î in many ways.  RCC is a first-order theory which is part of mereology, the study of parts and wholes.   Professor Cohen, my colleague at Leeds, researched this area and hence my acquaintance with it.

The basic rules are everything is connected with itself and c is symmetrical.  

Everything else is built up from c - including part p and proper part pp.  Here is RCC in THORN notation.

(define rcc

   {--> symbol}

   -> (kb->  [[all x [c x x]]
    [all x [all y [[c x y] => [c y x]]]]
    [all x [all y [[dc x y] <=> [~ [c x y]]]]]
    [all x [all y [[p x y] <=> [all z [[c z x] => [c z y]]]]]] \\ part
    [all x [all y [[pp x y] <=> [[p x y] & [~ [p y x]]]]]] \\ proper part
    [all x [all y [[e x y] <=> [[p x y] & [p y x]]]]]
    [all x [all y [[o x y] <=> [exists z [[p z x] & [p z y]]]]]]  \\ overlaps
    [all x [all y [[po x y] <=> [[o x y] & [[~ [p x y]] & [~ [p y x]]]]]]]
    [all x [all y [[ec x y] <=> [[c x y] & [~ [o x y]]]]]]
    [all x [all y [[dr x y] <=> [~ [o x y]]]]]
    [all x [all y [[tpp x y] <=> [[pp x y] & [exists z [[eq z x] & [ec z y]]]]]]]
    [all x [all y [[ntpp x y] <=> [[pp x y] & [~ [exists z [[eq z x] & [ec z y]]]]]]]]])

The command (rcc) returns compiled showing that this theory is compiled into THORN.

You see that RCC is largely composed of equivalences.  These generate a lot of clauses and hence in THORN, a lot of code.  At this level the branching rate of the search space is large.   

There are a lot of theorems about RCC which are gathered together here.  If I try one in THORN

(<-kb [[[tpp a b] & [ec b c]] => [[dc a c] v [ec a c]]])

THORN goes into a coma; the solution is too far out in search space.

PROVER 9, a very powerful system from Argonne, will compute a solution.  

% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.00) seconds.
% Length of proof is 36.
% Level of proof is 7.
% Maximum clause weight is 12.
% Given clauses 632.

3 (all x all y (dc(x,y) <-> -c(x,y))) # label(non_clause).  [assumption].
4 (all x all y (p(x,y) <-> (all z (c(z,x) -> c(z,y))))) # label(non_clause).  [assumption].
5 (all x all y (pp(x,y) <-> p(x,y) & -p(y,x))) # label(non_clause).  [assumption].
7 (all x all y (o(x,y) <-> (exists z (p(z,x) & p(z,y))))) # label(non_clause).  [assumption].
9 (all x all y (ec(x,y) <-> c(x,y) & -o(x,y))) # label(non_clause).  [assumption].
11 (all x all y (tpp(x,y) <-> pp(x,y) & (exists z (ec(z,x) & ec(z,y))))) # label(non_clause).  [assumption].
13 tpp(x,y) & ec(y,z) -> dc(x,z) | ec(x,z) # label(non_clause) # label(goal).  [goal].
14 dc(x,y) | c(x,y).  [clausify(3)].
16 -dc(c1,c3).  [deny(13)].
18 -pp(x,y) | p(x,y).  [clausify(5)].
20 -tpp(x,y) | pp(x,y).  [clausify(11)].
28 o(x,y) | -p(z,x) | -p(z,y).  [clausify(7)].
29 -o(x,y) | p(f2(x,y),x).  [clausify(7)].
30 -o(x,y) | p(f2(x,y),y).  [clausify(7)].
33 -ec(x,y) | -o(x,y).  [clausify(9)].
34 ec(x,y) | -c(x,y) | o(x,y).  [clausify(9)].
46 tpp(c1,c2).  [deny(13)].
49 -tpp(x,y) | p(x,y).  [resolve(20,b,18,a)].
73 -p(x,y) | -c(z,x) | c(z,y).  [clausify(4)].
74 p(x,y) | c(f1(x,y),x).  [clausify(4)].
75 p(x,y) | -c(f1(x,y),y).  [clausify(4)].
77 ec(c2,c3).  [deny(13)].
78 -ec(c1,c3).  [deny(13)].
79 c(c1,c3).  [resolve(16,a,14,a)].
82 -ec(x,y) | -p(z,x) | -p(z,y).  [resolve(33,b,28,a)].
83 ec(x,y) | -c(x,y) | p(f2(x,y),x).  [resolve(34,c,29,a)].
84 ec(x,y) | -c(x,y) | p(f2(x,y),y).  [resolve(34,c,30,a)].
87 p(c1,c2).  [resolve(49,a,46,a)].
98 p(x,y) | -p(x,z) | c(f1(x,y),z).  [resolve(74,b,73,b)].
105 p(f2(c1,c3),c1).  [resolve(83,b,79,a),unit_del(a,78)].
108 p(f2(c1,c3),c3).  [resolve(84,b,79,a),unit_del(a,78)].
185 p(f2(c1,c3),x) | c(f1(f2(c1,c3),x),c1).  [resolve(105,a,98,b)].
202 -p(f2(c1,c3),c2).  [ur(82,a,77,a,c,108,a)].
350 -c(f1(f2(c1,c3),c2),c2).  [ur(75,a,202,a)].
1222 -c(f1(f2(c1,c3),c2),c1).  [ur(73,a,87,a,c,350,a)].
3697 $F.  [resolve(1222,a,185,b),unit_del(a,202)].

============================== end of proof ==========================

PROVER 9 does 1.7 million inferences per minute vs THORN which which would do perhaps a billion in the same time.   But PROVER9 wins.  Why is that and can this situation be changed?   I'll come back to this.

Mark

[dr.mt...@gmail.com]

The answer to why THORN comes off worse than PROVER 9 while being so much faster has to do with the control of search space

and memory.   THORN is a near-Prolog theorem prover that inherits the limitations of Prolog with respect to memory.  That is, THORN

has no global memory of what it has searched.   If it finds a node it has searched before, it will search again.  PROVER 9 uses breadth first

search and retains a global memory space for eliminating bad nodes.  For example, out of 1.6 million clauses, all but 38,000 were rejected

by analysing the search space.  This, and a battery of special techniques is what makes PROVER 9 so powerful.

Can THORN be changed to be more like PROVER 9 but with the same fast performance?   IMO, yes.  And even better, we could actually create

a massively parallel THORN which could do billions of inferences per second.  A system measured in GLips (gigalips).    I'm going to

talk with Professor David Hogg about setting that up using Chez Scheme on a supercomputer.   It might be a showpiece research.

In the meantime, I'll continue to improve THORN 5 and as you will see we'll crack RCC.

Mark