Axioms for
"A Theory of Multidimensional Qualitative Space:
Semantic Integration of Spatial Theories that Distinguish Interior from Boundary Contact"

Torsten Hahmann and Michael Gruninger

Extended abstract submitted to Conference of Spatial Information Theory (COSIT) 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.

---

qs
|
|-- dim
|   |-- dim_prime_linear (Theory of linear dimension)
|
|-- cont
|   |-- cont_basic (Theory of basic spatial containment)
|   |-- cont_ext (Theory of extensional spatial containment)
|   |-- cont_c (Theory of basic spatial containment with contact)
|   |-- cont_c_ext (Theory of extensional spatial containment with contact)
|
|-- zex
|   |-- zex (Axiom forcing the existence of a zero entity)
|
|-- codi
|   |-- codi_linear (Basic theory of linear dimension, extensional containment, and contact)
|   |-- codi_int (Theory of linear dimension, extensional containment, and contact with mereological closures under intersections)
|   |-- ep_ext (Axiom forcing extensionality of parthood)
|   |-- codi_down (Theory of linear dimension, extensional containment, and contact with mereological closures under intersections
|                  and differences for equidimensional proper parts)
|   |
|   |-- defs
|   |   |-- ep (Definition of equidimensional parthood P)
|   |   |-- epp (Definition of equidimensional proper parthood PP)
|   |   |-- po (Definition of partial overlap PO)
|   |   |-- inc (Definition of incidence Inc)
|   |   |-- sc (Definition of superficial contact SC)
|   |   |-- min_max_in_dimension (Definitions of minimal and maximal entities within a dimension)
|   |   |-- connected (Definitions of self-connectedness, interior connectedness, and uniform connectedness)
|
|-- codid 
    |-- codib (codi_down with BCont) (Theory of linear dimension, extensional containment, and contact with mereological closures under intersections
                                      and differences for equidimensional proper parts and a primitive relation of boundary containment)

---

Consistency of the full theory CODIB

An automatic translation of the full theory CODIB from CommonLogic into the LADR syntax of Prover9: codib.all.p9
and finally into to the TPTP syntax: codib.all.tptp

A non-trivial model of CODIB using the input file where

• y and z are superficially connected, but the entity x contained in both is only in the boundary of y;
  
• R is a non-self-connected entity (with two complementary proper parts t and s);
  
• t and x are incidence (t being of lesser dimension than x) and there is a v that is in the boundary of both.
  

In the model the extensions of all primitive and defined relations are non-empty, thus we call it a "non-trivial model" (implying not only that the theory is consistent, but also that consistent models do not rule out that certain relations actually hold).

---