Ontology Validation as Dialogue Michael GRÜNINGER a a Department of Mechanical & Industrial Engineering, University of Toronto, Canada Abstract. Ontology verification is concerned with the relationship between the in- tended models of an ontology and the models of the axiomatization of the ontology. An even more difficult challenge is ontology validation – are the intended mod- els of the ontology indeed the correct models for the ontology? The identification and specification of the intended models of an ontology is inherently a dialogue between the user of the ontology (who implicitly knows the intended models) and the ontology designer (who is attempting to axiomatize the class of intended mod- els). In this paper we explore techniques for eliciting intended models from the user and evaluating these models with respect to user responses. We consider how this procedure can be applied to several first-order ontologies. Keywords. ontology design, verification, validation, intended models 1. Introduction The design of high quality ontologies is an overarching challenge for the applied ontol- ogy community. Following Ontology Summit 2015, we consider ontologies to be arte- facts that are designed with respect to a set of requirements, analogous to software engi- neering. In particular, these requirements may be characterized by the class of structures which capture the intended semantics of the signature of the ontology. If we carry the analogy of software engineering further, we see that ontology evaluation also focuses on verification and validation. Ontology verification is concerned with the relationship between the intended models of an ontology and the models of the axiomatization of the ontology. An even more difficult challenge is ontology validation – are the intended models of the ontology indeed the correct models for the ontology? In this paper, we take the position that the identification and specification of the in- tended models of an ontology is inherently a dialogue between the user of the ontology (who implicitly knows the intended models) and the ontology designer (who is attempt- ing to axiomatize the class of intended models). After an overview of ontology verifica- tion and validation, we motivate the need for an interactive approach by considering three large first-order ontologies. We then propose a procedure for eliciting intended models from the user and evaluating these models with respect to user responses. Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 2. Ontology Evaluation 2.1. Ontology Verification When selecting or developing an axiomatization of an ontology1 for an application do- main, the knowledge engineer typically has some requirements in mind. These require- ments for the ontology are specified with respect to the intended semantics of the ter- minology; from a mathematical perspective the requirements may be characterized by the class of structures which capture the intended semantics, and such structures can be referred to as the required structures for the ontology. Previous work in this approach [1,2] has focused on the case in which the required models and the axioms of the on- tology have the same signature. In this case, the correctness of the ontology is defined with respect to the relationship between the required structures for the ontology (which we will denote by Mreq ) and the models of its axiomatization Tont (see Figure 1). If the ontology is too weak, then there exist models which are spurious (that is, they are not required structures): M ∈ Mod(Tont ) and M 6∈ Mreq If the ontology is too strong, then there exist required models which are omitted: M ∈ Mreq and M 6∈ Mod(Tont ) In other words, an axiomatization is correct if and only if it does not include any spurious models, and it does not omit any required models: M ∈ Mod(Tont ) iff M ∈ Mreq (C) Verification is therefore concerned with the relationship between the intended mod- els of an ontology and the models of the axiomatization of the ontology. In particular, we want to characterize the models of an ontology up to isomorphism and determine whether or not these models are equivalent to the intended models of the ontology. This relationship between the intended models and the models of the axiomatization plays a key role in the application of ontologies in areas such as semantic integration and deci- sion support. We can say that two software systems are semantically integrated if their sets of in- tended models are equivalent. However, systems cannot exchange the models themselves – they can only exchange sentences in the formal language that they use to represent their knowledge. We must be able to guarantee that the inferences made with sentences exchanged in this way are equivalent to the inferences made with respect to the system’s intended models – given some input the application uses these intended models to infer the correct output. In the area of decision support, the verification of an ontology allows us to make the claim that any inferences drawn by a reasoning engine using the ontology are ac- 1 By an ontology, we mean an axiomatic theory in the language of first-order logic. We, therefore, use the words ‘ontology’ and ‘theory’ interchangeably. We consider a theory to be a set of first-order sentences closed under logical entailment, and a subtheory to be a subset of the corresponding theory. For a theory T , Mod(T ) denotes the class of all models of T . Conceptualization C Logical language L Models Ontology models MD(L) OK Intended models IK(L) Unintended models Omitted models Figure 1. The possible relationships between the models of an ontology and the required structures (modi- fied after [2]). Note that Guarino’s notions of intended and unintended models corresponds to our notions of required and spurious structures. tually entailed by the ontology’s intended models. If an ontology’s axiomatization has unintended models, then it is possible to find sentences that are entailed by the intended models, but which are not provable from the axioms of the ontology. Unfortunately, it can be quite difficult to characterize the models of an ontology up to isomorphism. Ideally, since the classes of structures that are isomorphic to an on- tology’s models often have their own axiomatizations, we should be able to reuse the characterizations of these other structures. 2.2. Ontology Validation If ontology verification is concerned with the relationship between the models of the axioms of the ontology and the intended models for the ontology, ontology validation addresses the problem of whether the intended models are actually the right ones for the user. Following the Ontology Application Framework developed during Ontology Sum- mit 2013, there are three major kinds of applications that motivate the design of ontolo- gies – search, decision support, and semantic integration. Ontology validation seeks to evaluate the ontology with respect to its application. When integrating software applications, we are faced with the additional challenge that almost no application has an explicitly axiomatized ontology. We can model a soft- ware application as if it were an inference system with a formal ontology, and use this ontology to predict the set of sentences that the inference system decides to be entailed or satisfiable. This approach, known as the Ontological Stance ([3]), is an operational characterization of the set of intended models for the application’s terminology. The Ontological Stance also addresses the relationship between the intuitions and the intended models; this is, of course, informal, but we can consider the domain intu- itions as providing a physical interpretation of the intended models. In this sense, we can adopt an experimental or empirical approach to the evaluation of the class of intended models in which we attempt to falsify these models. If we can find some objects or be- haviours within the domain that do not correspond to an intended model, then we have provided a counterexample to the class of model. In response, we can either redefine the scope of the class of models (i.e. we do not include the behaviour within the characteri- zation of the models) or we can modify the definition of the class of models so that they capture the new behaviour. If a software application already has an ontology, then the Ontological Stance can be used to evaluate the ontology with respect to the application’s intended models. This is distinct from ontology verification – even if we have a complete characterization of all models of the ontology’s axiomatization, the models of the ontology may not be intended models. Using the Ontological Stance, if the models of the application ontology are not equivalent to the intended models, then there are two possibilities: 1. there exists a model M of the ontology’s axioms T that is not an intended model; 2. the intended models entail some sentence Φ that is not entailed by the axioms T . These two possibilities provide the fundamental distinctions that we need to imple- ment any procedure for ontology validation. 3. Case Studies The challenges of ontology verification and validation can be illustrated with several large first-order ontologies. 3.1. MoSt The field of medicinal chemistry involves the design, synthesis, and development of new drugs that can be further enhanced with the application of ontologies. The work of [4] introduces a molecular structure ontology MoSt to aid in the task of drug discovery. MoSt combines conventional graph theory and ontological approaches to describe the shape of molecules. This ontology allows us to consider molecules from the shape perspective by identifying basic functional groups of the ring and chain types, and to use the axioms of the ontology to combine these functional groups together. The verification of MoSt proves that models of MoSt correspond to the class of tripartite incidence structures for cyclic and path subgraphs of a graph. Intuitively, the graph is isomorphic to the structure axiomatized by ontologies for conventional chem- ical graph theory, in which atoms are the vertices and bonds are the edges. Primitive functional groups are either chains (which are path subgraphs of the molecular graph) or rings (which are cyclic subgraphs of the molecular graph). Intended models of MoSt correspond to physically realizable molecules, so that the validation problem is composed of two parts: 1. Every molecule is a model of the ontology. 2. Every model of the ontology is a molecule. Molecules are Models of MoSt Molecules that currently exist and are chemically feasi- ble are named in accordance with the IUPAC naming rules from which an unambiguous structural formula can be created, which in turn can be used to build the underlying chem- ical graph. The MoSt Ontology axiomatizes the chemical graphs by taking the graphs and decomposing them into their primitive functional groups, and then re-composing them again via an attachment theorem. Furthermore, MoSt has the property that two models of the ontology can be combined together to form another model of the ontology. Con- sequently, we can say that all IUPAC-named molecules that have underlying chemical graphs are therefore models of the ontology. Models of MoSt are (Chemically Feasible) Molecules Conversely, a model of MoSt is essentially a chemical graph: we can give this graph to a chemist and ask her to deter- mine whether it is possible to synthesize the molecule. Whether or not a chemical graph can be physically realized is dependent on the difficulty of the synthesis process, along with the number of steps required. The motivation for MoSt is that a model can result in a potential molecule that has not yet been discovered and physically realized. Drug dis- covery becomes the process of building models by answering queries with the ontology and constructing models of the ontology using additional constraints and extensions. To prove that the models of MoSt are indeed molecules therefore requires a dialogue with users of the ontology. Models of MoSt are generated and then presented to medicinal chemists. If they reject a model (i.e. it is not a feasible molecule), we would need to generate new axioms to eliminate the model. In other words, user interaction is needed to identify and eliminate unintended models. To guarantee that there are no omitted models (i.e. physically feasible molecules that are not models of MoSt), we can search through existing molecule knowledge bases (e.g. ChemSpider) to verify that each molecule is a model of MoSt. We first generate molecular descriptions from IUPAC names and then construct models of the molecular descriptions; in such a case, no user interaction is required. 3.2. BoxWorld The BoxWorld Ontology Tboxworld ([5]) is a modular first-order ontology of shape that supports intelligent manufacturing and commonsense reasoning about cutting, joining, and folding sheets of materials such as cardboard and metal. The verification of Tboxworld demonstrates that models of Tboxworld are equivalent to mathematical structures that are generalizations of polyhedra and abstract polytopes. The question remains, though, as to exactly which shapes are models of Tboxworld . In particular, are all intuitive shapes also models of the axioms? Are there models of the axioms which do not correspond to intuitive shapes? Tboxworld has no omitted models iff all physically possible shapes are models of Tboxworld . Tboxworld has no unintended models iff all models of Tboxworld are physically possible shapes. To some extent, ontology verification can address this by providing representation theorems that characterize the models up to isomorphism; however, by itself, this does not give any indication of whether or not the models are intended. Who judges the feasibility of a shape? An additional difficulty in this regard is that the answer might indeed vary across different users. An ontology for shapes composed of surfaces also has applications in sheet metal fabrication, in which products are man- ufactured by folding, cutting, and joining pieces of sheet metal. A shape ontology for sheet metal processes would be able to answer questions such as: • What objects can we make from a single sheet of metal, either by cutting or fold- ing? • What objects can we make from joining multiple surfaces? On the other hand, an ontology of shape for furniture might well have a different set of intended models. As a result, there is no single correct answer to the problem of specifying intended models. Instead, we need a flexible way of allowing different users to interact with the ontology and specify those models that are intended from their perspectives. 3.3. CardWorld Vision The CardWorld Vision Ontology Tcardworld vision provides an axiomatization of images and depiction for 2D polygonal surfaces in scenes with occlusion and noise (errors in edge detection). It consists of eight modules that axiomatize intuitions about scenes, im- ages, depiction, and occlusion for 2D polygonal surfaces. Strictly speaking, we only need to show that a model exists in order to demonstrate that a theory is satisfiable. However, for ontology validation, we need a complete characterization of the possible models. For example, since we are considering the domain of computer vision, to show that a theory is satisfiable, we need only specify an image and scene which together with the axioms are satisfied by some structure. The problem with this approach is that we run the risk of having demonstrated satisfiability only for some restricted class of images, scenes, or surfaces. For example, a theory of scenes and images may be shown to be consistent by constructing a satisfying interpretation, but the interpretation may require that there is no occlusion in the scene; although such a model may be adequate for such scenes, it would in no way be general enough for our purposes. Tcardworld vision is supposed to support a comprehensive theory of 2D image interpretation, so we need to explicitly characterize the classes of images, scenes, surfaces, and other assumptions which are guaranteed to be satisfied by the specified structures. For example, within CardWorld, we are only con- sidering 2D surfaces which are opaque, which are not self-occluding, which cannot inter- penetrate each other. In addition, we are not considering scene features such as colour, surfaces markings, or texture. Since these properties are not considered within the scope of the ontology, they are not formalized within any structures. Of course, if someone wished to represent these properties, then they would need to extend the class of intended structures appropriately. Tcardworld vision has no omitted models iff all interpretations of the image are mod- els of Tcardworld vision . In other words, an omitted model exists if there exists a possible interpretation of the image that is not a model. On the other hand, Tcardworld vision has no unintended models iff all models of Tcardworld vision are possible interpretation. Unin- tended models are not a problem for Tcardworld vision , but omitted models are – how do we have a sense of all possible interpretations of an image, particularly in cases where there is heavy noise? One approach is to use annotation by users – given an image, the user specifies which scene objects are depicted by which image objects, which image objects are noise, and which objects are undepicted (either by occlusion or because of noise). However, this typically identifies only one possible interpretation of the image. People abandon such a preferred interpretation only when presented with refuting evidence (in which case the interpretation is not actually a model). The relationship between the intuitions and the structures is, of course, informal, but we can consider the domain intuitions as providing a physical interpretation of the structures. In this sense, we can adopt an experimental or empirical approach to the eval- uation of the class of intended structures in which we attempt to falsify these structures. If we can find some objects or behaviour within the domain which do not correspond to an intended structure, then we have provided a counterexample to the class of structures. In response, we can either redefine the scope of the class of structures (i.e. we do not include the behaviour within the characterization of the structures) or we can modify the definition of the class of structures so that they capture the new behaviour. 3.4. Upper Ontologies Upper ontologies characterize the semantics of general concepts that underlay every knowledge representation enterprise. Since upper ontologies are expected to be broadly reused, verifying that they do not have unintended models and that they are not missing any intended models are of paramount interest for the knowledge representation commu- nity. Work has been initiated on the verification of upper ontologies. For example, in [6] and [7], a number of novel classes of mathematical structures were axiomatized in order to adequately represent the models of DOLCE. A much more difficult challenge is the validation of upper ontologies. How do we discover the models that the designers of upper ontologies intended? For example, the work of [8], a model of SUMO-Time was discovered in which there was not a linear ordering over the set of timepoints. This is unusual insofar as most other time ontologies enforce linearity, but absent any interaction with the ontology designer it is not clear whether this should in fact be allowed as an intended model. 4. Finding the Right Models In each of the ontologies discussed in the preceding section, we noted the role that the on- tology user plays in identifying which models are unintended and which intended models are omitted. We now consider procedures that can be used to support the validation of an ontology as a dialogue between the ontology curator and the ontology user/designer. At the heart of any such procedure is the identification of unintended and omitted models, followed by decisions about how to modify the ontology in light of the existence of any such models. For example, with an early version of Tboxworld , a proof could not be found for the competency question stating that an edge cannot meet another edge at two distinct points: (∀e1 , e2 , e3 , p1 , p2 )meet(e1 , e2 , p1 ) ∧ meet(e1 , e3 , p2 ) ∧¬(p1 = p2 ) ⊃ ¬(e2 = e3 ) In this case, no proof existed because there existed a model of the axioms that did not satisfy this sentence, that is, there existed a surface with a hole consisting of only two edges. But is this model indeed unintended? If so, we need to extend the axioms. If not, then we need to relax the specification of the class of intended models. On the other hand, intended models of an ontology are omitted if the axioms of the ontology are not satisfied by the intended models, that is, the ontology is too strong. In this case, a proof can be found for a sentence that contradicts the intended semantics of the ontology. Given this possibility, a thorough inspection of all proofs found must be performed; if this case is detected, it is indicative of at least one of two possible errors with the ontology. First, an examination of the proof may lead to the identification of some axiom in the ontology which is not entailed by the intended models, and the prob- lem can be resolved by removing the axiom. A second possible error arises when exam- ination of the proof leads to the detection of some error in the definition of the require- ments, that is, in the specification of the intended models. It is important to devote con- siderable attention to the detection of this possibility so that the ontology is not revised to satisfy incorrect requirements. For example, the following sentence was entailed from an early version of Tboxworld : Every edge meets at most two distinct edges. Upon inspection, however, it was discov- ered this was actually a proof of: Tboxworld |= (¬∃p)point(p) Examination of the proof showed that the axiom: (∀e, p1 , p2 , p3 )edge(e) ∧ point(p1 ) ∧ point(p2 ) ∧ point(p3 ) ∧ part(p1 , e) ∧part(p2 , e) ∧ part(p3 , e) ⊃ (p1 = p3 ) ∨ (p2 = p3 ) was incorrect, and needed to be weakened. We will refer to this as the existence of an unintended proof, since it is not a sentence that should be provable from the ontology. It is interesting to see the relationship between this case and the failure of verifi- cation for the ontology. Part of the methodology for verification shows that a sentence that is entailed by axioms is also entailed by the set of intended models. Hidden conse- quences such as the above are counterexamples to this part of the verification, since it is a sentence that is provable from the axioms, yet it is not entailed by the intended models. One can either weaken the axioms (so that the sentence is no longer provable), or one can strengthen the requirements by restricting the class of intended models (so that the sentence is entailed by all intended models). 4.1. Hashemi Procedure [9] proposed an interactive procedure for using an ontology repository to find the axiom- atization of an ontology. The Hashemi Procedure finds the best match between a theory in a given ontology repository and the set of intended and unintended models as iden- tified by an ontology designer. Since the class of intended models Mintended is not al- ways explicitly specified, the system elicits a subset N from the user. It is not enough to jump from N to a theoryT . Further interaction is required, in which the system provides models of existing ontologies and the user identifies them as either intended or not. The Hashemi Procedure presumes that there is an existing set of axiomatized theo- ries with the same signature (known as a hierarchy in [10]): Definition 1. A hierarchy H = hH , ≤i is a partially ordered, finite set of theories H = T1 , ..., Tn such that 1. Σ(Ti ) = Σ(T j ), for all i, j; 2. T1 ≤ T2 iff T2 is an extension of T1 ; 3. T1 < T2 iff T2 is a non-conservative extension of T1 . The Procedure consists of two parts – elicitation of user models and the proposal of models for existing ontologies. The first component locates the user somewhere in the hierarchy, providing “bounds” for theories which characterize the user’s intended models. In the second part, models of existing ontologies, coupled with user responses, tighten this bound, resulting in selecting the strongest (if any) theories from the hierarchy which capture the user’s intuition. 4.2. The Dialogue of Validation The Hashemi Procedure was actually motivated by the problem of ontology design rather than ontology verification and validation. It was assumed that the user knows the class of intended models but does not know how to axiomatize them. In the current paper, we are considering a different problem – we have the axioms of the ontology, but we are unsure whether or not the models of the axioms are equivalent to the intended models, and we require interaction with the user to validate the ontology. We start with a verified ontology T and crawl through the hierarchy by generating unintended proofs and unintended models. The first InsertT heory Procedure adds T to the hierarchy; this is a modification of the FindT heory Procedure introduced by [10]. Beginning with the root theory in a core hierarchy C, the procedure searches2 through C to find the maximal theories that are interpretable by T . If there are multiple maxi- mal theories, the procedure returns the union of their sets of axioms. The result com- pletely specifies which theories in the hierarchy are weaker than T and which theories are stronger than T . Within the EliminateUnintende Procedure, the user distinguishes intended and un- intended models of T that are generated from the ontology 3 Once an unintended model has been identified, we find the weakest extension of T that eliminate these models. Since extending T might lead to a theory that is too strong and omits models, the WeakenProo f Procedure allows the user to select which axioms to eliminate from potential unintended proofs generated from the ontology. This dialogue with the user, through alternating requests for unintended models and unintended proofs, leads to a theory whose models is the closest approximation to the class of intended models. Definition 2. A near-miss for a class of intended structures Mintended in a hierarchy H is a theory T miss that has no omitted models with respect to Mintended , and all extensions of T miss in H have either unintended models or omitted models. 2 We assume the existence of three other algorithms related to partial orderings. The first is ChainDecomp(P) which outputs the set of chains for a poset P, and the second is PosetSort(X, P), which constructs a poset P from an unordered set X. The third algorithm is NextT heory(T, P) which returns the elements in the poset P that covers the element T . 3 In the procedures introduced in this section, we restrict our attention to theories that have finite models, a property that holds for all of the case study ontologies considered in Section 3. Procedure 1 InsertT heory(H, T, H0 ) Require: Hierarchy H = hT , vi, theory T 6∈ T . Ensure: Hierarchy H0 = hT ∪ {T }, vi. Chainsi ← ChainDecomp(Ci ) Collecti ← 0/ for all Gi j ∈ Chainsi do Candidatei j ← 0/ 5: Tcurrent ← minimal theory in Gi j Tmax ← maximal theory in Gi j while Tcurrent 6= Tmax do if T ∪ ∆i |= Tcurrent and T ∪ ∆i is a conservative extension of Tcurrent then Candidatei j ← Tcurrent 10: Tcurrent ← NextT heory(Gi j , Tcurrent ) else Tcurrent ← Tmax end if end while 15: end for Collecti ← j {Candidatei j } S PosetSort(Collecti , P) Ti ← set of axioms in the union of maximal theories in P T ← T ∪ {Ti } Procedure 2 EliminateUnintended(T, H, T 0 ) Require: Theory T , Hierarchy H = hT , vi. Ensure: Theory T 0 with no unintended models. Generate M ⊆ Mod(T ) User selects subset N ⊆ M of unintended models. T 0 ← weakest extension of T in H such that N ∩ Mod(T 0 ) = 0/ Procedure 3 WeakenProo f (T, H, T 0 ) Require: Theory T , Hierarchy H = hT , vi. Ensure: Theory T 0 with no omitted models. Θ(T ) ← {θ : θ ∈ S < T such that θ is not an axiom in T } for all θ ∈ Θ(T ) do Generate proof of θ User selects subset Σ ⊂ T of sentences that should be eliminated 5: EliminateUnintended(T \ Σ, T 0 ) if T 0 < T then WeakenProo f (T 0 , H, T ∗ ) end if end for Procedure 4 Validate(T, H, T ∗ ) Require: Theory T , Hierarchy H = hT , vi. Ensure: Near-miss theory T 0 . InsertT heory(H, T, H0 ) EliminateUnintended(T, H, T 0 ) WeakenProo f (T, H0 , T ∗ ) It is easy to see from this definition that a near miss with no unintended models has the property that Mod(T miss ) is equivalent to Mintended . Theorem 1. Given a theory T and hierarchy H, if the Validate(T, T ∗ ) Procedure termi- nates, then T ∗ is a near-miss theory for the class of intended structures provided by the user. 5. Summary We have presented a procedure which incorporates interactions with an ontology user to arrive at an ontology whose models are the closest approximation to the class of intended models. The resulting ontology can be considered to be validated with respect to the user’s selections of unintended and omitted models. One limitation with the Procedure is that we can only guarantee a near-miss theory as the output, since it can only add or remove axioms that already appear within some other theory in the same hierarchy. In general, we must be able to weaken an axiom rather than remove axioms (as illustrated by the example in Section 4). A major challenge in the implementation of the validation procedures is the gen- eration of models for the user to select. In the case of the BoxWorld Ontology, Mace4 was able to construct models of the CardWorld and BoxWorld axioms that correspond to the common shapes. Unfortunately, Mace4 has been inadequate for exploring the set of all models of the CardWorld and BoxWorld Ontologies, in the search for potentially unintended models. Even if we restrict our attention to small domains (e.g. a box with five surfaces, twelve edges, and eight vertices), Mace4 is unable to find models. We will be pursuing the use of other model constructors such as Paradox to see whether they are able to construct models on different domains. References [1] Megan Katsumi and Michael Gruninger. Theorem Proving in the Ontology Lifecycle. In Knowledge Engineering and Ontology Design (KEOD 2010), pages 74–86, 2010. [2] Nicola Guarino, Daniel Oberle, and Steffen Staab. What is an Ontology?, pages 1–17. Springer-Verlag, Berlin, 2 edition, 2009. [3] Michael Grüninger. The ontological stance for a manufacturing scenario. Journal of Cases in Informa- tion Systems, 11:1–25, 2009. [4] C. Chui and M. Gruninger. A molecular structure ontology for medicinal chemistry. In Proc. of the 10th Int. Conference on Formal Ontologies in Information Systems (FOIS2016), pages 317–330. IOS Press, 2016. [5] M. Gruninger and S. Bouafoud. Thinking outside (and inside) the box. In Proceedings of SHAPES 1.0: The Shape of Things. Workshop at CONTEXT-11, volume 812. CEUR-WS, 2011. [6] Carmen Chui and Michael Grüninger. Mathematical Foundations for Participation Ontologies. In For- mal Ontology in Information Systems - Proceedings of the Eighth International Conference, FOIS 2014, September, 22-25, 2014, Rio de Janeiro, Brazil, pages 105–118, 2014. [7] C. Chui and M. Grüninger. Verification and modularization of the dolce upper ontology. In FOUST: The Foundational Stance, Joint Ontology Workshop 2017, Bolzano, Italy, 2017. [8] Lydia Silva Muñoz and Michael Grüninger. Mapping and verification of the time ontology in SUMO. In Formal Ontology in Information Systems - Proceedings of the 9th International Conference, FOIS 2016, Annecy, France, July 6-9, 2016, pages 109–122, 2016. [9] Ali B. Hashemi and Michael Grüninger. Ontology design through modular repositories. In KEOD, 2009. [10] Michael Grüninger, Torsten Hahmann, Ali Hashemi, Darren Ong, and Atalay Özgövde. Modular first- order ontologies via repositories. Applied Ontology, 7(2):169–209, 2012.