Automated proofs for
"A naive theory of dimension for qualitative spatial relations"

Torsten Hahmann and Michael Gruninger

The paper has been accepted for a full presentation at CommonSense 2011


All modules of the proposed ontology are specified in CommonLogic and will eventually be included in the COLORE repository. We used Chris Mungall's cltools (in particular clif-to-prover9) to translate common logic to ladr, the format required by Prover9 and Mace4. In the following the modules used for all proofs as well as the proof outputs.

D - Theory of dimension (Section 2)

Basic theory of dimension (D-A1 to D-A10) dim_basic

Two mutually inconsistent extensions:
Zero region exists (Z-A1 to Z-A3) dim_zex: extending non-conservatively any theory extending dim_basic
No zero region (Z-A4) dim_nozex: extending non-conservatively any theory extending dim_basic

Definitional extension: Dimension definitions (D-D1 to D-D5) dim_def: extending any theory extending dim_basic
Proofs: D-T1, D-T2, D-T3, D-T4, D-T5, D-T6

Bounded dimension (D-E1 to D-E3) dim_bounded: extending dim_basic non-conservatively

Linear dimension (D-E4) dim_linear: extending dim_basic non-conservatively

Consistency

Model of {dim_basic, dim_zex, dim_bounded, dim_linear}
Model of {dim_basic, dim_nozex, dim_bounded, dim_linear}

C - Theory of containment (Section 3)

Basic theory of containment (C-A1 to C-A4) cont_basic
Two mutually inconsistent extensions:
Zero region exists cont_zex: extending non-conservatively any theory extending cont_basic
No zero region cont_nozex: extending non-conservatively any theory extending cont_basic

Theory of containment and contact (C-D, C-A5) cont_c: extending cont_basic non-conservatively
Proofs: C-T1, C-T2, C-T3, C-T4

Consistency

Model of {cont_basic, cont_c, cont_zex}
Model of {cont_basic, cont_c, cont_nozex}

CD - Interaction of dimension and containment (Section 4)

Theory of containment and dimension (CD-A1) cont_dim: extends cont_basic dim_basic conservatively

Indivisible atoms in the theory of containment and contact (CD-E1) cont_atom: extends cont_basic dim_defs and thus also cont_dim non-conservatively

Definitional extension: Parthood (P-D) p: extends cont_dim
Proofs: P-T1, P-T2, P-T3, P-T4, P-T5, P-T6, P-T7, P-T8

Definitional extension: Partial overlap (PO-D) po: extends cont_dim and uses the definition p
Proofs: P-T1, P-T2, P-T3

Definitional extension: Incidence (INC-D) inc: extends cont_dim and uses the definition p
Proofs: INC-T1, INC-T2, INC-T3, INC-T4, INC-T5, INC-T6

Definitional extension: Superficial Contact (SC-D) sc: extends cont_dim
Proofs: SC-T1a (->), SC-T1b (<-), SC-T2, SC-T3, SC-T4

Exhaustiveness and disjointness of the contact relations: Proofs that the contact relations PO, Inc, and SC are exhaustive with respect to C and pairwise disjoint
CD-T1, CD-T2, CD-T3, CD-T4, CD-T5, CD-T6, CD-T7, CD-T8, CD-T9, CD-T10

CD-T1 to CD-T4 form the conservative extension c_exhaustive_lemmas of cont_dim
CD-T5 to CD-T10 form the conservative extension c_disjoint_lemmas of cont_dim

Consistency of the full theory

An automatic translation of the full theory from the LADR syntax of Prover9 to the TPTP syntax can be found here: {dim_cont, p, po, inc, sc, dim_zex, dim_bounded, dim_linear}

Non-trivial model of {dim_cont, p, po, inc, sc, dim_zex, dim_bounded} where


Model found by Paradox3 of {dim_cont, p, po, inc, sc, dim_zex, dim_bounded, dim_linear} using the TPTP input file where

I - INCH Calculus (Section 5.1)

Definitional extension: Definition of INCH (I-D) inch: extends {dim-cont, p, dim_zex, dim_linear}

Definitional extension: Definitions in INCH (I-D1 to I-D5) inch_basic: extends inch. We omit the trivial definitions (I-D7 to I-D9) but prove I-D6
Proofs: I-D6, I-PA3, I-PA4, I-PA5, I-PA6, I-PA7
Proofs of the mappings (we split proofs of the directions of the implication as well as disjunctions):
I-M1a, I-M1b, I-M2a, I-M2b, I-M3, I-M4, I-M5 (see also the explanation in the input of I-M5), I-M6a, I-M6b, I-M7a, I-M7b, I-M7c

Restriction to the models of the INCH Calculus (I-PA1, I-PA2, I-PA8 to I-PA10): inch_full = {inch_basic, inch_ext, inch_pa8, inch_closure}
Proofs that in inch_full I-M1R implies I-M3R, I-M4R, I-M5R, and I-M7R.

Consistency

Non-trivial model of inch_def
Trivial model of inch_full

RCC - Region Connection Calculus (Section 5.2)

Definitional extension: Definitions of `regions' (here Region, in the paper R), non-zero regions (NZRegion) and `region part' (here RegionPart, in the paper RP) (RCC-D1 to RCC-D3) dim_eq_defs: extends {dim-cont, p, dim_zex, dim_linear, dim_bounded}

Restriction to the models of the Region Connection Calculus (RCCA1 to RCC-A7): dim_eq_axioms extends dim_eq_defs non-conservatively
Proofs: Unfortunately, the theorem RCC-T1 cannot be proved automatically, but it is well-known to follow from the remaining axioms.

Consistency

It is difficult to verify consistency for a theory with only infinite models. However, Prover9 failed to derive an inconsistency. Moreover, if we remove RCC-A5 (extensionality of C amongst regions), RCC-T1 is not entailed any longer and we can generate various C-extensional models (satisfying C-E1; e.g. models of size 7, size 8, size 9) whose `regions' form the smallest non-trivial Boolean lattice with 4 elements.