Orchestrating a Network of Mereotopological Theories: An Abridged Report

1 Introduction

Mereology, the theory of parthood, is well-established in Ontology (philosophy), and is used widely in ontologies for the Semantic Web and other ontology-driven information systems. For instance, the medical terminologies openGalen (23 part-whole relations) [Rogers and Rector, 2000] and SNOMED CT, the Gene Ontology [Gene Ontology Consortium, 2000] that is used widely for database integration in the biological sciences, and the Foundational Model of Anatomy [Rosse and Mejino Jr, 2003] all use variants of mereology. Mereotopology is an extension of mereology with topological notions so that one can distinguish between interior part and tangential part. It is used in geographic information systems and for annotation of pictures and with it, one can infer, e.g., whether a country is landlocked; e.g., [Gr¨utter and Bauer-Messmer, 2007; Keet et al., 2012].

Due to the trade-offs between the expressiveness of logic languages and computational complexity, it has been difficult to represent mereology and mereotopology in full and such that one can obtain the desired inferences. Attempts include the extension of OWL with reflexivity and irreflexivity [Horrocks et al., 2006] and trade-off assessments for the OWL

∗This is an abridged version of a paper titled "Orchestrating a Network of Mereo(topo)logical Theories" which won the Best Paper award at the K-CAP 2017 conference, Dec. 4-6, Austin, Texas.

species on consequences for automated reasoning [Keet et al., 2012]. The most expressive Description Logics (DL)-based OWL language, OWL2 DL, creates further complications for the modeller due to expressiveness limitations on object properties. A concrete example of this is the choice between parthood's transitivity vs. its use with qualified number restrictions. This gives a modeller three options, using humans with their limbs and feet as example: 1) humans can have as part any number of limbs and infer that if a foot is part of a limb and a limb part of a human, then that foot is part of that human; 2) a (canonical) human has as part exactly four limbs but it cannot be inferred that the foot is part of the human; and 3) a human has exactly four limbs and we can make the (transitive) inferences about feet at the cost of scant tool support and poor performance compared to options 1 and 2, due to translating it to first-order logic (FOL) and calling a corresponding reasoner. If some OWL ontology O1 uses option 1 and OWL ontology O2 option 2, then importing or merging the ontologies leads to option 3-an OWL file outside of OWL2 DL-and undecidability in general. This lack of closure under modular combination is a rather unusual aspect for a logic-based modelling language (this problem does not exist in, e.g., FOL), and in the typical situation of ontology development with Prot´eg´e, this leaves the modeller stranded.

In sum, within the OWL context, it is confusing for the modeller as to which mereo(topo)logical theory to include, it does not meet the representation and reasoning requirements of the domain experts, computationally incompatible modelling choices may not be obvious, and yet for various scenarios different choices are applicable.

We aim to solve these issues by tying together two components. First, we structure the mereological theories, using a two-pronged approach. There are several recognised subtheories in the KGEMT mereotopology and there are established languages with their language features that can represent various subsets of those theories. We investigate this intersection and elucidate the maximum possible sub-theories for each language. They and their interactions are presented formally in a networked set of theories represented in the Distributed Ontology, Model, and Specification Language (DOL), as it was specifically designed for linking theories represented in different logics up to higher order logic. DOL is supported by a tool ecosystem (ontohub.org/Hets [Codescu et al., 2017a]) to select the appropriate reasoners for it, rather than sticking to one upfront. This resulted in 28 interconnected micro-ontologies-serving as basic versions of ontology design patterns-of mereology, topology, and mereotopology. A modeller then can choose which theory to include for which ontology usage scenario, and when to use the linking to a more expressive version when reasoning time is not crucial. Due to the interactions of language features that pushes an ontology into one fragment or another, we propose steps towards conflict resolution, which pinpoints automatically which axioms violate which logic, so that a modeller can make an informed decision.

2 Preliminaries

2.1 Mereotopology

The mereotopologies we focus on are based on [Varzi, 2007; Keet et al., 2012], building them up from the primitive parthood and connection relations up to the KGEMT mereotopological theory, as depicted in Fig. 1. Ground Mereology commences with the primitive part of relation that is transitive, reflexive, and antisymmetric (t1-t3) and Ground Topology commences with the reflexive and symmetric (t6,t7) connection relation. It is possible to construct a different lattice of mereo(topo)logical theories; the scope of this paper, however, is to present a reusable approach to represent and reason over a set of interconnected theories in different logics.

