A Logical–Algebraic Approach to Revising Formal Ontologies: Application in Mereotopology

Citation: Aranda-Corral, G.A.; Borrego-Díaz, J.; Chávez-González, A.M.; Gulayeva, N.M. A Logical–Algebraic Approach to Revising Formal Ontologies: Application in Mereotopology. AI 2024,5, 746–789. https://doi.org/ 10.3390/ai5020039 Academic Editor: Miguel Molina-Solana Received: 1 March 2024 Revised: 4 April 2024 Accepted: 26 April 2024 Published: 29 May 2024 Copyright: © 2024 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (https:// creativecommons.org/licenses/by/ 4.0/). Article A Logical–Algebraic Approach to Revising Formal Ontologies: Application in Mereotopology Gonzalo A. Aranda-Corral 1, Joaquín Borrego-Díaz 2,* , Antonia M. Chávez-González 2 and Nataliya M. Gulayeva 2,3 1Departamento de Tecnologías de la Información Escuela Técnica Superior de Ingeniería, Universidad de Huelva, Crta, Palos de La Frontera s/n, 21819 Huelva, Spain; [email protected] 2 Departamento de Ciencias de la Computación e Inteligencia Artificial, Universidad de Sevilla E.T.S. Ingeniería Informática, Avda. Reina Mercedes s/n, 41012 Sevilla, Spain; [email protected] (A.M.C.-G.) 3Department of Informatics, Faculty of Informatics, National University of Kyiv-Mohyla Academy, 2 Skovorody vul., 04070 Kyiv, Ukraine *Correspondence: jborr[email protected] Abstract: In ontology engineering, reusing (or extending) ontologies poses a significant challenge, requiring revising their ontological commitments and ensuring accurate representation and coherent reasoning. This study aims to address two main objectives. Firstly, it seeks to develop a methodological approach supporting ontology extension practices. Secondly, it aims to demonstrate its feasibility by applying the approach to the case of extending qualitative spatial reasoning (QSR) theories. Key questions involve effectively interpreting spatial extensions while maintaining consistency. The framework systematically analyzes extensions of formal ontologies, providing a reconstruction of a qualitative calculus. Reconstructed qualitative calculus demonstrates improved interpretative capabilities and reasoning accuracy. The research underscores the importance of methodological approaches when extending formal ontologies, with spatial interpretation serving as a valuable case study. Keywords: foundational ontologies; automated reasoning; qualitative spatial reasoning 1. Introduction Contemporary practices in artificial intelligence (AI) research have emphasized the significance of ontologies in formally representing knowledge within specific domains or scopes. According to Gruber [ 1 ], an ontology serves as an explicit specification of a conceptualization, outlining the concepts, entities, and relationships inherent in a knowledge domain. Ontologies encode the formal structure of existence (formal ontologies) and categorize what exists in a domain (material or domain ontologies), connecting scientific disciplines by making their assumptions and commitments explicit. The proliferation of ontological research, sometimes called the “Ontological Turn”, demonstrates the growing recognition of the importance of formalizing knowledge [ 2 ]. In a more applied context, viewing ontologies as the ideal references for accuracy in data science (e.g., in knowledge graphs) makes their creation, usage, and maintenance essential tasks for the robustness of results and their explainability. In computer science, a formal ontology represents a precise and rigorous mathematical– logical framework for collectively understood concepts, presented in a format comprehensible and processable by computers [ 3 ]. Achieving such conceptualization requires designing formal definitions for the vocabulary, expressed through axioms and rules. This facilitates the exact definition, constraint, and interrelation of concepts, thereby eliminating potential confusion or ambiguity. Various formalisms can be utilized to represent a formal ontology, including firstorder logic (FOL), higher-order logic, description logic (DL), or RDF, among others. The AI 2024,5, 746–789. https://doi.org/10.3390/ai5020039 https://www.mdpi.com/journal/ai AI 2024,5747 choice of formalism is determined not only by representational considerations, such as expressiveness, but also by the need to support automated reasoning, ensure conceptual consistency, infer new knowledge, and facilitate general computational analysis, among other practical considerations. However, effectively leveraging ontologies is faced with challenges. As discussed by Gomez et al. [ 4 ], ontologies must strike a balance between the complexity of formal representation and the reasoning capabilities they afford. Overly simplistic ontologies may fail to capture the nuances of complex domains, limiting inferential capabilities, while excessively complex ontologies can impede efficient computational reasoning. Ongoing research aims to develop techniques for constructing ontologies at an appropriate level of complexity, supporting robust knowledge representation and reasoning (KRR) paradigms. In addressing this challenge, a thorough analysis of the logical representation language is essential [5]. Ontology engineering (OE) involves several stages that range from project conceptualization to ontology maintenance and documentation. The two initial extraction-based steps focus on requirement specification and conceptualization of the domain. In the conceptualization stage, relevant domain concepts and relations are identified to represent the informal conceptual model. The next two stages focus on formalizing the conceptualization, both from a logical perspective (e.g., with description logic) and in terms of implementation (e.g., with OWL), enabling web standard representation as well as reasoning engines. Lastly, other activities are necessary to enhance the quality and usability of the ontology. The first of these is the evaluation stage, which involves assessing the correctness, completeness, and conciseness of the implemented ontology relative to the requirements. The last stage centers around documentation and maintenance activities, which include documenting design decisions and keeping the ontology up to date in evolving domains via planned revisions and extensions, preserving backward compatibility when possible. This paper is focused on the foundational aspects associated with the aforementioned process, particularly concentrating on the critical maintenance task, which can involve revising concepts and relationships when there are changes in the domain, particularly for ontology reuse, with a primary focus on foundational or formal ontologies. Foundational ontologies are pivotal in KRR and reuse because they contribute to the creation of shareable and reusable domain ontologies [ 6 ]. A persistent challenge in OE is the need for a comprehensive analysis of the relationship between foundational and domain ontologies. The OE process outlined in the introduction poses several logical challenges, many of which can be effectively addressed through the adoption of a robust methodology. A notable approach to (formal) ontology design is the “definitional methodology” proposed by Bennett [ 7 ]. This approach is rooted in the recognition that definitions play a central role in ontology construction. The idea is to begin by establishing a small set of primitive concepts with precisely defined model-theoretic semantics upon which other concepts and relationships are built. Definability theorems are then introduced to identify concepts that can be defined in terms of others. The expressive power of definitions, the importance of primitives, and the comprehension of definability are all factors that contribute to the resilience of ontologies when constructing extensive ontological vocabularies. Despite its advantages, the definitional strategy may be perceived as overly rigid due to stringent requirements such as categoricity, where any two models of ontology are equivalent in a certain sense. In reality, the characterization of classes and relations in the “intended models” could be more crucial than in the general FOL class of models to which logical categoricity refers. An illustrative case study can be found in QSR ontologies, where a recognized class of real spatial models represents the target of KRR practices. While such models may not be logically characterized without considerable complexity, in practice, an affordable approach that ensures essential features may be considered sufficient. Research has demonstrated the value of developing and reusing ontologies that formalize general concepts across domains. There is a great deal of well-founded explicit AI 2024,5748 knowledge formalizing general notions (such as time concepts and the part-of relation) [ 8 ]. However, it is often the case that instead of reusing existing ontologies, engineers create custom procedural programs that implicitly encode such knowledge. This practice results in duplicated effort and lost opportunities to leverage prior work. The creation of formal ontologies represents a substantial investment of time and skill to form standardized, logic-based conceptual systems. As a result, enabling ontology reuse across different applications has become a key priority within knowledge engineering fields. Effective ontology reuse offers many potential benefits, including reducing redundant modeling work, promoting consistency across projects, and improving semantic interoperability for knowledge transfer. As ontologies are reused in new contexts, it often becomes necessary to re-examine ontological commitments made in the original ontology development. Such commitments may include the definitions of classes, the relationships between them, and the properties of those classes. In some cases, the new application environment may require modifications or extensions to the ontology to represent the concepts and relationships in the domain accurately. Several factors can motivate such ontological revisions instead of simple ontology reuse, including the following: • Emergence of new entity types or activities in the domain not currently modeled in the ontology; • Changes in assumed relationships between existing domain concepts; • Novel user requirements and use cases not originally envisioned; • Inaccuracies in the original conceptual model exposed during ontology deployment. When revising an ontology, it is crucial to ensure compatibility with existing models by properly interpreting changes. This becomes particularly critical when existing definitions require modification. For instance, when introducing new concepts or relationships that expand the ontology, it is advisable to provide theoretical justification connecting these additions to the original theory. This approach allows for the reconsideration of the class of representative models from the source theory (i.e., the “intended models” that the engineer aims to represent) to incorporate the new ontology elements in a principled manner. Overall, ontology revisions should strike a balance between innovation and continuity, achieved through sound theoretical grounding and methodical integration with existing elements. Despite the aforementioned desiderata, it is common for some of new ontology components to be undefinable or only partially characterized based on the elements of the source ontology. Consequently, the definitional methodology may not be suitable in such cases. Alternative approaches are needed to effectively capture the relationships between the existing and newly introduced elements, ensuring the coherence and integrity of the revised ontology. This underscores the importance of a systematic and carefully planned expansion strategy when modifying ontologies, ensuring the ongoing relevance and applicability of the underlying conceptual framework. 1.1. From Ontologies to Relation Calculus In advocating for ontology-building methodologies, computational solutions derived from the ontology characterize relationships and concepts. This facet plays a pivotal role in guaranteeing the resilience of the associated computation [ 9 ] (e.g., spatial reasoning). By ensuring that the definitions within the ontology effectively capture the intricacies of relationships and concepts, the qualitative computation derived from such formalism becomes a reliable foundation. This not only strengthens the computational aspects of the ontology but also establishes a solid ground for employing spatial theory in the development and reasoning processes. Analyzing the computational complexity of reasoning problems in the (revised) ontology is an important research direction. As Lutz et al. [ 10 ] demonstrate, model–theoretical techniques can be used to study the complexity of constraint satisfaction problems (CSP). Such techniques can provide valuable insights into the scalability of ontology-based systems. AI 2024,5749 In the field of AI, qualitative calculus serves as a specific type of mathematical formalism crafted to represent and reason about relations and properties in a qualitative, rather than quantitative, manner. This formalism centers on qualitative properties, relations, and changes within the objects or processes under study, utilizing a finite set of symbols or qualitative values to encode these properties and relations. Furthermore, qualitative calculus provides operators designed to combine qualitative values into meaningful expressions. For instance, it facilitates the composition of spatial relations and includes inference rules to derive new qualitative knowledge from established facts. Additionally, certain calculi permit the qualitative simulation and analysis of how values change over time, enhancing their utility in understanding dynamic systems and temporal aspects. As Gruter points out, these characteristics make qualitative calculi a valuable tool for AI applications, offering a natural and effective approach to handling qualitative aspects of KRR [9]. According to [ 11 ], the paradigm of algebraic constraint-based reasoning, embodied in the notion of a qualitative calculus, has been studied within two frameworks. One framework defines qualitative calculus as “a non-associative relation algebra (NA) with a qualitative representation”, while the other defines it as “an algebra generated by Jointly Exhaustive and Pairwise Disjoint (JEPD) relations”. These frameworks provide complementary perspectives. The divergence of definitions creates confusion around the notion of a qualitative calculus and revisits the “what” question (cf. [12]). Emerging from Allen’s examination of temporal relations, the concept of a composition table (CT) has evolved into a crucial technique, offering an efficient inference mechanism for a broad spectrum of theories [ 13 ]. In Allen’s interval algebra (IA), reasoning is manageable only for specific subalgebras and is executed through path consistency, a constraint propagation algorithm. Its rule-based implementation necessitates O(n2)rules for a subalgebra with n relations [14]. The work in [ 13 ] focuses on the challenge of providing comprehensive characterization of the class of theories and relational constraint languages. It investigates situations in which a complete proof procedure can be specified by a CT, shedding light on the potential and limitations of this approach. Likewise, in order to optimize the calculus, redundancy checking is a crucial task [15]. Formally, in the context of a theory T wherein Rels is a JEPD set of defined base relations, the composition of two of them is entailed by T . That is, given R , S∈Rels , the problem consists of determining the smallest subset {Ri}⊆Rels such that T|=∀x∀y∀z[R(x,y)∧S(y,z)→(R1(x,z)∨ · · · ∨ Rn(x,z))]. In semantic terms, this definition ensures that whenever R(a , b) and S(b , c) hold in M a model of T, some i Rimust exist such that aand care related. One of the primary challenges in qualitative spatial reasoning (QSR) revolves around integrating or expanding existing theories to incorporate new aspects within the same formalism while ensuring the existence of a sound calculus [ 16 , 17 ]. Even when a qualitative calculus is derived from a formal ontology, a common practice in ontology reuse involves reconsidering ontological commitments that would affect the calculus. For instance, in QSR, the dilemma between crisp and fuzzy spatial sets is often reevaluated. Addressing such issues requires taking various features and perspectives into account. On the one hand, there is a desire to maintain the characteristics of existing objects; on the other hand, there is a necessity to reassess some definitions and the associated qualitative calculus. This balance underscores the need to relax the definitional methodology, requiring only certain axioms and properties of the definitions to exhibit categoricity (i.e., common to all intended models). Lastly, it is worth noting that qualitative calculus-based techniques have applications beyond foundational studies. For example, in [ 14 ], a practical approach to rule-based temporal reasoning over RDF/OWL using Allen’s interval algebra (IA) is outlined, showcasing the versatility of the methodology. This example provides an idea of both the utility of hav- AI 2024,5750 ing foundational ontologies and the need to adapt these ontologies to different applications through revision to a greater or lesser extent. 1.2. Formalization for Qualitative Spatial Representation and Reasoning Representation and reasoning with qualitative spatial relations constitute an important problem in AI, with wide-ranging applications in fields such as geographic information systems, computer vision, autonomous robot navigation, natural language understanding, spatial databases, and image mining [ 18 ]. One of the necessary elements (though not necessarily sufficient) for the effectiveness of a QSR proposal (e.g., for prediction) is the availability of a reasonably high-quality theory, especially when complete information is available and the range of scales involved, both temporal and spatial, is not extreme. When these conditions are not met, simulation becomes less effective or entirely inappropriate. In [ 19 ], an insightful discussion on twelve features of physical reasoning problems that present challenges for simulation-based reasoning is developed. The paper also surveys alternative techniques for physical reasoning that do not rely on simulation. Mereotopology is a field in logic and ontology concerned with parts, wholes, and connections. The term ‘mereotopology’ combines ‘mereology’ (the study of part-whole relations) and ‘topology’ (the study of connections and boundaries without considering the form). Mereotopology aims to provide a formal framework for describing concepts such as parts, wholes, boundaries, contact, and connection. It builds upon mereology by incorporating topological notions such as closure and neighborhood into the theory of parts and wholes. This expansion allows for a richer characterization of concepts that involve both parthood and connection relations. The importance of mereotopology in qualitative spatial and temporal reasoning (QSTR) cannot be overstated. Serving as an alternative to set theory and Euclidean geometry, mereotopology finds applications across diverse fields beyond spatial and temporal reasoning (e.g., [20]). The ongoing debate surrounding the point versus object dilemma persists in various manifestations. Mereotopologies, as point-free methodologies, offer an alternative for modeling information while sidestepping certain perplexing assumptions inherent in set– theoretical systems. The essence of point-free approaches lies in introducing points into mereology or mereotopology only when their existence is unequivocally justified. The task of constructing spatial ontologies is not without representational challenges, especially when dealing with diverse ontological entities such as bodies, space, and situated objects. An illustration of this is [ 21 ], where the exploration of location ontologies is grounded in mereotopological pluralism. Regarding language design itself, the scope encompasses both time and space, as well as the structural properties of objects, adopting a way of considering the structure of space and the entities that inhabit it. This design should draw inspiration from robust classifications and specifications. The need for a sound language for representation is intrinsic to any ontology with a remarkable level of abstraction. For instance, in [ 22 ], a taxonomy of part types is proposed based on the manner of attachment of a part to its parent whole, its degree of dependence on that whole, or external factors. As another example, in [ 23 ], a novel approach to qualitative shape recognition and matching in design is introduced. The method employs an ordering information approach for the qualitative description of shapes, considering features such as angles, relative side lengths, concavities, convexities of the boundary, and color. The design challenge in the case of ontologies for mereotopology involves difficulties from both a logical and representational standpoint, as well as in OE. Nuances come into play that are challenging to represent or interpret appropriately. This situation can lead to major issues that affect the ontology’s design itself. In addressing these issues, the authors of [ 24 ] propose corrections and additions to the axiomatization of SUMO (https:// www.ontologyportal.org/ (accessed on 27 february 2024). Their work focuses on rectifying problems related to omitted and unintended models of classical mereology. Additionally, a AI 2024,5751 more recent study by Silva in [ 25 ] demonstrates that the existing axiomatization of SUMO fails to capture some of the intended models of classical mereology. The logical approach to QSTR becomes ubiquitous in situations where there is a desire to formalize, almost at the verification level, the relationships between information, space, and objects. In this context, an example could be the paper [ 26 ], where a spatiotemporal specification language resulting from the integration of temporal and spatial logic is introduced. Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies rooted in logical methods for topological spaces, as seen in [27] in biomedicine. Continuing in the field of biomedicine, the development of biomedical ontologies necessitates a meticulous formal analysis of foundational relations, utilizing various formal tools in the process. Ideally, an analysis in a highly expressive language, like FOL, should be complemented by analyses in less expressive but computationally tractable deductive systems, such as description logics [28]. In the context of biomedical ontologies, the qualitative and time-dependent nature of spatial relations is highlighted in [ 29 ]. The motivation stems from the relatively wellunderstood formal representation of mereological aspects, specifically parthood relations, in canonical anatomy. However, other aspects, including connectedness and adjacency relations between anatomical parts, their shape and size, as well as the spatial arrangement within larger anatomical structures, are less comprehensively represented in existing computational, anatomical, and biomedical ontologies. The paper [ 30 ] also illustrates the utility of a formal spatial theory in clarifying spatial information within biomedical ontologies and enhancing their automated reasoning capabilities. In the field of image mining, as presented in [ 18 ], the authors introduce an innovative framework for robot vision based on concept lattice theory and cloud model theory. The concept lattice serves as a representation of the human conceptualization process using mathematical formal language, while the cloud model provides a transformation model between qualitative concepts and quantitative numerical values. Notably, the authors contend that the problem at hand possesses a rough nature, implying a certain degree of indistinctness in the relationships addressed. Alongside the logical dimension, computational considerations are crucial. Spatial– temporal reasoning can benefit from various tools derived from computational logic. For instance, in [ 31 ], the authors propose an approach to trajectory calculus that can be implemented using answer set programming (ASP). ASP is also valuable for designing a formal framework for representing and reasoning about cardinal directions between extended spatial objects on a plane, as demonstrated in [32]. The QSR team at the University of Leeds pioneered the development of several logical calculi designed for the representation and analysis of QSR on regions, with a particular focus on the so-called Region Connection Calculus (RCC) (see Section 5below and [ 17 , 33 ]). RCC has proven useful across several AI domains such as GIS. As articulated in [ 34 ], their motivation lies in utilizing regions as the fundamental spatial entity and showcasing how a rich language can be constructed using few primitives. In the case of RCC, this begins with the concept of connection. The reasoning within RCC encompasses both static and dynamic aspects, providing a comprehensive framework for QSR. Although RCC serves as a notable example of a mereotopological system, some discussion on its semantic nature is necessary [35]. Certainly, alternative approaches to RCC exist, deviating from the definitional strategy inherent in the RCC axiom system. In [ 36 ], the relations of contact, nontangential inclusion, and dual contact are treated as non-definable primitives. This extends the language of distributive contact lattices significantly. Part of the paper focuses on appropriately axiomatizing the new language termed Extended Distributive Contact Lattice (EDC-lattice) using universal first-order axioms that hold in all contact algebras. EDC-lattices can also be regarded as an algebraic tool for a specific subarea of mereotopology [ 37 ]. Ref. [ 38 ] provides an overview of research examining the cognitive validity of qualitative spatial AI 2024,5752 calculi, with a focus on the RCC and Egenhofer’s intersection models (IM), in which both topological theories are frequently claimed to align with human spatial cognition and extensions. 1.3. On the Use of Automated Reasoning Systems in Ontology Engineering Automated reasoning systems (ARS) provide tools to contrast hypotheses, specifications, and axioms. Results obtained by automated theorem provers (ATPs) ensure the correctness of certain ontological reusing practices. This allows verification of the logical validity of extensions or transformations without relying on unspecified intuitive properties or hidden ontological commitments [ 39 ]. In QSR, using an ATP to establish properties ensures that only the knowledge expressed in the axioms is utilized, avoiding reliance on spatial intuitions not formalized in the theory. In this paper, ATP Prover9 (https://www.cs.unm.edu/~mccune/prover9/ (accessed on 27 February 2024)) and model finder Mace4 (https://www.mcs.anl.gov/research/ projects/AR/mace4/ (accessed on 27 February 2024)) are utilized to support findings in our work. Prover9 is software for automated first-order logic theorem proving, employing resolution and paramodulation inference. Key features include equality reasoning, customizable search strategies, proof output in natural deduction format, and stand-alone proof checking. Complementing Prover9, the Mace4 system searches for finite models satisfying input statements and their negations. It clarifies axiomatic systems by testing conjectures and revealing counterexamples, further aiding Prover9 proof construction. Together, these tools enable robust development, testing, and formal proof of mathematical conjectures. Their versatility supports applications in mathematics, computer science, and AI research. In this paper, both systems are actively utilized in proofs. 1.4. Aim and Contributions of the Paper Ontology reuse remains a challenge for the ontology community [ 40 ]. The lack of a consensus on this notion poses a barrier in OE. Without understanding what constitutes reuse, it is difficult to perform or assist in ontology design for reuse. The aim of this paper is to address the issue. More concretely, the main contributions of this paper are the following: • A proposal for the formal definition of ontology reusability (Section 6), which includes extension and revision as tasks. • Beyond clarifying these concepts, the paper proposes a methodology for formal ontology reuse (Section 6.3). It characterizes reuse operations that can guide reuse to meet specified requirements. This not only directs the reuse task but also assesses the implications of reusing an ontology. • As an illustrative case, the paper tackles a second aim: the problem of obtaining a sound interpretation (by conferring spatial meaning) to the extensions of RCC obtained-according to the methodology-by inserting an “undefined” relationship (Section 7). • The application case of the methodology establishes the mereological paradigm in 3WD, providing a formal framework that encompasses various possibilities of representing 3WD mereological relations (as used, for example, in [41]). In a broad scope, the aim is to describe how the rudiments of first-order model theory (and computational logic) can be used to increase knowledge on generic extensions of the theory. This paper substantially extends a previous contribution [42]. 1.5. Structure of the Paper The next section provides a description of state-of-the-art work related to this paper, referring to the specific representational challenges of spatial KRR. Section 3offers a brief summary of the basic ideas of the three-way decision paradigm and provides some notes AI 2024,5753 on three-way mereo(topo)logy. Section 4contains some examples motivating ontology revision, covering spatial notions in socio-geodemographic systems, spatial interpretation for ontology reasoning, and extending the formalism of description logic. Section 5presents background information on the mereotopological theory RCC required for the development of the paper. The subsequent sections represent the formal instantiation of the ideas outlined earlier. Both contain the main contributions of the paper. Section 6is dedicated to presenting a type of ontological extension with a certain degree of categoricity and defining the methodology for ontology extension and revision. As the second main contribution of the paper, this methodology is then applied in Section 7to RCC. Section 8is devoted to comparing the results obtained with our methodology with other different ontological redesigns, such as the “egg-yolk” approach. In Section 9, some conclusions, a discussion on the strengths and weaknesses of our proposal, and some ideas for future work are presented. 2. Related Work Given that the paper has a dual objective (on the one hand, formalizing a concept of extension + ontology revision; on the other hand, its application to a case of RCC extension), we will proceed to dissect and examine the related existing literature in both scenarios. 2.1. Commonsense versus Formal Ontologies in Spatial Representation Contrary to the apparent anticipation that constructions for QSR should have wellestablished “standard formalizations”, the reality is quite different. This is due to the fact that the representation and reasoning involving spatially or temporally extended objects are intentionally crafted to mirror diverse ontological commitments, consistently considering their computational reasoning counterparts in AI. An exemplar of this approach is highlighted in [ 43 ], where an alternative perspective of mereological pluralism is presented. In such a framework, each mereological relation corresponds to a distinct characteristic of the solid physical object, and these characteristics are formalized in different modules within an upper ontology. Ref. [ 44 ] serves as an example of these diverse commitments, presenting a mereotopological theory of time that effectively discriminates between various temporal topologies. From the cognitive and commonsense realms, in the paper [ 45 ], the author contends that children approach spatial term learning with a pre-existing conceptual differentiation between core and non-core concepts of containment and support. The learning process involves understanding how language aligns with this conceptual distinction, considering both the simple prepositions and their associations with specific verbs and the distributions of their co-occurrences. Another illustration of this diversity in representation and its strong connection to commonsense knowledge and ontological commitments is found in [ 46 ]. That work conducts a comprehensive study of parthood and part-whole relations in the Zulu language and culture. The paper underscores the dependency on whether there are ontological differences, potentially implying that the ’common’ list is not universal across languages and cultures. This raises new questions for OE on how to manage the plurality of relations and for philosophy to possibly extend mereology. All of the above examples demonstrate the ongoing need to reassess the ontological commitments upon which a QSR approach is based in order to function effectively in diverse environments. If one chooses to adapt an existing ontology, even one considered standard, it may require the aforementioned reconsiderations. The realm of QSTR revolves around the symbolic representation of knowledge, primarily across infinite domains. The utilization of QSTR techniques is driven by the desire to harness computational properties that enable efficient reasoning and the integration of human cognitive concepts into a computational framework [33]. Similarly, a crucial aspect contributing to the success of QSR is the translation of many problems into constraint satisfaction problems (CSPs), especially in the qualitative context, AI 2024,5754 as emphasized in [ 10 ]. For example, the expansion of qualitative CSPs to include the ability to restrict selected variables to finite sets of possible values has been recognized as a promising research direction with substantial applications [47]. The roadmap for a formalization project of a QSR framework follows steps similar to those in the construction of formal ontologies: a representation language is introduced, its expressive power is analyzed, and finally, representation and reasoning mechanisms are designed, and their utility is evaluated. An example of such methodology is found, for example, in [ 48 ], where the author presents a logic-based formalism for formal reasoning about visual representations. After laying down foundational principles, a description logic is designed, offering decidable reasoning mechanisms well-suited for genuinely spatial domains, such as geographic information systems (GIS). This approach exemplifies how systematically following steps in QSR formalization can lead to effective and domainspecific solutions. However, there are ongoing challenges. In the realm of logic, computer science, cognitive science, and geographic information science, extensive studies have focused on mereotopological theories. However, the majority of these theories are unidimensional mereotopologies, restricting entities of only a single dimension to cost. To integrate mereotopological information with geometric data effectively, a multidimensional mereotopology is essential [49]. Spatial Vagueness and Indefinition Exploring the modeling of imprecise objects (or relations) with undetermined boundaries has become a focal point in fields such as GIS. An illustrative example is provided in [ 50 ], which discusses the characteristics of vague regions by examining them through the lens of the field/object dichotomy, recognizing that fields and objects offer distinct perspectives for modeling geographic phenomena. One of the goals of this paper is to exemplify how the strategy of introducing indefiniteness in spatial relations can be controlled and certified following the formal ideas developed in the paper. The use of such relations, which are not primarily specified in the axioms of classical formal QSR theory like the region connection calculus, is motivated by their potential application in AI systems. Alternatively, this could be approached using mereotopological relations with a certain level of indefiniteness. The need to work with relations beyond “crisp” ones is inherent to reasoning in several QSR frameworks. A natural option, in terms of model foundations, is to start with a new notion of topology, such as fuzzy topological spaces [ 51 ]. This framework, originating from the concept of a fuzzy set, provides a natural approach to generalizing many concepts of general topology to what might be called fuzzy topological spaces. In [ 52 ], the authors discuss rough inclusions defined in rough mereology, a paradigm for approximate reasoning introduced by Polkowski and Skowron. The paper suggests that rough inclusions can serve as a foundation for common models for both rough and fuzzy set theories, with the common motif being tolerance (or similarity). In [ 53 ], the authors propose a method for revealing spatial hierarchies among vague places extracted from geotagged user-generated data. The approach utilizes fuzzy formal concept analysis to represent each place as a concept with extent and intent. 2.2. Reasoning, Extending, and Reusing RCC In RCC-based relational calculus, two JEPD are used, RCC8 and RCC5 (Figure 1). Despite the initial presentation of RCC8 relations as defined in the axioms of the RCC, most implementations opt for working with the RCC8 Composition Table (RCC8-CT) instead. However, the replacement of a theory with calculus is not without issues. In [ 54 ], the foundation of RCC8-CT is investigated to discern the underlying mereotopological principles, highlighting the significance of this reasoning method for the theory. AI 2024,5761 Figure 4. Extension of the logic formalism of description logic ALC by typicality inclusions. 5. Formal Elements of the Mereotopological Theory RCC The application of the proposed ontology extension method will be illustrated grounded in RCC as the foundational theory (Section 6). In this section, we provide a more technical description of the key elements of this theory. Roughly speaking, RCC can be seen as the outcome of applying the definitional methodology to the primitive connection relation between two regions, denoted as C(.,.). Axioms asserting that this relation is reflexive and symmetrical are introduced. The intended models of RCC operate on connected regular regions from topological spaces. In the design of RCC, the intended interpretation of connection is the topological closures of the two connected regions intersect. The axiom set presented in Table 1expresses the remaining relations’ properties and definitions, which can be regarded as RCC’s set of axioms [ 17 ]. We denote by LRCC the first-order logic language used in these axioms. A key property of the set of RCC relations is that it possesses the mathematical structure of a lattice, derived from the partial order “provably subrelation of”. Figure 5illustrates the Hasse diagram of this lattice. Recall that the Hasse diagram of a partially ordered set is a directed graph constructed using the elements of the set as nodes, where the edges consist of all ordered pairs (x , y) such that x<y, and there exists no zsuch that x<z<y. Figure 5. The lattice of RCC spatial relationships. The index accompanying each relation will be utilized to reference it in first-order formulas when applying Mace4. AI 2024,5762 Table 1. Axioms of RCC: axioms stating that the connection is a reflexive and transitive relation, plus the definition-axioms for the other spatial relations. Axiom Relation Defined ∀xC(x,x) (Re f lexivity) ∀x[C(x,y)→C(y,x)] (symmetry) DC(x,y)↔ ¬C(x,y) (xis disconnected from y) P(x,y)↔ ∀z[C(z,x)→C(z,y)] (xis part of y) PP(x,y)↔P(x,y)∧ ¬P(y,x) (xis proper part of y) EQ(x,y)↔P(x,y)∧P(y,x) (xis identical with y) O(x,y)↔ ∃z[P(z,x)∧P(z,y)] (xoverlaps y) DR(x,y)↔ ¬O(x,y) (xis discrete from y) PO(x,y)↔O(x,y)∧ ¬P(x,y)∧ ¬P(y,x) (xpartially overlaps y) EC(x,y)↔C(x,y)∧ ¬O(x,y) (xis externally connected to y) TPP(x,y)↔PP(x,y)∧ ∃z[EC(z,x)∧EC(z,y)] (xis a tangential prop. part of y) NTPP(x,y)↔PP(x,y)∧ ¬∃z[EC(z,x)∧EC(z,y)] (xis a non-tang. prop. part of y) Definition 1. Let Ω be a topological space and T be a mereotopological theory. An interpretation on Ω is an interpretation of the language of T whose universe is the R(Ω) class of regular sets in Ω. T is interpretable on Ωif there exists an interpretation on Ω, which is model of T. The set of eight RCC binary relations shown in Figure 1is denoted as RCC8. These relations form a JEPD set. As a JEPD set, the set RCC8 is exploited as a calculus for constraint satisfaction problems (CSPs) (see [ 12 ]). Another useful calculus is based on the JEPD RCC 5 ={DR , PO , PP , PPi , EQ} . In short, the key difference between RCC8 and RCC5 is that the former enables enriching the knowledge representation by utilizing region frontiers, while the latter does not. Although empirical evidence has found that RCC8 better suits representing topological relations distinguished by humans than RCC5 [105], both are used here. 5.1. Relational Calculus in RCC Since RCC8 forms a JEPD set, we can define relation composition and study the relation calculus over RCC8 as described in Section 1.1. The composition table is shown in Table 2. For instance, the following fact is represented in the table: if region A is a proper part (PP) of region B , and region B is a proper part (PP) of region C , then by composition, we can infer that region A is a proper part (PP) of region C. The task of building the table involves analyzing how to compose relations. The exhaustive analysis of composition, reflected in Table 2, is provable from RCC (for example, using Prover9, it is possible to obtain formal proofs of each case). AI 2024,5763 Table 2. Composition table for RCC8. The “*” symbol corresponds to the complete RCC8. R2(b,c) R1(a,b)DC EC PO TPP NTPP TPPi NTPPi EQ DC *DC,EC PO,TPP NTPP(1) DC,EC PO,TPP NTPP(1) DC,EC, PO,TPP NTPP(1) DC,EC PO,TPP NTPP(1)DC DC DC EC DC,EC PO,TPPi NTPPi(2) DC,EC, PO,TPP, TPPi,EQ (3) DC,EC PO,TPP NTPP(1) EC,PO, TPP, NTPP, (4) PO,TPP NTPP(5) DC,EC (d DR)DC EC PO DC,EC PO,TPPi NTPPi(2) DC,EC, PO,TPPi NTPPi(2)*PO,TPP NTPP(5) PO,TPP NTPP(5) DC,EC PO,TPPi NTPPi(2) DC,EC PO,TPPi NTPPi(2)PO TPP DC DC,EC (d DR) DC,EC PO,TPP NTPP(1) TPP NPPP (f PP) NTPP DC,EC, PO,TPP TPPi,EQ (3) DC,EC PO,TPPi NTPPi(2)TPP NTPP DC DC DC,EC PO,TPP NTPP(1)NTPP NTPP DC,EC PO,TPP NTPP(1)*NTPP TPPi DC,EC PO,TPPi NTPPi(2) EC,PO, TPPi, NTPPi(7) PPPi, NTPPi (8) PO,EQ TPP TPPi(6) PO,TPP NTPP(5) TPPi NTPPi (g PPi) NTPPi TPPi NTPPi DC,EC, PO,TPPi NTPPi(2) TPPi PO NTPPi(8) TPPi PO, NTPPi(8) TPPi, PO, NTPPi(8) PO,TPPi TPP,NTPP NTPPi,EQ (b O) NTPPi NTPPi NTPPi EQ DC EC PO TPP NTPP TPPi NTPPi EQ 5.2. The Challenge of the Interpretability of RCC Extensions There are two types of extension to consider in OE: one involving a specific model (or class of models) while respecting the original ontology, and the other involving the redefinition of the model class in the ontology extension. This paper focuses on the latter. Regarding the first type, an example is demonstrated in [ 55 ], where it is shown how any consistent RCC8 binary constraint network (RCC8 network) can be consistently extended. This result ensures the transfer of tractability from a set of RCC8 relations to its closure under composition, intersection, and converse. In this way, we can enrich the mereotopological configuration of the regions under study with more regions. In reality, these types of extensions affect the population of the ontology (the new elements must be added while preserving consistency) and not the design of its axioms. The second type of extension is foundational in nature as it pertains to the theories that underpin the models. Therefore, the task could be more complex. If an abstract extension of a standard QSR theory is obtained, it is necessary to extend the standard interpretation to accommodate the new concepts/relationships as spatial regions/relations. This type would encompass revisions of mereological ontologies implicit in machine learning to accommodate new methods, such as 3WD clustering [ 41 , 77 , 80 ] commented on in Section 3. If, in the new theory, the elements of the initial theory can be considered objects of the universe, then it can be interpreted within the former. We formalize this idea below. Firstly, it is worth noting that the notion of interpretability between theories can be considered from different perspectives. For example, if our framework is OE, and we only want to use the knowledge represented in one theory in another target theory, it would suffice to find a syntactic translation mapping that operates on the axioms (e.g., [ 25 ]). In this case, we are not relativizing the information to a special type of objects and properties. Nevertheless, if we want to work with more complex interpretations that use the same language, we can resort to relativization. The relativization of a formula ψ(x) with respect to another φ(x) consists of restricting the property expressed by the former to those elements that satisfy the latter (in our case, the objects considered in the models of the former ontology). AI 2024,5764 Definition 2. Let φ(x)be a formula in a FOL language L. • The relativization with respect to φ(x) is an operator ·φ on L formulas defined by recursion as follows: –If p( x)is an atomic formula, p(x1, . . . , xn)φ≈V1≤i≤nφ(xi)→p(x1, . . . , xn); –(¬ψ)φ≈ ¬(ψφ); –(∃xψ(x))φ≈ ∃x(φ(x)∧ψ(x)φ); –(∀xψ(x))φ≈ ∀x(φ(x)→ψ(x)φ). •Theory T1is interpretable into theory T2if there exists a formula φsuch that for any ψ T1|=ψ⇐⇒ T2|=ψφ The idea is to use this type of interpretability to relativize any T extension of RCC to the regions considered in RCC. For example, a property ψ in a theory about spatial vagueness could be relativized to the special case of (crisp) regular regions, which must be characterized by such a formula φ. 6. Lattice Categorical Ontology Extensions From a certain perspective, ontologies could be viewed as qualitative theories aimed at representing the conceptualization of knowledge space. This standpoint includes the representation of class (concept) and relation hierarchies. Therefore, a fundamental requirement for a qualitative theory is the ability to entail basic relationships (those that the ontological engineer intends to preserve under extensions) among its concepts or relations. For instance, it has already been mentioned that RCC entails relationships between spatially defined relations, exhibiting a lattice structure of Figure 5, and a composition calculus, (as shown in Table 3) [39]. Likewise, any extension or revision of the ontology should thus meet similar requirements. In an effort inspired by foundational questions in the semantic web [ 106 ], a formal definition of a “robust ontology”, termed “lattice categorical extension” [ 87 ], was proposed. In brief, a “lattice categorical” theory is one that entails the lattice structure of its basic relations. Next, we formalize this notion. Given a fixed language L , let C={C1 , . . . , Cn} be a finite set of concept/relation symbols, and let T be a theory. Given M|=T , a model M of a T , consider the structure L(M , C) in the language LC={⊤ , ⊥ , ≤ , ∧ , ∨} ∪ {c1 , . . . , cn} defined as follows. The universe of L(M , C) consists of interpretations in M of C , with ci interpreted as CM i for each C∈ C . Here, ⊤ represents M , ⊥ represents ∅ , and ≤ denotes the subset relation. We denote |X| by the cardinal of set X. It is assumed that L(M , C) is required to have a lattice structure, although this requirement can be relaxed as the poset of relations among the concepts in C can be embedded into a lattice structure (even if it necessitates introducing dummy concept/relation names). In order to work with the relationships between the elements of C , it is necessary to work with equations that identify the basic operations with these elements. Definition 3. Consider the language LC={⊤,⊥,∧,∨} ∪ {c1, . . . , cn}. 1. The set of lattice closed equations in this vocabulary is denoted by EQL(C). 2. Given E is a set of equations, it is denoted by the ET translation of E to the set of first-order logic formulas in the language C. AI 2024,5765 Table 3. Composition table for the extension corresponding to L1. R2(b,c) R1(a,b)DC EC PO TPP NTPP TPPi NTPPi EQ I1 DC RCC8[I1] DC,EC, PO,TPP, NTPP,I1 DC,EC, PO,TPP NTPP,I1 DC,EC, PO,TPP, NTPP,I1 DC,EC, PO,TPP, NTPP,I1 DC DC DC DC,EC PO,TPP, NTPP,I1 EC DC, EC, PO,TPPi NTPPi DC,EC,PO, TPP,TPPi, EQ,I1 DC,EC, PO,TPP NTPP,I1 EC,PO, TPP NTPP,I1 PO,TPP NTPP,I1DC,EC DC EC EC,PO, TPP NTPP,I1 PO DC, EC, PO,TPPi NTPPi DC,EC, PO,TPPi NTPPi RCC8[I1]PO,TPP NTPP,I1 PO,TPP NTPP,I1 DC,EC PO,TPPi NTPPi DC, EC, PO,TPPi NTPPi PO PO,TPP NTPP,I1 TPP DC DC,EC DC,EC, PO,TPP NTPP,I1 NTPP DC,EC, PO,TPP TPPi,EQ I1 DC,EC, PO,TPPi NTPPi TPP TPP NTPP I1 NTPP DC DC DC,EC PO,TPP NTPP,I1 NTPP NTPP DC,EC PO,TPP NTPP,I1 RCC8[I1]NTPP NTPP,I1 TPPi DC, EC, PO,TPPi NTPPi EC,PO, TPPi NTPPi PO TPPi NTPPi PO,EQ TPP TPPi PO,TPP NTPPI1 TPi NTPP NTPPi TPPi PO,EQ TPP,TPPi NTPP,I1 NTPPi DC,EC PO,TPPi NTPPi POPPPi, NTPPi PO TPPi NTPPi PO TPPi NTPPi PO,TPPi TPP,NTPP NTPPi,EQ I1 NTPPi NTPPi NTPPi PO,TPPi TPP,NTPP NTPPi,EQ I1 EQ DC EC PO TPP NTPP TPPi NTPPi EQ I1 I1DC DC,EC DC,EC, PO,TPP NTPP,I1 NTPP,I1 DC,EC PO,TPP EQ NTPP,I1 RCC8[I1]I1TPP NTPP,I1 An example is presented in Figure 6, where a set of equstions E , and its translation ELRCC , is the set of formulas that appear in Figure 7. 16 = or(14,15). 15 = or(7,8). 14 = or(13,7). 13 = or(1,11). 13 = or(11,12). 13 = or(1,12). 12 = or(4,10). 11 = or(9,4). 10 = or(5,6). 9 = or(2,3). and(1,11) = 0. and(1,12) = 0. and(1,15) = 0. and(2,12) = 0. and(2,15) = 0. and(3,12) = 0. and(3,15) = 0. and(4,10) = 0. and(4,15) = 0. and(5,15) = 0. and(6,15) = 0. Figure 6. A set E⊆EQLRCC (C)which serves as a skeleton for RCC. AI 2024,5766 Figure 7. Theorems corresponding to lattice equations of Figure 6. A relationship between L(M , C) and model M can be established through the union of two sets of formulas. The first is a finite set E⊆EQL(C) (for example, that of Figure 6 for RCC). The second is a set of formulas ΘC that categorizes the lattice axioms under completion. The latter contains the following: • A domain closure axiom with respect to LC (ensuring that only named elements exist); • Unique name axioms (stating that different relation names denote different elements) [107] for the elements of C(which are the elements of the lattice); • The axioms of lattice theory (Figure 8). %conmutativity all x all y (or(x,y) = or(y,x)). all x all y (and(x,y) = and(y,x)). %asociativity all x all y all z (or(x, or(y,z)) = or(or(x,y),z)). all x all y all z (and(x, and(y,z)) = and(and(x,y),z)). %idempotence all x (or(x,x) = x). all x (and(x,x) = x). %absorption all x all y (x = or(x,(and(x,y)))). all x all y (x = and(x,(or(x,y)))). Figure 8. Prover9 axiomatization for the Lattice structure. These axioms are included in ΘLRCC . Idem: A lattice skeleton is a set E of lattice equations that characterizes (modulo ΘC ) the lattice of a model excluding isomorphism. The idea of a lattice skeleton is to have a set of interesting properties that we wish to preserve, and which are provable in the theory and its extensions. Definition 4. Let E be an LC theory. We say that E is a lattice skeleton (l.s.) for a theory T if E verifies that. •There are M |=T such that L(M,C)|=E∪ΘC, and •E∪ΘChas a unique model except isomorphism. Idem: The definition formalizes the concept of a comprehensive specification of the class or relation hierarchy, which, akin to description logic ontologies, a lattice skeleton would resemble a T -box with a specific inferential completeness, showcasing all the “subclass of” relations between classes in its concept hierarchy, thereby ensuring that all models share these selected relationships (expressed in the lattice language). Note that no condition of minimality on the set of equations E is requested. The reason is that the designer aims to represent in E all the information to be preserved in the AI 2024,5767 extensions, even if some of it is redundant to satisfy both properties of the above definition. If this was not the case, the application of techniques developed in [ 108 ] would allow (after passing to propositional formulas) us to reduce the size of the skeleton if necessary while preserving the information. Theorem 1. Every consistent theory has a lattice skeleton. Proof. (sketch) The proof is based on the description of a lattice skeleton for the theory T from a model M|=T: • First, the lattice L(M,C)is constructed. • Next, a set of lattice equations EC in the language (C , ⊤ , ⊥ , ≤ , ∧ , ∨ , ) is chosen so that there exists a single model of size |C| + 2 (these two additional elements correspond to ⊤and ⊥). Then, EC+ΘChas a unique model. 6.1. Lattice Categorical Theories Idem: It is worth noting that lattice skeletons are essentially model-based, so it is possible for there to be non-equivalent ones (modulo ΘC ). This poses challenges to reasoning with relations. While lattice skeletons characterize L(M , C) with intentional purposes, the existence of a unique lattice structure, up to isomorphism (thus entailed by T ), would enhance relational reasoning. This uniformity across models of T ensures consistency in relationships among the relations and enables the entailment of the transition table by T. Definition 5. A theory T is called a lattice categorical (l.c.) theory if every pair of lattice skeletons for T are equivalent theories modulo ΘC; that is, for any E1and E2skeletons for T, E1+ΘC≡E2+ΘC, as lattice theories. A key result regarding the extensions we aim to specify is the following, ensuring their existence: Theorem 2. Every consistent theory T has an extension which is lattice categorical. Proof. Idem: Let T be consistent and M be a model of T . Consider the partially ordered set XM whose elements are the interpretations CM for each C∈ C , and the relation ≤ represents the subset relation. In terms of sets, the lattice operations ∧ and ∨ are interpreted as ∩ and ∪, respectively. Consider L(M , C) the lattice generated by XM . Since C is finite, this lattice is also finite. Therefore, we can select E as a finite set of equations such that ΘC∪E has L(M , C) as its only model up to isomorphism. Then, the theory T+ETwould serve as such an extension. Idem: The most important feature of lattice categorical theories is that they guarantee reasoning only with the lattice equations is sufficient to work with the relations of the theory. E+ΘC allows focusing the reasoning on the relationships among the elements of C , avoiding the use of the more complex T . Lattice categoricity has been used for extending ontologies by the decision of the user, motivated by data and designed by the user [ 87 ], and ontology merging [ 109 ]. It is also necessary to emphasize that from a set E+ΘC , one can reconstruct a theory that has E as its skeleton, namely ET . An important example for our purposes is RCC: Theorem 3. RCC is a lattice categorical theory. AI 2024,5768 Proof. (sketch) The proof is assisted by Mace4 (to determine the models of the skeleton) and Prover9 (to find the justifying proofs). In the input file for Mace4, we introduce the following: • The set Efrom Figure 6; • The axioms characterizing the lattice theory (Figure 8). The axioms for unique names and domain closure would be missing. To simplify the coding work, each relation is assigned a number from 0 to 16, as shown in Figure 5. This ensures the principle of unique names when working with Mace4 without explicitly stating the axiom in ΘLRCC . Similarly, if models of size |LRCC ∪ {⊤ , ⊥}| = 17 are sought with Mace4, the domain closure axiom of ΘRCC is implicitly satisfied and does not need to be explicitly stated with formulas. The result follows from the following facts: • The only model obtained by Mace4 (Figure 9) has a Hasse diagram that matches that of Figure 5. •RCC entails all the formulas in ELRCC (provided in Figure 7). It is necessary to prove this to verify that the operations of the elements of the model found by Mace4 (Figure 6) are indeed theorems of RCC. Figure 9. Lattice operations of the model of E+ΘLRCC founded by Mace4, with E being the lattice skeleton from Figure 6. Finally, a lattice ontology is defined as a “complete” hierarchical view of a classic ontology as follows: Definition 6. Alattice ontology is a pair (T , E) , where T is the formal theory and E a lattice skeleton. If T is l.c., it will be called l.c. ontology. An example of a lattice categorical ontology is (RCC , E) , where E is the set of equations provided in Figure 6. It is important to note that the concept of a lattice ontology is more constrained than other notions, such as the usual pair (T,A) (i.e., T -box, A -box) in description logics. Let us consider a simple example of obtaining an lattice categorical extension in the form of a lattice ontology of a DL-ontology. Consider the ontology formed only with the T-box (A=∅): O:=C1⊑C2⊔C3 C2⊑ ¬C1. AI 2024,5769 Following the proof of Theorem 1, it suffices to select a model: I=Universe ={a,b,c} CI 1={a},CI 2={b},CI 3={a,c} Next, the poset (C1,C2,C3 , ⊆) is embedded into a lattice, for example, L , whose Hasse diagram is depicted in Figure 10. It is easy to see that the following lattice equation set is a skeleton for this lattice: E:=   c2∨c3=c4 c1∧c3=c1 c1∧c2=⊥ Figure 10. Partial order ⊑on the concepts (left) and one inmersion into a lattice (right). Therefore, (∅ , E) would be a lattice categorical extension, or, by explicating a DL- theory from E,(EO,E), being EO: EO:=       C4≡C2⊔C3 C2⊑ ¬C1 C1≡C1∧C3(i.e.C1⊑C3) C1∧C2≡ ⊥ (i.e.C1⊑ ¬C2) 6.2. Ontological Extension and Revision The following idea builds on concepts from [ 86 ], where we examine how information inconsistent with the base theory can be retrieved. The operators from that paper are not directly applicable here because we must select the information through its corresponding translation into lattice language. Recall that this information is included in the skeleton because we aim to preserve it as valid in the extension. The following formalization of robust ontological extension translates the notion of categorical extension in first-order logic (FOL) into a lattice-based ontology. Definition 7. Given two lattice ontologies (T1 , E1) , (T2 , E2) we will say that (T2 , E2) is a lattice categorical extension of (T1 , E1) (denoted by (T1 , E1)◁(T2 , E2) ) with respect to the sets of concepts C1and C2respectively, if •C1⊆ C2,(T2,E2)is lattice categorical and •E1is C1conservative on E2; that is, for any t =t′∈EQL(C1): E2|=t=t′=⇒E1|=t=t′. Please note that the above definition does not explicitly require any direct relationship between T1 and T2 , although such a relationship actually exists and can be extracted through ET 1 and ET 2 . Therefore, a type of lattice-based extension of the form (T∅ , E) can be found, where T∅ is the theory in the base first-order language without axioms. For example, AI 2024,5770 for E from Figure 6, this would be effectively equivalent to (ERCC , E) , where ERCC consists of the formulas appearing as theorems in Figure 7. 6.3. Extension Methodology Taking into account the construction carried out in this section, the proposed methodology for extending (possibly with revision) a formal ontology consists of the following stages: 1. Obtain T1 , a lattice categorical extension of the formal ontology to extend. In a skeleton E1 , include the relations between the concepts/relations of the set C1 of T1 that are to be preserved. The goal is to extend the revise the theory, possibly extending C1 with new concepts/relations, resulting in the language C2. 2. Extend the equations of E1 to obtain a new set of equations, E′ , where the fundamental relations that the new concepts/relations would have among themselves and with the original ones appear. Then, extend E′ to obtain E2 such that the theory E2+Θ has a unique model (lattice) up to isomorphism. The sought-after extension is (EC2 2,E). 3. Finally, interpret the new lattice ontology, possibly reinterpreting the elements of C1 , to align the extension with the new intended models. 7. A Case Study: Extending RCC The purpose of the second part of the paper is to explore, using the proposed methodology, extensions of RCC that accommodate relations of indefiniteness or vagueness among spatial regions. A motivation for this study is to provide a certified and complete blueprint of all possible definitions of uncertainty for RCC. Thus, the analysis should cover the various solutions existing in the literature. Additionally, this study would underpin the 3WD paradigm in RCC by offering all the possibilities of mereotopological combinations of regions with uncertainty. The problem ventures into a meta-meteorological realm as it necessitates reasoning within the RCC theory and adjusting its axioms accordingly for an extension of the type (RCC,E)◁(ELRCC∪{I} 2,E2), where Iwill denote the undefined relationship under study. According to the third stage of the extension methodology, to complete the study of the extensions, all new relations must be reinterpreted in the new intended models while respecting the global lattice structure of the relations. Given the importance of transition tables in QSR, the new spatial relation I , signifying “with a certain degree of indefiniteness”, should complement RCC8. That is, RCC 8 ∪ {I} should form a JEPD and should be incorporated into a new table of relation composition. Refer to [ 87 ] for alternative extension approaches. Based on this condition, using ELRCC∪{I} 2 , it should demonstrate, with the assistance of Prover9, the new transition table. If the intention is to interpret the new relation as “vague”, two options are available. The first option involves changing the semantics, as discussed in [ 110 ], while the second option entails reinterpreting the nature of the intended models of the original ontology. This would require revising the semantics, but it would be tailored specifically for that new class of intended models, which is common in 3WD reinterpretations. In this paper, we opt for the second option, which, as we will demonstrate in the following sections, allows for the derivation of classical interpretations in QSR through lattice categorical extensions of RCC. The main result on this kind of RCC extensions is the following: Theorem 4. There are only eight l.c. extensions of (RCC , E) (being E the lattice skeleton of Figure 6) by insertion of a new relation I such that RCC8∪ {I}is a JEPD set. Proof. (Sketch) The idea behind the proof is as follows: The language LRCC ∪ {I} is considered, and on this, a set of equations E∪ΘLRCC∪{I} is considered along with the AI 2024,5777 Figure 14. Egg-yolk relations (the enumeration of the seminal paper [ 63 ] has been preserved). In the figure, one region e-y ( a , a ) is represented by the flashing line figure (blue colour) and the other ( b , b ) by the dotted line figure (green colour). They have been grouped according to the RCC5 relationship between a and b (see Theorem 10). Since the objective to demonstrate is that the relations from {I1 , . . . , I5 , I7 , I8} ∪ RCC 5 are interpretable in this paradigm, we must find a specification in terms of the e-y paradigm relations. Theorem 10. The set {I1, . . . , I5,I7,I8} ∪ RCC5is interpretable in the egg-yolk paradigm. Proof. The interpretation (using the enumeration of Figure 14) is as follows: •DR ={1}and EQ ={42, 43, 44, 45, 46} •PP ={(A,B):PP(a,b)}which agree with I1(acording to lattice L1). Thus: I1=PP ={8,13,22,24,26,34,35,36,37,38,41}. •I2=PP ∪EQ ={8,13,22,24,26,34,35,36,37, 38,41,42,43,44,45,46}, • By symmetry, I3=PPi ={7,12,21,23,25,28,29,30,31,33,40}and I4=PPi ∪EQ ={7,12,21,23,25,28,29,30,31, 33,40,42,43,44,45,46}. •PO ={2,3,4,5,6,9,10,11,14,15,16,17,18,19,20, 27,32,39}, thus •I5=I2∪I4∪PO ={2, . . . , 46} •I7=DR ={1}. •I8={1,2, . . . , 46}=[ k∈{1,2,3,4,5,7} Ik=I5∪I7. AI 2024,5778 Corollary 3. RCC 5 ∪ {I1 , . . . , I5 , I7 , I8} induces, in the egg-yolk interpretation, the lattice structure depicted in Figure 15. Figure 15. Lattice of egg-yolk interpretations of new relationships. Proof. The proof follows from the classification of the interpretations of the relations e-y given in Theorem 10. Corollary 4. The set {I1,EQ,I3,PO,I7}is JEPD, and also {I2,I4,PO,I7}y{I5,I7}. Moreover, it is possible to build composition tables for their calculus from the lattice of Figure 15. Theorem 11. The theory RCC is interpretable in the class of models of the e-y paradigm. Proof. Since, in the egg-yolk paradigm, regions are represented as pairs (a , b) , it is necessary to add two function symbols to the language, e(·) and y(·) , to denote each component of a region. The formula φ(x)for the interpretation of RCC is as follows: φ(x):=EQ(e(x),y(x)) It is also possible to interpret the new relations of indefiniteness through contraction in the e-y paradigm. Given a vague region a , the “egg-yolk” representation would be the pair (ξ(a) , a) . To make the reasoning more legible, we denote ˜ a by the contraction of a . Using RCC5, the relations between each component of two regions can be specified. Given R∈RCC5, we denote e Rby the set (e×e)−1[R]; that is, (a,b)∈e R⇐⇒ (˜ a,˜ b)∈R This way, RCC5 is naturally included. The interpretation of RCC5 and the new indefiniteness relations is as follows: • The interpretation of PP coincides with the intuitive idea of being “proper part”. In our case, if a region A is a proper part of another B , then a and ˜ a are proper parts of ˜ b and, consequently, of b . This situation is represented by relation 24 in Figure 14. Thus, PP ={24}. Similarly, the remaining RCC5 relations can be interpreted. • On the other hand, the interpretation of f PP would be {(a , b):PP(˜ a , ˜ b)} , which, in turn, is the interpretation of I1due to its position in L1. Therefore, I1=f PP ={18,24,26,32,33,37,38,45} • The position of I2in L2suggests the interpretation AI 2024,5779 I2=f PP ∪f EQ ={18,24,26,32,33,37,38,39,40,41,45,46}, where f EQ ={39,40,41,46}. • By symmetry, I3and I4are defined similarly to I1and I2, respectively: I3=g PPi ={17, 23, 25, 27, 30,31,36,44} I4=g PPi ∪f EQ ={17,23,25,27,30,31,36,39,40,41,44,46} •f PO ={14,15,16,20,21,22,29,35,43}, therefore, I5=I2∪I4∪f PO, i.e., I5={14,15,16,17,18,20,21,22,23,24,25,26,27,29,30, 31,32,33, 35, 36, 37, 38, 39, 40, 41, 43, 44, 45, 46}. •I7=g DR ={1,2,3,4,5,6,7,8,9,10,11,12,13,19,28,34,42}. •I6 is nothing but a subset of I7 , as it contains figures where regions overlap but their contractions are discrete. Thus, I6={2,3,4,5,6,9,10,11,19} • Finally, as I8 represents total indefiniteness, it will be represented by any of the figures in Figure 14, so I8={1,2, . . . , 46} As seen, it is not necessary to interpret relation I6 although it is indeed possible since I8=[ k∈{1,2,3,4,5,7} Ik, which coincidentally is equal to I5∪I7. This observation is part of the proof of the following result: Theorem 12. In the egg-yolk interpretation described above, the relations I1 , . . . , I8 comprise the lattice in Figure 16, along with RCC5. Figure 16. Lattice of the relation set {I1, . . . I8} ∪ RCC5. Proof. It is necessary to proceed following the same strategy as in Theorem 6. As a corollary, different JEPDs are available for constructing a calculus through transition tables: Corollary 5. In the interpretation described above, the set of relations {I1 , f EQ , I3 , f PO , I7} forms a JEPD AI 2024,5780 8.2. Interpretation Inspired by Rough Set Theory In spatial reasoning, the focus on approximating a set is often associated with understanding its constituents (as illustrated in Example I), as well as with approximating or decomposing regions using others with a particular geometric or topological structure. This concept underlies the significance of rough approximation in naive set theory, which can be interpreted using concepts from RCC. Given the ambient space Ω and a family of sets {Xi:i∈I} , including subset b⊆X , it is approximated using a function ϕb:I7→ {fo , po , no} , where the values {fo , po , no} represent the relations of full overlap, partial overlap, and no overlap. The function ϕb indicates the degree of overlap between the subset b and the elements Xi of the partition of X. ϕb(i) =    fo if P(Xi,b) no if DR(Xi,b) po otherwise The approximations band bof the set bcan be defined in this context as follows: b=S{Xi:ϕb(i) = fo}, b=S{Xi:ϕb(i)=no}. To offer a fresh interpretation of the indefiniteness relations {Ik:k= 1...8 } employing rough notions, we will generalize the partition concept as follows. The underlying idea in this formalization is to consider sets with non-empty interiors as the “empty sets”. Definition 10. A topological space Ω is called DR-Rough if there exists F={Xi}_i ∈N a family of regular subsets of Ωsuch that: 1. ∀i=j:Ω|=DR(Xi,Xj)(i.e. Ω|=¬O(Xi,Xj)); 2. ∀J⊆Nthe set [ j∈J Xjis regular; 3. it is a covering of X, [ i∈N Xi=Ω. The family Fis called a DR-Rough cover. Note that, in the previous definition, condition 2is necessary since, in general, the union of regular sets is not regular. Consider the example in Figure 17. In R2 with the usual topology, let {Bn:n> 0 } be the family of closed balls with center ( 1 /n ,0 ) and radius 1/2(n+1). It is verified that [ n∈N Bn=[ n∈N Bn, since (0,0)∈[ n∈N Bnbut (0,0)/∈[ n∈N Bn. Figure 17. The union of regular sets is not regular in general. The idea of working with regions as DR-Rough spaces is interesting because it relates rough approximation with the approximation provided in this paper. This concept cuts across many research lines. For example, when working with boundary regions in 3WD or in the geometric case and when attempting to restructure concept AI 2024,5781 spaces using specific regions (e.g., [ 111 ]). Additionally, in the case of the local treatment of massive data, it could be useful (cf. [79]). Example 1. An example of a DR-Rough topological space, consider R2 and the cover F={Xij}i,j∈Z where Xij = [i,i+1]×[j,j+1](Figure 18). Figure 18. Diagram showing approximations of A⊆R2,Aand Aby DR-rough cover. In DR-rough spaces, the relations Ii can be interpreted with rough-type approximations. For this, consider a DR-rough cover F={Xi}i∈N of non-empty regular closed sets. It is easy to prove the following (see Figure 18): Theorem 13. Let b =S{Xi:Xi⊆b}and b =S{Xi:Xi∩b=∅}. Then: 1. σ(b) = b is a pulsation, and 2. ξ(b) = b is a contraction. Thus, σ(b)∖ξ(b) can be considered as an a rough fringe region of indecision in threeway clustering. 9. Conclusions and Future Work The need to revise formal ontologies for reuse presents logical and computational challenges, making this task in OE difficult to execute safely while adhering to representational principles and coherence. An ontology revision lacking formal grounding may compromise the quality of the ontology and the accuracy of the data it supports. Conversely, while the definitional methodology is theoretically suitable for extending ontologies, it encounters challenges in practical application, particularly in the case of non-lightweight ontologies. This paper presents a proposal for robustly extending and reusing formal ontologies, aiming to overcome the stringent constraints of the definitional methodology. The approach involves replacing the requirement of definability with weaker conditions associated with the (finite) ⊆ structure induced by the theory on its concepts/relations. By focusing on finite structures, it becomes feasible to effectively analyze extensions, facilitated by the use of ARS, enabling result verification. Moreover, this approach allows for the determination of all structures of a given type, with fewer requirements than the definitional methodology, facilitating the categorization and interpretation of generic extensions of formal ontologies. The second part of the paper focuses on applying the extension methodology to classify and interpret various classes of RCC extensions for vagueness, as well as computing their composition tables. These extensions are part of the logical foundation for ontology cleaning with RCC, as described in [ 99 ], and implemented using the associated tool. Furthermore, classic extensions of RCC have been reinterpreted as particular cases encompassed within the computed extensions. The case study also provides a solid foundation for reinterpreting mereotopological ontologies in the 3WD paradigm. The strength of the methodology we present for obtaining ontological extensions lies in considering a notion of lattice categoricity that is weaker than that of first-order logic categorical theory. This notion focuses on the relationships among concepts/relations that AI 2024,5782 are the representational objective of the ontology, avoiding the concept of categoricity in the sense of first-order logic, which is much more complex. In this way, with the assistance of automated reasoners, we can find the required extensions. As a trade-off for the loss of “uniqueness” that the definitional methodology provided, the method has limitations due to the weakening of conditions. The first is that it is not a method that can be applied independently of the domain expert or ontology user. It would be advisable for the expert to choose the relationships (the lattice skeleton) they wish to preserve in the extension. Likewise, as observed in the case of the RCC extension studied in the paper, there may be multiple extensions satisfying those constraints. This fact necessitates that, once calculated, the expert must be consulted to select the appropriate one. Although the first part of the paper conducts an analysis of the state of the art on RCC extensions and variants, it is important to emphasize that the logical–algebraic approach in studies on RCC is not entirely novel. For instance, in [ 112 ], RCC5 is studied by defining relations between regions using Boolean tuples. A partial order is induced between the five RCC5 relations. Ref. [ 113 ] introduces a method for approximately analyzing binary topological relations between regions with indeterminate boundaries. It includes examples demonstrating the determination of the eight relations in 2D space. Additionally, spatial reasoning within a fuzzy region connection calculus is explored in [ 61 ]. Notably, the paper establishes a close relationship with the egg–yolk paradigm and demonstrates that satisfiable knowledge bases can be realized by fuzzy regions in any dimension. In [ 114 ], multi-level topological relations of RCC-8 are introduced using concepts such as separation number and types of spatial elements. The paper focuses on detailing four relations: EC, PO, TPP, and TPPi at additional levels. On the other hand, in [ 62 ], there is a proposal to extend algebraic and topological relations between sets and fuzzy sets to bipolar fuzzy sets. Computing abstract RCC extensions may not be adequate when the new relations lack a mereotopological basis. Alternative methods like lattice alignment may be more appropriate. This issue will be the subject of future study. Likewise, estimating the complexity of constraint satisfaction problems (CSP) in the extensions is also an interesting research line. Additionally, we intend to apply the methodology to foundational ontologies, for example, attempting to resolve anomalies found in them through revisions (e.g., [25]). Author Contributions: Conceptualization, J.B.-D. and A.M.C.-G.; methodology, J.B.-D.; software, G.A.A.-C., J.B.-D. and A.M.C.-G.; validation, G.A.A.-C., J.B.-D., A.M.C.-G. and N.M.G.; formal analysis, G.A.A.-C., J.B.-D., A.M.C.-G. and N.M.G.; investigation, G.A.A.-C., J.B.-D., A.M.C.-G. and N.M.G.; resources, J.B.-D.; writing—original draft preparation, J.B.-D.; writing—review and editing, G.A.A.-C., J.B.-D., A.M.C.-G. and N.M.G.; visualization, J.B.-D.; supervision, J.B.-D.; project administration, J.B.-D.; funding acquisition, J.B.-D. All authors have read and agreed to the published version of the manuscript. Funding: This research was funded by Project PID2019-109152G, funded by the State Investigation Agency (Agencia Estatal de Investigación), MCIN/AEI/10.13039/501100011033. Institutional Review Board Statement: This study did not require ethical approval. Informed Consent Statement: Not applicable. The study did not involve humans. Data Availability Statement: No data was required for this work. Conflicts of Interest: The authors declare no conflicts of interest. Appendix A. Proof of Theorem 9 Let us take a look at the test step by step. Step 1: Let us see that (LRCC,≤)⊂(Lk,≤)for k∈1,2, . . . , 8. AI 2024,5783 •k=1 : The proofs for each R∈ RRCC ∖NTPP,TPP are analogous to each other. The same applies to the proofs for TPP and NTPP . Therefore, we demonstrate it for one of them in each case. POΩ1≤OΩ1:POΩ1=POΩ∩WRCC8σ ≤OΩ∩WRCC8σ=OΩ1 NTPPΩ1≤PPΩ1:NTPPΩ1=NTPPΩ∩NTPPσ ≤PPΩ∩WRCC8σ=PPΩ1 •k=2 : The proofs for each R∈ RRCC ∖PP,NTPP,TPP are analogous to each other. Therefore, we demonstrate the result for one of them. For instance, let us see that PΩ2≤OΩ2: PΩ2=PΩ∩WRCC8σ≤OΩ∩WRCC8σ=OΩ2 Next, we have to check the positions they occupy PP,NTPP yTPP. PPΩ2=PPΩ∩PPσ≤PΩ∩WRCC8σ=PΩ2 The cases of NTPP and TPP are analogous, so we see only one of them. NTPPΩ2=NTPPΩ∩PPσ≤PPΩ∩PPσ=PPΩ2 •k=3 : This case is identical to k=1 , with Ω1 , TPP , and NTPP replaced by Ω3 , TPPi , and NTPPi respectively. •k=4 : This case is identical to k=2 , with Ω2 , PP , TPP , and NTPP replaced by Ω4 , PPi,TPPi, and NTPPi, respectively. •k=5 : The proofs for each R∈ RRCC ∖{PO} are analogous to each other. Therefore, we demonstrate the result for one of them. For instance, let us see that NTPPΩ5≤ PPΩ5. NTPPΩ5=NTPPΩ∩WRCC8σ≤PPΩ∩WRCC8σ=PPΩ5 Next, we have to check the position of PO. POΩ5=POΩ∩POσ≤OΩ∩WRCC8σ=OΩ5 •k=6 : In this case, the interpretation of relations with contraction is performed. The proofs for each R∈ RRCC ∖{C,DR,EC,DC}are analogous to each other. Therefore, we demonstrate the result for one of them. For instance, let us see that PPΩ6≤PΩ6. PPΩ6=NTPPΩ∩Oξ≤PΩ∩Oξ=PΩ6 Next, we have to check the positions of C , DR , EC , and DC . and DC . Let us look at two of them. OΩ6=OΩ∩Oξ≤OΩ≤CΩ=CΩ6 ECΩ6=ECΩ≤DRΩ=DRΩ6 •k=7: We check the position of DC in the lattice. DCΩ7=DCΩ∩DCσ≤DRΩ∩WRCC8σ=DRΩ7 •k=8: Let us check, as an example, the relative position of EC yDR. ECΩ8=ECΩ∩ECσ≤DRΩ∩DRσ=DRΩ8. Step 2: In effect, we have the following: 1. I1Ω1= (TPPΩ∩(WRCC8σ∖{TPPσ})) ∪(NTPPΩ∩(WRCC8σ∖{NTPPσ})) <(PPΩ∩(WRCC8σ∖{TPPσ})) ∪(PPΩ∩(WRCC8σ∖{NTPPσ})) =PPΩ∩(WRCC8σ∖{TPPσ} ∪ WRCC8σ∖{TPPσ}) =PPΩ∩WRCC8σ=PPΩ1 2. I2Ω2=PPΩ∩(WRCC8σ∖{PPσ})<PΩ∩WRCC8σ=PΩ2 3. I3Ω3<PPiΩ3 : This case is identical to that of I1Ω1 , with Ω1 , PP , TPP , and NTPP replaced by Ω3,PPi,TPPi, and NTPPi, respectively. 4. I4Ω4<PiΩ4 : This case is identical to that of I2Ω2 , replacing Ω2 , P , and PP with Ω4 , Pi , and PPi, respectively. 5. I5Ω5<OΩ5 : This case is identical to that of I2Ω2 , replacing Ω2 , P , and PP with Ω5 , O , and PO, respectively. 6. I6Ω6=OΩ∩DRξ<OΩ<CΩ=CΩ6. 7. I7Ω7<DRΩ7 : This case is identical to that of I2Ω2 , replacing Ω2 , P , and PP with Ω7 , DR, and DC, respectively. AI 2024,5784 Step 3: In this step, it is sufficient to verify that for each k∈ { 1,2, . . . ,8 } , the relation Ik Ωk is disjoint from the rest of the relations in the lattice Lk . This is an immediate consequence of the interpretation of Ik. •k=1: IΩ1 1∧TPPΩ1= (TPPΩ∩(WRCC8σ∖{TPPσ})) ∪(NTPPΩ∩(WRCC8σ∖{NTPPσ})) ∩TPPΩ1= (TPPΩ∩(WRCC8σ∖{TPPσ})∩TPPΩ∩TPPσ)∪ (NTPPΩ∩(WRCC8σ∖{NTPPσ})∩TPPΩ∩TPPσ) = ⊥ por ser (WRCC8σ∖TPPσ)∩TPPσ=⊥yNTPPΩ∩TPPΩ=⊥ Similarly, the following is tested: IΩ1 1∧NTPPΩ1=⊥. Now let us see that IOmega1is disjunct with POΩ1 IΩ1 1∧POΩ1=IΩ1 1∧(POΩ∩WRCC8σ) = (TPPΩ∩(WRCC 8 σ∖{TPPσ})) ∪(NTPPΩ∩(WRCC 8 σ∖{NTPPσ})) ∩ POΩ∩WRCC8σ= (TPPΩ∩POΩ∩(WRCC8σ∖{TPPσ})∩WRCC8σ)∩ (NTPPΩ∩POΩ∩(WRCC8σ∖{NTPPσ})∩WRCC8σ) = ⊥ for being (WRCC8σ∖NTPPσ)∩NTPPσ=⊥yTPPΩ∩POΩ=⊥. It is also tested for R∈ RRCC ∖{TPP,NTPP} •k=2: IΩ2 2∧PPΩ2=PPΩ∩WRCC8σ∖{PPσ} ∩ PPΩ∩PPσ=⊥ because (WRCC8σ∖PPσ)∩PPσ=⊥. The same is true for NTPPΩ2yTPPΩ2: Let us look at the case of POΩ2: IΩ2 2∧POΩ2=PPΩ∩WRCC8σ∖{PPσ} ∩ POΩ∩WRCC8σ=⊥ because PPΩ∩POΩ=⊥. The same is done for the rest of the relationships of the RRCC. • The rest of the cases, except for underlinek =6 , are solved in a similar way to the previous two. •k=6 : IΩ6 6∧ECΩ6=OΩ∩DRξ∩ECΩ=⊥ por ser OΩ∩ECΩ=⊥ . Por otra parte, IΩ6 6∧OΩ6=OΩ∩DRξ∩OΩ∩Oξ=⊥ por ser DRξ∩Oξ=⊥ ya que ξ es una contracción. Step 4: Lastly: •k=1: We have to demonstrate that TPPΩ1∨NTPPΩ1∨IΩ1 1=PPΩ1: TPPΩ1∨NTPPΩ1∨IΩ1= (TPPΩ∩TPPσ)∪(NTPPΩ∩NTPPσ)∪(TPPΩ ∩(WRCC 8 σ∖TPPσ)) ∪(NTPPΩ∩(WRCC 8 σ∖NTPPσ)) = (TPPΩ∩WRCC 8 σ)∪ (NTPPΩ ∩WRCC8σ) = (TPPΩ∪NTPPΩ)∩WRCC8σ=PPΩ∩WRCC8σ=PPΩ1 •k=2 : We must test two results: NTPPΩ2∨TPPΩ2=PPΩ2 y PPΩ2∨EQΩ2∨I2Ω2= PΩ2: –NTPPΩ2∨TPPΩ2= (NTPPΩ∩PPσ)∪(TPPΩ∩PPσ) = (NTPPΩ∪TPPσ)∩ PPσ=PPΩ∩PPσ=PPΩ2 –PPΩ2∨EQΩ2∨I2Ω2= (PPΩ∩PPσ)∪(PPΩ∩(WRCC 8 σ∖PPσ)) ∪(EQΩ∩ WRCC8σ) = (PPΩ∩WRCC8σ)∪(EQΩ∩WRCC8σ) = PΩ∩WRCC8σ=PΩ2 •k=3 : We have to demonstrate that TPPiΩ3∨NTPPiΩ3∨IΩ3 3=PPiΩ3 .The proof is identical to the case k=1 , replacing PP , TPP , and NTPP with PPi , TPPi , and NTPPi , respectively. •k=4 : The same applies in this case. It suffices to replace in the proof of the case k=2 the relations P,PP,TPP, and NTPP with Pi,PPi,TPPi, and NTPPi, respectively. •k=5: Let us verify that the following is true: IΩ5 5∨POΩ5∨PΩ5∨PiΩ5=OΩ5: IΩ5 5∨POΩ5∨PΩ5∨PiΩ5= (POΩ∩(WRCC 8 σ∖POσ)) ∪(POΩ∩POσ)∪(PΩ∩ WRCC 8 σ)∪(PiΩ∩WRCC 8 σ) = (POΩ∩WRCC 8 σ)∪(PΩ∩ WRCC8σ)∪(PiΩ∩WRCC8σ) = OΩ∩WRCC8σ=OΩ5 AI 2024,5785 •k=6 : In this case, we will demonstrate, as an example, two results. The others are obtained in the same manner. –OΩ6∨IΩ6 6∨ECΩ6=CΩ6: OΩ6∨IΩ6 6∨ECΩ6= (OΩ∩Oξ)∪(OΩ∩DRξ)∪ECΩ= (OΩ∩(Oξ∪DRξ)) ∪ ECΩ=OΩ∪ECΩ=∪CΩ=CΩ6 –POΩ6∨PΩ6∨PPiΩ6=OΩ6 POΩ6∨PΩ6∨PPiΩ6= (POΩ∩Oξ)∪(PΩ∩Oξ)∪(PiΩ∩Oξ)=(POΩ∪PΩ∪ PiΩ)∩Oξ=OΩ∩Oξ=OΩ6 •k=7: The following are verified: ECΩ7∨DCΩ7∨IΩ7 7=DRΩ7: ECΩ7∨DCΩ7∨IΩ7 7= (ECΩ∩WRCC 8 σ)∪(DCΩ∩DCσ)∪(DCΩ∩(WRCC 8 σ∖ DCσ)) = (ECΩ∩WRCC8σ)∪(DCΩ∩WRCC8σ) = DRΩ∩WRCC8σ=DRΩ7 •k=8: The test consists of testing various results: –ECΩ8∨DCΩ8= (ECΩ∩ECσ)∪(DCΩ∩DRσ)⊆DRΩ∩DRσ=DRΩ8 The other containment also holds. Let (a , b)∈DRΩ∩DRσ . Since it belongs to DRΩ , it implies (a , b)∈DCΩ , and therefore (a , b)∈(DCΩ∩DRσ) , or alternatively, it implies (a , b)∈ECΩ , and hence (a , b)∈(ECΩ∩ECσ) , from which (a,b)∈ECΩ8∨DCΩ8. –CΩ8∨DRΩ8∨IΩ8 8= (CΩ∩Cσ)∪(DRΩ∩DRσ)∪(CΩ∩DRσ)∪(DRΩ∩Cσ) = ((CΩ∩DRΩ)∩Cσ)∪((CΩ∩DRΩ)∩DRσ) = ⊤ – It is necessary to verify that the relations in RRCC ∖{DR , EC , DC} also maintain the structure. For example: PPΩ8∨EQΩ8= (PPΩ∩Cσ)∪(EQΩ∩Cσ) = (PPΩ∪EQΩ)∩Cσ=PΩ∩Cσ=PΩ8 References 1. Gruber, T.R. A translation approach to portable ontology specifications. Knowl. Acquis. 1993,5, 199–220. [CrossRef] 2. Tambassi, T. The Philosophy of Geo-Ontologies; Springer Briefs in Geography; Springer: Cham, Swizerland, 2018. [CrossRef] 3. Uschold, M.; Gruninger, M. Ontologies: Principles, methods and applications. Knowl. Eng. Rev. 1996,11, 93–136. [CrossRef] 4. Gómez-Pérez, A.; Fernández-López, M.; Corcho, O. Ontological Engineering; Advanced Information and Knowledge Processing; Springer: London, UK, 2004. [CrossRef] 5. Baader, F.; Calvanese, D.; McGuinness, D.L.; Nardi, D.; Patel-Schneider, P.F. (Eds.) The Description Logic Handbook, 2nd ed.; Cambridge University Press: Cambridge, UK, 2007. 6. Grüninger, M.; Katsumi, M. Foundationless Ontologies. In Proceedings of the Joint Ontology Workshops 2019 Episode V: The Styrian Autumn of Ontology, Graz, Austria, 23–25 September 2019; Barton, A., Seppälä, S., Porello, D., Eds.; CEUR Workshop Proceedings; CEUR-WS.org: Aachen, Germany, 2019; Volume 2518. 7. Bennett, B. The Role of Definitions in Construction and Analysis of Formal Ontologies. In Logical Formalization of Commonsense Reasoning (2003 AAAI Symposium); AAAI Press: Menlo Park, CA, USA, 2003. 8. Fernández-López, M.; Gómez-Pérez, A.; Suárez-Figueroa, M.C. Methodological guidelines for reusing general ontologies. Data Knowl. Eng. 2013,86, 242–275. [CrossRef] 9. Grütter, R.; Scharrenbach, T.; Bauer-Messmer, B. Improving an RCC-Derived Geospatial Approximation by OWL Axioms. In Proceedings of the The Semantic Web-ISWC 2008, LNCS 5318, Karlsruhe, Germany, 26–30 October 2008; Springer: Berlin/Heidelberg, Germany, 2008; pp. 293–306. 10. Jonsson, P. Constants and finite unary relations in qualitative constraint reasoning. Artif. Intell. 2018,257, 1–23. [CrossRef] 11. Inants, A.; Euzenat, J. So, what exactly is a qualitative calculus? Artif. Intell. 2020,289, 103385. [CrossRef] 12. Renz, J. Qualitative Spatial Reasoning with Topological Information, Lecture. In Lecture Notes in Artificial Intelligence; Springer: Berlin/Heidelberg, Germany, 2002; Volume 2293. 13. Bennett, B.; Isli, A.; Cohn, A. When does a composition table provide a complete and tractable proof procedure for a relational constraint language? In Proceedings of the IJCAI-97, Nagoya, Japan, 23–29 August 1997. 14. Lima, G.; Machado, M.; Uceda-Sosa, R.; Moreno, M.F. Practical Rule-Based Qualitative Temporal Reasoning for the Semantic Web. In Proceedings of the RuleML+RR, Leuven, Belgium, 13–15 September 2021; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 2021; Volume 12851, pp. 188–202. 15. Duckham, M.; Li, S.; Liu, W.; Long, Z. On Redundant Topological Constraints. arXiv 2014, arXiv:1403.0613. 16. Hernández, D. Qualitative Representation of Spatial Knowledge; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 1994; Volume 804. 17. Cohn, A.G.; Renz, J. Qualitative Spatial Reasoning. In Handbook of Knowledge Representation; Elsevier: Amsterdam, The Netherlands, 2007. AI 2024,5786 18. Xiao, Q.; Qin, K.; Guan, Z.; Wu, T. Image mining for robot vision based on concept analysis. In Proceedings of the 2007 IEEE International Conference on Robotics and Biomimetics (ROBIO), Sanya, China, 15–28 December 2007; pp. 207–212. 19. Davis, E.; Marcus, G. The scope and limits of simulation in automated reasoning. Artif. Intell. 2016,233, 60–72. [CrossRef] 20. Hahmann, T.; Grüninger, M. Region-Based Theories of Space: Mereotopology and Beyond. In Qualitative Spatio-Temporal Representation and Reasoning: Trends and Future Directions; IGI Global: Hershey, PA, USA, 2012; p. 62. [CrossRef] 21. Aameri, B.; Grüninger, M. Location ontologies based on mereotopological pluralism. Appl. Ontol. 2020,15, 135–184. [CrossRef] 22. Galton, A. Yet Another Taxonomy of Part-Whole Relations. In Joint Ontology Workshop; CEUR Workshop Proceedings; CEURWS.org: Aachen, Germany, 2018; Volume 2205. 23. Museros, L.; Escrig, M.T. A Qualitative Theory for Shape Representation and Matching for Design. In Proceedings of the 16th European Conference on Artificial Intelligence, NLD, Valencia, Spain, 22–27 August 2004; ECAI’04, pp. 858–862. 24. Muñoz, L.S.; Grüninger, M. The Mereologies of Upper Ontologies. In Knowledge Discovery, Knowledge Engineering and Knowledge Management—8th International Joint Conference, IC3K 2016, Porto, Portugal, 9–11 November 2016; Revised Selected Papers; Communications in Computer and Information Science; Fred, A.L.N., Dietz, J.L.G., Aveiro, D., Liu, K., Bernardino, J., Filipe, J., Eds.; Springer: Berlin/Heidelberg, Germany, 2016; Volume 914, pp. 191–212. [CrossRef] 25. Silva Muñoz, L.; Grüninger, M. The Mereologies of Upper Ontologies. In Knowledge Discovery, Knowledge Engineering and Knowledge Management; Fred, A., Dietz, J., Aveiro, D., Liu, K., Bernardino, J., Filipe, J., Eds.; Springer: Cham, Switzerland, 2019; pp. 191–212. 26. Li, T.; Liu, J.; Sun, H.; Chen, X.; Zhang, L.; Sun, J. A spatio-temporal specification language and its completeness & decidability. J. Cloud Comput. 2020,9, 65. 27. Banci Buonamici, F.; Belmonte, G.; Ciancia, V.; Fabiano, V.; Guerrini, G.; Mesiti, M.; Sorrentino, D. Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf. 2020,22, 195–217. [CrossRef] 28. Bittner, T.; Donnelly, M. Logical properties of foundational relations in bio-ontologies. Artif. Intell. Med. 2007,39, 197–216. [CrossRef] [PubMed] 29. Bittner, T.; Goldberg, L.J. The qualitative and time-dependent character of spatial relations in biomedical ontologies. Bioinformation 2007,23, 1674–1682. [CrossRef] 30. Donnelly, M.; Bittner, T.; Rosse, C. A Formal Theory for Spatial Representation and Reasoning in Biomedical Ontologies. Artif. Intell. Med. 2006,36, 1–27. [CrossRef] [PubMed] 31. Baryannis, G.; Tachmazidis, I.; Batsakis, S.; Antoniou, G.; Alviano, M.; Sellis, T.; Tsai, P.W. A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming. Theory Pract. Log. Program. 2018,18, 355–371. [CrossRef] 32. Izmirlioglu, Y.; Erdem, E. Qualitative Reasoning about 2D Cardinal Directions using Answer Set Programming. J. Artif. Intell. Res. 2023,77, 1371–1453. [CrossRef] 33. Cohn, A.G.; Bennett, B.; Gooday, J.; Gotts, N.M. Qualitative Spatial Representation and Reasoning with the Region Connection Calculus. GeoInformatica 1997,1, 275–316. [CrossRef] 34. Chen, J.; Cohn, A.G.; Liu, D.; Wang, S.; Ouyang, J.; Yu, Q. A survey of qualitative spatial representations. Knowl. Eng. Rev. 2015, 30, 106–136. [CrossRef] 35. Borgo, S. RCC and the Theory of Simple Regions in R2. In Spatial Information Theory; Tenbrink, T., Stell, J., Galton, A., Wood, Z., Eds.; Lecture Notes in Computer Science; Springer: Cham, Switzerland, 2013; Volume 8116. [CrossRef] 36. Ivanova, T.; Vakarelov, D. Distributive mereotopology: Extended distributive contact lattices. Ann. Math. Artif. Intell. 2016, 77, 3–41. [CrossRef] 37. Balbiani, P.; Ivanova, T. Representation theorems for extended contact algebras based on equivalence relations. arXiv 2019, arXiv:1901.10367. 38. Klippel, A.; Li, R.; Yang, J.; Hardisty, F.; Xu, S. The Egenhofer–Cohn Hypothesis or, Topological Relativity? In Cognitive and Linguistic Aspects of Geographic Space; Raubal, M., Mark, D., Frank, A., Eds.; Lecture Notes in Geoinformation and Cartography; Springer: Berlin/Heidelberg, Germany, 2013. [CrossRef] 39. Randell, D.; Cohn, A.; Cui, Z. Computing transitivity tables: A challenge for automated theorem provers. In Automated Deduction—CADE-11; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 1992; Volume 607; pp. 786–790. 40. Katsumi, M.; Grüninger, M. The metatheory of ontology reuse. Appl. Ontol. 2018,13, 225–254. [CrossRef] 41. Wang, P.; Yao, Y. CE3: A three-way clustering method based on mathematical morphology. Knowl.-Based Syst. 2018,155, 54–65. [CrossRef] 42. Aranda-Corral, G.A.; Borrego-Díaz, J.; Chávez-González, A.M. Extending Qualitative Spatial Theories with Emergent Spatial Concepts. In Hybrid Artificial Intelligence Systems; Polycarpou, M., de Carvalho, A.C.P.L.F., Pan, J.S., Wo´zniak, M., Quintian, H., Corchado, E., Eds.; Springer, Cham, Switzerland, 2014; pp. 427–438. 43. Ru, Y.; Gruninger, M. Parts Unknown: Mereologies for Solid Physical Objects. In Joint Ontology Workshops; CEUR Workshop Proceedings; CEUR-WS.org: Aachen, Germany, 2017; Volume 2050. 44. Mazzola, C. The Mereotopology of Time. Notre Dame J. Form. Log. 2019,60, 215–252. [CrossRef] 45. Landau, B. Learning Simple Spatial Terms: Core and More. Top. Cogn. Sci. 2020,12, 91–114. [CrossRef] [PubMed] 46. Keet, C.M.; Khumalo, L. Parthood and part-whole relations in Zulu language and culture. Appl. Ontol. 2020,15, 361–384. [CrossRef]