Foundational relations are formal and generic relations presenting a basic pillar of foundational ontologies (FOs). The employment of these relations in practice has become widely prevalent by means of FOs. However, for the utilization of sole foundational relations, we believe that a basis done exclusively on a FO is unsatisfactory due to (1) the dificulties that modelers face upon selecting a FO for practice, and (2) the fact that no FO incorporates inclusively the basic set of foundational relations in which we are interested. Hence, we have proposed in an earlier work an entity-type-free minimal set of Foundational Ontological Relations Theory (FORT). In this paper, we expound on the two arguments for FORT, compare and elucidate an alignment between FORT's micro-theories and the relation-based content of some FOs, and associate FORT with a CLIF-serialization that validates the consistency of the theory.
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). foundational relations; parthood, dependence, constitution, membership, and location with the formal properties and relations that are required to characterize them.
Moreover, foundational relations, together with general primitive concepts, form the pillars of foundational ontologies (FOs) aka upper/top-level ontologies. Nowadays, FOs are establishing forward the development of specific (core, domain, and application) ontologies and ontologydriven conceptual models i.e. enhancing the construction of models that are compliant with FOs and their ontological commitments, which guarantees their validation. In addition to that, achieving interoperability between models is reinforced upon the employment of FOs such as in the integration of diferent ontologies that comply to a unique FO in inter-disciplinary fields. As a consequence, the employment of foundational relations has become widely prevalent by means of FOs, where a unique set of relations is ofered and formalized in each.
Although some relations are commonly addressed among FOs, this set varies according to the ontological commitments made by each FO. For instance, a FO that revokes the co-existence of multiple individuals in the same space-time would treat the relation between a constituent and the constituted entity as an identity but not a constitution, and thus rejects the inclusion of constitution within its set of foundational relations. Thus, it is noticed that no FO covers completely the set of foundational relations in which we are interested (1). In addition to that, upon selecting a FO for practice, it is often recognized that modelers do face some complications concerning the complexity of the FO, the obligation to conform to the ontological commitments of the FO, and the concept-hierarchy mappings (2).
Based on the two preceding issues, we believe that for the representation and employment of solely foundational relations in general, and the mentioned set of relations in particular, a basis done exclusively on a FO is unsatisfactory.
Hence, in [
Therefore, the contributions of this paper are twofold; (a) the positioning and alignment of FORT with respect to some FOs, and (b) the validation of FORT’s consistency while providing a CLIF-serialization.
In this section, we illustrate briefly the work done around FORT in [
In the following, we clarify some characteristics of FORT. First, the notion of intralinked relation micro-theories corresponds to a group of definitions, axioms, and theorems that characterize our view (ontological analysis) of a specific relation. Theoretically, each relation has been thoroughly discussed taking into account its literary ontological and philosophical work. Empirically then, the relation has been formalized by importing, reusing and adapting extant theories according to our ontological analysis and requirements.
Second, the notion of interlinked micro-theories corresponds to links drawn between the relations of each micro-theory using axioms.
Third, the notion of entity-type free corresponds to the theory not committing to specific kinds, aka categories, for the entities participating in the relation; the domain and range of relations. Instead, FORT characterizes formally the relations by normalizing constraints on the relata of the relation upon their identification in practice. This is done by introducing axioms that project restrictions on the types that will be allocated for each relation while used in conceptual models, since the theory’s utilization is intended as a. This makes the theory straightforward to integrate within extant theories, without obliging the compliance to a hierarchy of entity types. Fourth, a basic assumption that FORT makes is to distinguish the parthood relation from membership and constitution. This demarcation is adopted to (a) refrain a philosophical debate on the consideration of these relations as part-whole typologies, (b) delimit the scopes upon which transitivity holds, and (c) advocate for the additional semantics that each relation acquires divergent from one another.
The axiomatization of FORT’s micro-theories is briefly illustrated in the appendix section (without presenting that of imported theories i.e. the closure extensional mereology (CEM), the minimal mereotopology (MT), and Varzi’s location (L) theories).
At this point, one might argue that FORT is just a repository of relations gathered as a grab-bag ontology. However, FORT ofers more than just a repository; (1) positioning FORT concerning the well-known literary work on foundational relations where the analysis and valorization of extant work have been performed; (2) analyzing the requirements in the ontology-driven conceptual modeling context in general, and concerning our motivation in particular, where the selection, re-use, and re-formalization of foundational relations have been rendered; and (3) ofering what preceded within a generic context as an entity-type free theory where the significance of FORT lies. We believe that such an approach is not a repository, but a theory.
While a major limitation of the approach is in its assumption of being atemporal, the forte contribution points of FORT are twofold. First, the relations being generic and entity-type free ofering modelers wide semantics of primitive relations without obliging primitive concepts. Second, the selected set of relations being ample for representing the internal structure, spatial conditions, and interrelations between entities as a minimal, yet inclusive, group of imported and formulated micro-theories of relations.
In this section, we expound on the arguments for FORT that derive from two challenges (issues introduced in section Section 1) faced by modelers employing FOs for with the aim to use foundational relations. In particular, we focus on the selected set of relations in which we are interested. It is important to point out that the two defended arguments promote the need for FORT, but do not make assumptions of drawbacks or shortcomings on extant FOs, nor do they argue for eliminating the practice on existing FOs and their corresponding conveniences. The employment of FORT is an option in the conceptual modeling tasks that do not seek the adoption of a category hierarchy but only the utilization of foundational relations. The dificulties upon the adoption and employment of a FO: The first dificulty is the responsibility that a FO choice incorporates towards understanding the diferent ontological and philosophical assumptions made in each FO. With the numerous FOs available today, the modeler having to choose a FO for practice has to understand several points; what does each FO ofer diferently from one another? what are the theoretical modeling decisions made in each FO, i.e. the ontological commitments that correspond to the world view it acquires? how are these ontological commitments empirically translated into formalizations? Performing such a comparison between FOs is a dificult task since most diferences occur at a high meta-physical level which requires deep philosophical understanding. After having this comparison, the modeler has to elect a FO for practice according to the needs of the application domain. This involves answering the following; how can the modeling dilemmas present in the application domain be represented in each FO? how are these representations diferent, and what are the conveniences ofered by each? Only if the modeler can answer all these questions, that necessitate massive work and time eforts, then the proper justification of the choice of FO can be made.
The second dificulty is the entire commitment to the assumptions made in the chosen FO
regarding its world-view. Upon employing a FO, the modeler is committed to its view on the
elements of reality that is wholly interpreted in its formalization. This can be problematic for
the modeler when the modeling dilemma ought to be modeled, cannot be fully represented
by the chosen FO due to the fact that a specific assumption made by it, rejects this view in
the dilemma. In case the assumption in the FO is ignored, the representation will yield in
contradicting semantics. And in case all assumptions are complied to, then the representation
of the dilemma is not fully achieved. Knowing that the list of ontological commitments varies
from one FO to another, one might want to comply with one assumption from one FO e.g.
BFO’s [
The third dificulty is the obligation to adhere to the categories-hierarchy of the chosen FO. This does not only oblige modelers to map the domain-specific types (aka kinds or categories) in their models to the top-level categories in the chosen FO, but also to comply to the constraints that each type acquires. For example, the category ”Non-Agentive-Physical-Object” in DOLCE is disjoint from the category ”Amount-of-Matter”, and requires that any instance of the former be generically constantly constituted by an instance of the latter by the axioms characterizing both categories. Thus, all categories that are mapped to any of the preceding two, will acquire additional inherited axioms and semantics that the modeler shall comply with. Thus, several obstacles arrive with FOs in general, and with the commitment to category hierarchies in particular. If the aim behind using a FO is foundational relations, then why not have a relation-centered approach and ignore any taxonomic category axioms? No FO incorporates inclusively the specified set of foundational relations: In this argument, we highlight an issue that is not (yet) handled in extant FOs. There is currently no FO that incorporates the intended foundational relations altogether; parthood, dependence, constitution, membership, and location. We elaborate on our claim by addressing some FOs.
BFO does not (and cannot) express constitution due to its reductionist view. BFO is a realist ontology capturing the world as (multiple) particular perspectives of reality i.e. possibly multiple instantiations of the same particular individual. For constitution, BFO regards the entities participating in a constitution relation, e.g. the vase and the clay, as the same spatiotemporal individual that instantiates diferent universals at the same space-time location i.e. an identity relation instead. Such an argument is added to BFO’s formalization using an axiom that prevents two material entities from occupying the same spatial region unless they coincide i.e. the relations collapse to an identity. Now if constitution is to be represented in BFO, then it will be a relationship taking place between an individual and itself as an instance of two diferent universals i.e. individual ID1 as an instance of a statue and the same ID1 as an instance of clay. This thus requires the fact that individual ID1 be instantiating two classes at the same time instance t. Let’s say BFO succeeds in representing such restrictions on a constituted relation. What about the specificity vs generality of this constitution? In other words, is it a constitution that is applied specifically to these to individuals? Or is it a constitution that takes place between any instance of the category of the constituent entity (any instance of clay) and any of the constituted entity (any instance of statue)? In the latter case, the representation of constitutional dependence (generic) between the constituent and the constituted entity, which is an important axiom in the characterization of the constitution relation, will still be unachievable. This is because constitutional dependence requires the two class types to be disjoint to ensure that the causal existential connection between instances of the classes comes to an end. Thus, constitution remains to be problematic for BFO.
DOLCE, on the other hand, does not explicitly define a locative relation nor does it adopt a
specific location theory such as that of Varzi. Instead it ofers locative representations via
qualities and quales as will be explained in section 4. In view of such a comprehensive treatment
of relations, membership is not (yet) covered within DOLCE’s specification. Although in the
earlier analysis of building DOLCE, in [
Similar to DOLCE, with some diferences in their treatment of regions, UFO does not integrate a
theory of location relations. Instead it presents an entity-type based approach of attributes and
attribute value spaces following [
Thus, each of the tackled FOs lacks some relation(s) due to some of its ontological commitments. If the intended relations are specified, then why not have an inclusive relation theory that encompasses the desired relations entirely?
In this section, we align and elucidate a relation-based comparison between each micro-theory in FORT and the corresponding consideration of the relation made in the FOs; BFO, DOLCE, and UFO, summarized in table 1. The FOs that we inspect are those to which our theory presents high similarities.
The dependence relation is generally defined in terms of an existence primitive relation, also referred to as ”being present”. The existence relation is pretty similarly presented in all FOs; existsAt in BFO, PRE (being present at) in DOLCE as binary predicates between an entity and an instance of time, and ex in UFO as a unary predicate due to a single time slice formalization. In BFO; ontological dependence is introduced in the form of entity types that are dependent on other entity types i.e. such as: qualities, functions, roles, and dispositions, and . This dependence is carried out via relation s-depends_on has as a domain a and as a range; an or in case of a one-sided s-dependence, or a in case of a reciprocal s-dependence.
In UFO, in addition to existential dependence (, ) and independence (, ) , functional
dependence is also studied in its generic (Φ, Ψ) and individual (, Φ, , Ψ) -defined in
terms of - forms according to the treatment of functional parts by Guizzardi in [
FORT adopts CEM, while DOLCE and UFO both adopt GEM, and BFO constructs its own mereology within its continuant part of relation.
FORT further accounts the combination of parthood with dependence to introduce the notion of inseparable parts (essential and mandatory); elements and components. This is plausible in DOLCE since the primitive relations (parthood and specific/generic existential dependence) exist. In UFO, it is feasible using the existential dependence relation to introduce essential parts (aka elements in FORT) but not mandatory parts (aka components in FORT). However, UFO does define dependent parts as components using the (, ) relation that is proper parthood (, ) accompanied with a restriction on the individual functional dependence of the whole on the part (, ′, , ′).
For the mereotopological theoretical aspect, none of the considered FOs imports the connection topological theory, whereas FORT imports minimal mereotopology i.e. the primitive connection relation with its corresponding topological predicates.
Since locative relations in FORT are divided into three types, we investigate according to each type, the similar relations in each of the studied FOs.
• region-to-region locative relations: Without committing to a region entity type, FORT
suggests the use of the primitive parthood relation − to express mereotopological
representations between entity types that can be regions. This is similar to BFO’s
utilization of its own mereological relation between spatial regions, and
DOLCE’s and UFO’s use of the primitive mereological relation .
• entity-to-region locative relations: In FORT, we import Varzi’s location theory [
FORT examines membership (, ) as a primitive relation that is defined in terms of
ground axioms with the characterization of its whole entity. Although FORT does not account
for entity types, it requires restriction on the range of the membership relation to be unified
( ) , through its members, by a unification relation (, ) . The axiomatization provided in
FORT is similar to that in BFO except that BFO uses a class type to characterize
the whole while FORT does not, and BFO does not oblige the binding of all members according
to a similarity constraint i.e. unifying relation. UFO also provides a membership primitive
(, ) that holds between an object and a collection following the preliminary analysis
in [
FORT treats constitution in a very similar manner to that in DOLCE and UFO. Using a constitution primitive (, ) ( (, ) in DOLCE, and ( , ) in UFO) along with defining specific and generic constitutional dependencies (, )/(Ψ, Φ) . However, in contrary to DOLCE’s concept , FORT does not restrict types but applies additional axiomatization on the relata of the relation. For BFO, as discussed in section 3, constitution is not regarded.
In this section, we associate the theory with another logical language; a CLIF-serialization
as a Common Logic (CL) [
CL, which is an extension of KIF (Knowledge Interchange Format), is a logical language based on FOL, with the purpose of standardizing syntax (e.g. “CLIF”; the Common Logic Interchange Format) and semantics for information interchange and transmission. CL is used in ontological theories as a formal language tool to prove the consistency of a theory by validating the existence of model(s) M for a theory T. For example, BFO 1 and some of DOLCE’s modules 2 are encoded in CLIF. In addition to FOs, an open-access repository of first-order theories “ Colore” is implemented as CL-ontology modules 3 such as mereology.
Considering that FORT is a group of interlinked ontology modules that imports and reuses some extant theories from the literature, firstly we import those that are already encoded and available online at the “Colore” repository. These are; the CEM mereological theory4, the MT mereotopological theory along with the basic connection topological theory5, Varzi’s Location theory6, and their corresponding definitions. We modified some files e.g. the mereological definitions file to account for additional definitions e.g. overcross, undecross, etc, the location root file to remove region axioms, etc.
Secondly, we initiate the serialization of FORT’s micro-theories in the sense of ”what-comesifr st?” i.e. starting by the basic primitive relations that do not necessitate the use of other primitives, and passing to relations that import other relations in their modules. The full CL formalization of the theory is available online on GitHub repository; FORT.
In the process of encoding the CL ontology of FORT, we face some limitations in the language’s syntax. In the following, we identify the issue, locate it in the theory, and propose a solution to dealing with it.
What is the issue? Since FORT is an entity-type free theory, then it’s FOL formalization 1https://github.com/BFO-ontology/BFO-2020/tree/master/21838-2/common-logic 2https://github.com/gruninger/colore/tree/master/ontologies 3https://github.com/gruninger/colore/tree/master/ontologies 4https://raw.githubusercontent.com/gruninger/colore/master/ontologies/mereology/cem_mereology.clif 5https://raw.githubusercontent.com/gruninger/colore/master/ontologies/combined_mereotopology/mt.clif 6https://raw.githubusercontent.com/gruninger/colore/master/ontologies/location_varzi/L_location.clif comprises mostly variables quantifying over binary predicates (aka relations) without defining unary ones that represent entity types. However, in cases where restrictions on relata types are crucial for the characterization of a relation, we have used unary predicates (e.g. Ψ, Φ, ) that resemble entity types. More precisely, these are functions that quantify over a list of entity types that the modeler or the user in application would have. As expressed earlier, the practice of FORT is intended as a relation theory to be imported within the user’s application (which is a complete model of concepts and relations) to add semantics and rule constraints. This strategy of dealing with unary predicates that range over a finite set of universals is inline with that proposed by the Common Logic working group 7, and followed by DOLCE, as follows: ∃(()) corresponds to ⋁Φ∈Π(Φ()) and ∀(()) corresponds to ⋀Φ∈Π(Φ()) where Π refers to the ifnite list of concept names in the ontology. According to such a treatment, it is possible to express existential and universal quantification on universals in DOLCE. However, FORT does not provide a hierarchy of concepts, thus asserting ranging predicates on a set of universals Π is not possible. The same issue also applies on quantifying over binary predicates that resemble relations.
Where is the issue located in FORT? We track this issue by identifying the definitions and axioms in FORT that use such a quantification over unary/binary predicate names. These are: (a) the use of a universal quantifier on concepts in the generic existential dependence relation, and (b) the use of existential quantifiers on the unifying relations in the definition of a unified entity.
How can the issue be resolved? We elucidate a possible strategy to resolve this issue. If we quantify over unary/binary predicate names in CLIF serializations, the syntax will be violated. If we withdraw the usage of these predicates as ranging over finite sets, the expressive power of some relations in FORT drops. The most suitable strategy is to consider these predicates (Ψ, Φ, , ) as functions that themselves range over unary and binary predicates and do not need quantification. In other words; the usage of () shall correspond to a definition of as () = ∃Φ(Φ ∈ Π ∧ (Φ())) in which in practice will be encoded as () = 1() ∨ 2() ∨ ... ∨ () where each of () will correspond to a category in the user’s model. Similarly for role names, the usage of () shall correspond to the union of all unifying relations, thus can be considered as the parent of all unification relations. The sole drawback of this solution is that it adds to modelers the efort of adding some definitions to their models to maintain the validity and consistency of the theory, while achieving the intended expressive power. The sole diference in comparison to DOLCE’s strategy lies in the finite set Π where DOLCE restricts the elements of its set to its defined category types, while FORT ofers the possibility for the user to specify the user-categories that the predicates will range over.
Besides a CLIF serialization, we performed an automatic translation of FORT into the LADR syntax of Prover9 which is the format required by Prover9 and Mace4, and to the TPTP format, to ofer multiple serializations of CL. For this translation, several tools exist such as the CLtools repository 8, which has been previously adopted by 9 for a theory’s translation to Ladr syntax. However, no maintenance of the tool or resolving of its issues has been carried out in the last decade. Another tool is the macleod program 10 which consists of python scripts that can; translate a CLIF file to tptp and ladr formats; extract an OWL approximation of a clif ontology/module; verify the logical consistency of a clif ontology; verify the non-trivial logical consistency of a CLIF ontology; and prove theorems/lemmas that encode intended consequences of an ontology or module. So, we adopted the macleod program, in which we had to modify some configuration files and adapt some scripts, to build TPTP and Prover9 translations for each ontology module.
As for running consistency checks, we used the ”darwin11” consistency checker in “The
Heterogeneous tools set” [
In this paper, we have illustrated our previous work on FORT [
For our future work, we plan to the next steps of the methodology; a decidable knowledge representation language formalization that supports reasoning services i.e a DL-SROIQ formalization; and an OWL2-DL lite implementation of FORT. Such an approach is in line with some approaches in the Semantic Web community which advocate that re-usability is enhanced by eliminating domain/range constraints. Providing such an OWL ontology of relations (FORTontology) serves as an ontological tool ofering a language of primitive relations and rules, and enhances and facilitates ontology-driven conceptual modeling tasks.
8https://github.com/cmungall/cltools 9http://www.cs.toronto.edu/ torsten/DCT-BCont/ 10https://github.com/thahmann/macleod 11http://combination.cs.uiowa.edu/Darwin/ 12Hets is a parsing, static analysis and proof management tool incorporating various provers and diferent specification languages. It can be used either in its web-based interface http://rest.hets.eu/or installed it in a Docker container following the instructions http://hets.eu/
( , ) → A . 1 Φ , ) ∧ ( , ) ∧ ¬ ∃ ( , , ) ( , ) ∧ ( , ) → ( , ) ( , ) ∧ , , ) ( , ) ∧ ( , ) ∧ ( , ) ) ) ) ( ∀ ) ( , ) ( ∀ , , ) ( ( , ) ∧ ( , ) → ( , ) ) ) ( ( , ) → ( , ) ) ) ( ( , ) ( ( , ) ( ( , ∧ ∧ ∧ ( , ( , ( , ) ) ) → → ( , ( , ) ) ) ) → ( , ) ) ) ( ( , ) ∧ ) ∧ ) ( ∀ ) ¬ ( , ) ( ∀
, ( ∀
, ( ∀
, ( ∀ , ) ) ) ) ( , ( , ( , ( , ( ∀ ) ¬ ( , ) ( ∀
, ( ∀
, ( ∀ , ) ) ) ( , ( , ( , ) ) ) ) ) ) ) → → → = → → → ( ∀
, ( ∀
, ( ∀
, ( ∀
, ( ∀ , , , , , ∀ ( , ) ( , )
= ( ∀ , , ) ( ,
) ∀ ( ∃ ( ( ) ∧ A . 5 .
C o n s t i t u t i o
n ( ∀
, ( ∀
, ( ∀
, ( ∀
, ( ∀ ) ) ) ) ) ( , ( , ∧ ( ∀ ) ¬
( , ( ∀ , ) ( , ) ) ( ∀ , ,
) ( , ( ∀ , ) ( , ) ) = ( ( , ) ∧ , ( ( ∀ , , , ) ∧ ( ) ∧ ( ) ) → = ( M a