KGEMT does not (have to) exist in isolation. For instance, it may integrate with the DOLCE foundational ontology as it already incorporates GEM [Masolo et al., 2003] and other foundational ontologies rely heavily on theories of parts, such as BFO [BFO, last accessed July 2017], who are struggling to reconcile the expressive theories from Ontology with the practicalities of OWL and OBO. It could serve the many attempts in domain ontology development in, e.g., medicine and environment [Donnelly et al., 2006; Gr¨utter and Bauer-Messmer, 2007].

2.2 Logics

We zoom into logics with a considerable uptake and some tool support: the OWL family of languages [Cuenca Grau et al., 2008; Horrocks et al., 2003], FOL, and the newly standardised DOL [Kutz et al., 2010; Mossakowski et al., 2015].

Mereotopology and OWL The most recent standardised language in the OWL family is OWL2 [Motik et al., 2009], of which most sublanguages are based on DLs [Baader et al., 2008], which are decidable fragments of FOL that aim to find 'sweet spots' of the trade-offs between expressiveness and decidability. It is already problematic to represent even just Ground Mereology in OWL2 DL: antisymmetry (t3) is not supported, nor can one use both transitivity of proper parthood (t26) together with asymmetry (t27). Such issues increase the number of subtheories to deal with (e.g.: theory 15 vs. 16 in Table 1).

Relevant DOL features When two independently developed ontologies have to be reused as modules in a larger ontology, their differences will typically prevent them from working together properly due to, e.g., synonyms, homonyms, and the need for bridge axioms to link the ontologies appropriately [Euzenat and Shvaiko, 2013; Codescu et al., 2017b]. DOL aims to provide a unified metalanguage for handling this diversity [Kutz et al., 2010; Mossakowski et al., 2015]. It was approved as a standard of the Object Management Group (OMG) in 2016 [DOL, 2016]. DOL enjoys many distinctive features, including, among others: (1) structuring constructs for building ontologies from existing ontologies, like imports, union, forgetting, interpolation, and filtering; (2) module extraction; (3) various mappings between ontologies and (4) networks of ontologies.

DOL is designed as a multi-logic meta-language, already supporting all of the mainstream ontology languages in use today. The framework is based on the theory of 'institutions', abstracting from the peculiarities of syntax and semantics of particular logics; see [Goguen and Burstall, 1992; Kutz et al., 2010] for technical details.

3 Tying It TogetherWith DOL

Given the five mereo(topo)logical theories together with the DL-based OWL species with their feature trade-offs and exclusions, FOL, and HOL, then in combining them, one can construct 28 theories (presented fully in [Keet and Kutz, 2017]), which are the maximal subsets of the mereo(topo)logical theories per language. Note that there are not 227 theories, because not every combination of the 27 axioms makes sense ontologically. For instance, the combination of, say, t1 (reflexivity of parthood) and t16 (additivity of closure) into one theory is not meaningful, because i) the two are independent as such, for t1+t16 lacks the inclusion axiom (t14) that relates parthood with closure, and ii) each one misses characteristics deemed essential in ontology (transitivity and antisymmetry for parthood, and its definition and idempotence for closure, respectively).

The theories are available on OntoHub at https://ontohub.org/repositories/mereotopology, and the repository is currently being extended with further first- and second-order modelling and full structuring. For presentation purposes and anticipated usage, we present the structuring of the network of theories using DOL by focusing on the OWL species and extensions to OWL + FOL. From the DOL structuring point of view, second-order axioms can be dealt with in the same way, including SOL (a second-order sublogic of CASL), HasCASL (the higher-order extension of CASL), Common Logic, Isabelle/HOL and HOL-light, as well as THF; see [Mossakowski et al., 2014].

3.1 OrganisingMicro-Ontologies in DOL

The basic structuring operations for logical theories are available also on the logic-specific level. E.g., when working exclusively with OWL theories, we can employ the purely homogeneous DL-based OWL fragment of DOL, called DOWL [Kutz et al., 2016]. The most basic mechanisms relevant for the present paper that we gain, in terms of structuring, on top of OWL are the following: (1) control over signatures via renaming symbols along imports, (2) extending existing theories with new axioms (theory extensions), (3) unions of theories, (4) theory interpretation, (5) syntactic extraction of modules using specified symbols, and (6) lemma book-keeping and counterexample specification. Features 1-5 will be illustrated in this section; the two more advanced DOL features (item 6) will be discussed in Section 3.2. We begin by illustrating the idea of extending a theory by new axioms (feature 2). We use the simplest possible examples on purpose, to illustrate the underlying ideas as clearly as possible.

Extensions We extend theory8 (OWL2 EL/QL) into theory4 (OWL2 QL) by adding symmetry (t7):

logic OWL2.QL ontology theory4 = theory8 then ObjectProperty: C Characteristics: Symmetric %(t7)

Unions We simultaneously illustrate unions of theories (feature 4) with control over signatures (feature 1). The union of theory7 (OWL2 EL) and theory11 (OWL2 RL) results in theory2, expressed in OWL2 QL. To illustrate how we can directly manage signatures, the given theories use diverging vocabulary for talking about connection, which is a very common phenomenon in practice.

logic OWL2.QL ontology theory2 = theory7 with Con |- > C and theory11 with Co |- > C

The result is a theory that combines the axioms of theories 7 and 11, with a unified signature for connection, using the symbol C.

Theory Interpretation To continue the previous example, clearly, theory7 (or theory11) can be interpreted into theory2 by mapping the symbol Con to C. According to the semantics of theory interpretation, theory2 can then prove all the consequences of theory7, under this translation (see [Kutz et al., 2010] for a more detailed discussion of interpretations).

Heterogeneous DOL: Logic translation The heterogeneous case, i.e., when moving from a weaker logic (say, OWL DL) to a more expressive one (say, full FOL) is a specific strength of DOL. We illustrate this by extending theory6 (in OWL2 EL) with antisymmetry and weak supplementation (this is 'almost' theory20 (in FOL), however still lacking the definitions of O and EQ), as follows:

logic CASL.FOL ontology theory6_plus_antisym_and_WS = theory6 with translation OWL22CASL then forall x,y:Thing . P(x,y) /\ P(y,x) => x =y %%(t3) forall x,y:Thing . not P(y,x) => exists z:Thing . P(z,y) /\ not O(z,x) %%(t4)

Definitional Extensions Definitional extensions are one of the most basic tools in ontology design (cf., e.g., DOLCE) and can be specified explicitly in DOL. Indeed, they are one of the basic structuring means to organise mereotopological theories: e.g., proper part of (PP) and overlap (O) can be defined in terms of part of (P), and tangential proper part of (TPP) in terms of part of and connection.

Technically, a definitional extension with a definition of, e.g., overlap (O) consists of a signature extension with the binary predicate symbol O(x, y), together with the basic definition of O in terms of P. More formally, a theory T2 in signature σ′ is a definitional extension (%def) of theory T1 in signature σ, if any T1-model has a unique expansion to a T2model. Intuitively, T2 adds neither additional constraints nor additional freedom of interpretation to T1, but rather the new symbols in T2 are uniquely defined in terms of the symbols in T1 [Kutz et al., 2010]. Note that it is a slightly different situation when previously introduced symbols, even if unaxiomatised, are augmented with definitions (which is in general neither definitional nor conservative). We say that T2 is a weakly definitional theory extension (%wdef) of T1 if each realisation of T1 can be expanded to at most one realisation of T2. All these requirements can be expressed in DOL. We complete the previous incomplete definition of theory20 as follows:

logic CASL.FOL ontology theory20 = theory6_plus_antisym_and_WS then %wdef . forall x,y:Thing . O(x,y) <=> exists z:Thing (P(z,x) /\ P(z,y)) %(t21) . forall x,y:Thing . EQ(x,y) <=> P(x,y) /\ P(y,x) %(t22)

The result is a complete specification of theory20, where the previously undefined symbols O and EQ have been augmented with their formal definitions.

DOL network and colimits The entire network of 28 theories can be formally represented as a DOL network, written as follows:

network KGEMT_network = theory1,...,theory28,M1,...,Mp

Here, the theories theory1-theory28 are listed, followed by the defined theory interpretations Mi connecting the various ontology nodes.

Since the network explores the subtheories of KGEMT along the dimensions of language expressivity and ontological soundness, there are no conflicting logical statements among the 27 axioms. In fact, DOL's combination technique (based on computing colimits of the network) can compute the colimit of the network of theory1-theory28 resulting in the full KGEMT.

All 28 theories live in subsignatures of the full KGEMT, where some, but not all, have different signatures. E.g., MT's signature does not have parthood, and GEM does not have connection and enclosure, and neither has closure, interior, and exterior that are part of KGEMT's axioms only.

ontology KGEMT = combine KGEMT_network

Moreover, the network construct allows us to exclude certain mappings and ontology nodes. Therefore, we can select a language species, and compute the maximal combination of subtheories that live in that species. Note, as discussed earlier, that this might lead to a theory outside of the logic species for some logics, such as OWL2 DL, but this will not occur for OWL2 EL or FOL sub-networks.

3.2 Lemmas, Consistency, and Countermodels

When using one or more of the 28 mereotopological theories, it is important to keep track of the desired consequences of the theories and to record counterexamples of properties that do not follow from the current theory. Both features are supported by DOL, as discussed next.

Keeping track of consequences We continue the example from above. If proper part of is introduced definitorially then we expect its typical properties to be entailed by the definition. This depends on how precise part of was axiomatised. We can augment any given theory with a definition of PP, and record the consequences, as follows:

logic CASL.FOL ontology theory20_with_PP_lemmas = theory20 then %wdef . forall x,y: Thing . PP(x,y) <=> P(x,y) /\ not P(y,x) then %implies .forall x,y: Thing . not PP(x,x) %(t25) .forall x,y,z: Thing . PP(x,y) /\ P(y,z) => PP(x,z) %(t26) .forall x,y,z: Thing . PP(x,y) => not PP(y,z) %(t27)

Assuming the stated theory, the declared lemmas (sentences in the present logic), namely, the three axioms listed after the annotation %implies, are logical consequences of the theory. This specification therefore introduces proof obligations, i.e., forces a connected automated reasoner to prove the axioms (t25)-(t27) from the theory specified before.

Relative consistency and countermodels Proving consistency of the theories is easy for the OWL-based ones, for one simply can use one of the OWL2 reasoners. Theories 1-19 have been checked as such, and are consistent according to those reasoners. However, as soon as we move away from OWL to FOL, establishing consistency can be extremely difficult with current automatic reasoning capabilities.

We outline how in DOL we can specify and verify automatically the consistency of adding axioms to an existing theory, and how to prove that a theory admits unintended models. This is possible with theory interpretation and formal specification of models. A model can be declaratively specified as a logical theory with exactly one model up to isomorphism (there is standard approaches for this in the literature). For instance, to prove that theory23 is consistent, one specifies a finite model in a specification M which we assume uses symbols co, e, P and write the following interpretation:

logic CASL.FOL interpretation Cons : theory23 to M = C |-> co, E |-> e

By definition of theory interpretation, 'Cons' is correct iff every model of M reduced along the morphism defined in Cons is a model of theory23. NowM specifies a fixed model and thus proving the interpretation correct (the axioms of theory23 hold on M) establishes consistency. The same technique can be used to show that a theory T is both consistent and admits counterexamples to specific principles, by interpreting T into a model M that violates principle φ. Here, the heterogeneous features of DOL are a powerful tool, since the countermodel can be specified in a more expressive logic (e.g., FOL) than the theory that we interpret (e.g., OWL2 EL). A very simple example: the mereology in theory15 leaves out antisymmetry, which clearly has unintended models. We can specify in FOL a non-well-founded model for part of, and by interpreting theory15 into this model, give formal proof that theory15 admits such models.

4 Conclusion

We have presented an overview of a network of 28 modular ontologies in DOL (more fully presented in [Keet and Kutz, 2017]), relating various fragments of the KGEMT mereotopological theory and its five sub-theories, which was driven by the expressiveness of the six DL-based OWL species and first and second order logic.

Work has commenced with resolution of feature conflicts among the OWL species with the OWL classifier tool, informing a modeller about language violations in order to make informed decisions; its preliminary results and usage scenarios are described in [Keet and Kutz, 2017]. Future work includes extending this network with incompatible extensions, such as atomicity and gunk, as well as a detailed specification of countermodels, formal consistency proofs, and the exploration of logic-specific sub-networks.