On the Formal Alignment of Foundational Ontologies: Building Mappings Between Basic Formal Ontology and Descriptive Ontology for Linguistic and Cognitive Engineering

Abstract

The development of an ontology-based ecosystem suitable for interoperability and for the reliable exchange of data and information is a longstanding goal of the applied ontology community. The construction of such a system relies on the alignment of a variety of ontologies. The alignment can be vertical, that is, across systems in different ontological layers (foundational, reference and domain) or horizontal, that is, across systems within a single layer. While techniques for vertical and horizontal alignments among reference and domain ontologies have been continuously studied for more than 15 years; the development of techniques for the alignment of foundational ontologies and across foundational and reference ontologies has been scattered or hardly addressed. This paper aims to bring attention to this latter problem in several ways: Highlighting the motivations for the alignment across foundational ontologies; presenting a methodology to develop such alignments; implementing the methodology to the case of the ontologies Basic Formal Ontology and Descriptive Ontology for Linguistic and Cognitive Engineering; and showing how an alignment deepens our understanding of such systems. The paper discusses also some alternative types of alignments, and briefly compares advantages and difficulties.

Keywords

ontology Basic Formal Ontology Descriptive Ontology for Linguistic and Cognitive Engineering ontology mappings

1. Introduction

In the 1980s the continuous improvement of storage and computational capacities made evident that interoperability across an increasing number of data and systems was becoming a fundamental problem in information science. In the early 1990s the research community started to focus on the hidden assumptions behind the generation and collection of data and the construction of information systems at large and, in a few years, this turned into a visionary research line, soon called applied ontology, that quickly became ‘the’ approach to solve interoperability problems. The roots of interoperability barriers were not yet clear but the growing availability and potentiality of large datasets, varying in both organisation and quality, drove attention to what one means by interoperability and how it could be achieved (Gardner, 2005; Ouksel & Sheth, 1999). A first source of problems, as it became clear later, was the lack of conceptual clarity and coherence in the internal organisation of datastores. Relational databases are powerful and successful tools but have important limitations (in particular when dealing with heterogeneous data) due to their rigidity and structural complexity. A second source of problems was the lack of a consistent methodology to merge databases and, more generally, to cope with the different structures of information systems. The fact that data were collected from different sources (each following its own purposes) using different approaches (relying on often implicit assumptions) hampered any attempt to develop such a methodology, and information sharing across data storage remained a problem.

The applied ontology vision relied on two tenets: (i) exploitation of formal semantics, and (ii) transparency of the assumptions. It followed that the process of data integration should be analysed at different levels: Syntactic, semantic, conceptual and structural. The focus on the semantics of data and on the conceptualisation of data organisation has brought a sharp change of perspective, and led to studying how to make explicit the viewpoint one takes on reality. In the following ten years, the idea that one has to make explicit the assumptions behind data collection and data management became popular, even though how to do it remained unclear (Ouksel & Sheth, 1999).

By focussing on semantics and hidden assumptions, applied ontology made possible to develop methodologies for data integration and systems’ interoperability. The idea was to study interoperability problems by separating interoperability levels, and to use formal logic to uncover semantic inconsistencies, and philosophical analysis to uncover conceptual inconsistencies. These distinctions allowed the clarification of the implicit choices on which a system or dataset relies, and to use logical and philosophical analyses to identify possible mismatches across systems. The next step was to harvest logical approaches to develop an alignment methodology among different semantic frameworks, and similarly to harvest philosophical approaches for an alignment methodology among different conceptual frameworks. This procedure gives, as one would expect, a general methodology whose outcome is a mapping across the systems at stake; mapping which is reliable both at the semantic and conceptual levels, and that explicitly shows the compatibility extension of those systems. This approach suggested that datasets and information systems should be shared together with their semantic and conceptual frameworks, now known as their ontology. Each system, augmented with its (explicitly documented) ontology, was then considered transparent and suitable for interoperability, if not for full integration. Admittedly, systems may rely on incompatible semantic or conceptual choices, the alignments one can find in such cases may be only partial. This, one would have argued, is the cost of the pluralistic approach in modelling. The community, with only limited exceptions, accepted this cost as needed to practically verify which modelling approaches were optimal and for which purposes.

Today we have a set of general methodologies (Euzenat & Shvaiko, 2013; Fernández-López et al., 1997; Jarrar & Meersman, 2009; Suárez-Figueroa et al., 2012) that help to develop and align datasets and information systems. While these approaches need time to be consolidated, they leave open the problem of aligning the most general ontologies, called foundational or top-level, aimed to be broadly applicable. How interoperability may work at this level is still unclear, mainly because of the complexity of these systems. Early works include a comparative study of Basic Formal Ontology (bfo), Descriptive Ontology for Linguistic and Cognitive Engineering (dolce) and Object-Centered High-level Reference Ontology (ochre), with an alignment of ochre to dolce (Masolo et al., 2003). Unfortunately, this study uses an ad hoc approach and does not provide a systemic view. So far no general methodology has been investigated and no systematic study has been carried out.

The present paper is part of a larger effort to build an ontology ecosystem as described by the visionary OntoCommons European project.¹ Motivated by this line of research, the paper proposes an approach to align top-level formal ontologies and presents problems, advantages and limitations as elicited in the study of the alignment of two well-known systems, namely dolce (Borgo et al., 2022a) and bfo (Arp et al., 2015; Otte et al., 2022; Smith et al., 2020). The main purpose is to identify and investigate the kind of problems, and possible solutions, that emerge in the alignment of foundational ontologies. The hope is that the collection and study of these cases can highlight the specificity of these issues and their relevance to understand ontology interoperability at this level. Furthermore, it is hoped that practical experiences like this can lead to developinging a shared and general methodology for the alignment of top-level ontologies.

The view underlying the work in this paper is known as ‘ontological pluralism’. It claims that science needs to remain open to different views, that is, to ontologies representing different conceptualisations of the world, and thus should allow the coexistence of possibly mutually inconsistent models.² Inconsistency can be at the conceptual as well as at the formal level. Interoperability across mutually inconsistent ontologies is obtained by (possibly partial) alignments via formal mappings. The OntoCommons ontology ecosystem is essentially a network of interconnected domain, reference and foundational ontologies, which is being built starting from an initial set of ontologies and a number of guidelines. The alignment presented in this paper is one of the results achieved by the project. The alignment (and underpinning conceptual and technical choices) is based on the first-order logic (FOL) versions of these ontologies. The $bfo$ - $dolce$ mapping applies to the most recent versions of these two ontologies in the CLIF language of Common Logic (CL), an ISO standard³, as submitted by the groups that developed these ontologies, see Section 2 for more details. The choice to use CL is the result of several considerations including that the use of CL is fairly consolidated in the research literature and in applications, and that the visibility and stability of standards can help to increase users’ trust in an ontology ecosystem and to foster its adoption and extension.

The aims of this paper are:

(i)
to report the theoretical and practical challenges one faces in aligning foundational large ontologies (these systems have more than 100 axioms);
(ii)
to highlight the most difficult and intertwined choices one might be confronted with during alignment processes;
(iii)
to discuss possible alignment strategies and their consequences on the alignment; and
(iv)
to provide an analysis of the main differences/similarities between $bfo$ and $dolce$ according to the obtained alignment.

The paper is structured as follows: Section 2 introduces the two ontologies and the notation. Section 3 describes the adopted methodology and the software used to support and check the alignment. Section 4 presents the alignment strategy and discusses the main categories that form the core of the two ontologies. The two following sections, Section 5 and Section 6, form the technical core of the paper: They present the formal alignment as two distinct mappings: From $dolce$ to $bfo$ and from $bfo$ to $dolce$ . Since the motivation of this work is the construction of an ontology ecosystem that includes also reference and domain ontologies, Section 7 adds some considerations on the possible use (and consequences) of the given alignments to support mappings across languages of the OWL family (W3C OWL Working Group, 2012). The last session, Section 8, summarises the results, discusses other open questions, and lists the next steps in this research line.
2. bfo and dolce

bfo and dolce are among the most well-known and used foundational ontologies. Several other foundational ontologies can be found in the literature, all developed within the last 20 years and each investigating different ontological choices (Borgo et al., 2022b). The decision to investigate the alignment between bfo and dolce is due to the choice made in the OntoCommons project which, in turn, has selected the two ontologies that have been developed earlier in this research area and that have influenced how applied ontologies are presented and discussed today. Note that, leaving aside terminological and other lightweight alignments, a formal comparison of bfo and dolce was partially investigated in 2003 (Masolo et al., 2003) and, more recently, a conceptual analysis has been proposed (Guarino, 2017). A brief historical view of the bfo and dolce ontologies is given next, an introduction of their formal approaches follows. For more information on the ontologies see (Borgo et al., 2022b; ISO 21838-2, 2021; ISO 21838-3, 2023).

$bfo$ is a top-level ontology, motivated by a realist philosophical position, intended to represent entities as described by science and designed to support information integration, retrieval, and analysis across all domains of scientific investigation. $bfo$ has been under development since around 2002 (Grenon et al., 2004) and serves as the top-level ontology of the Open Biological and Biomedical Ontology Foundry (OBO)⁴ and the Industrial Ontology Foundry⁵. $bfo$ has changed considerably over the years and today there are several versions available. The one considered in this paper is the $bfo$ presented in 2020 as part of the standard ISO 21838 (part 2) (ISO 21838-2, 2021). This version is axiomatised in CL (CLIF) (ISO 24707, 2007) and in the Web Ontology Language (OWL), as required by the standard.

$dolce$ is a top-level ontology, motivated by a cognitive view of reality, and designed to support sharing of data, information and knowledge across all domains. $dolce$ was developed in early 2000 as part of the European project ‘WonderWeb’⁶, published in the WonderWeb Deliverable 18 (Masolo et al., 2003), and is axiomatised in FOL extended with modalities, namely, the standard necessity and possibility operators. $dolce$ has been applied in a number of areas, in several European and international projects, and is also provided in application-oriented versions in OWL, in particular: $dolce$ -lite, $dolce$ -ultralite, and $dolce$ -zero. The ontology is consolidated as it has been only minimally changed over the years making it the most stable top-level ontology worldwide. The one considered in this paper is the $dolce$ presented in 2020 as part of the standard ISO 21838 (part 3) (ISO 21838-3, 2023). This version is axiomatised in CL (CLIF) (ISO 24707, 2007) and in the Web Ontology Language (OWL), as required by the standard.

2.1. bfo: CL Version (as of November 12, 2021)

We start from the logical theory bfo-cl consisting of all the axioms of BFO 2020 in CLIF, released on 12 November 2021 and accessible in GitHub⁷. The version we actually use in the alignment is labelled $B$ , is given in the syntax of Prover9 and presents four differences with respect to bfo-cl: (i) Inverse relations that can be found in bfo-cl (e.g., hasContinuantPart is the inverse of continuantPartOf) are not present in $B$ , and instead they are replaced by the original relation with arguments in reverse order (the temporal argument maintains its position); (ii) the ‘AtSomeTime’ and ‘AtAllTimes’ relations present in bfo-cl are never used in other axioms of bfo-cl and, for this reason, are not considered in $B$ ⁸; (iii) relations introduced in bfo-cl with ‘if and only if’ clauses are present in $B$ as syntactic definitions, that is, while in bfo-cl all these relations may be considered as ‘genuine’ additional predicates that are related with other predicates by a bi-conditional axiom, we consider these relations as ‘parametric macros’ that can be replaced by their definient, and have no impact on the interpretations of the theory (cfr. Section 3.1); and (iv) further syntactic definitions are added to improve the readability of some formulas.

To have more compact formulas, the bfo predicates have been shortened as shown in Table 1 (where the third column gives the original predicates in bfo-cl) and in Table 2. To avoid confusion, we indicate the bfo-predicates in $i t a l i c s$ while the dolce-predicates in $t y p e w r i t e r$ . The classes of particulars and universals are represented in bfo by unary predicates (and not by individual constants): We use $par$ for particulars and $uni$ for universals. The taxonomy of the $B$ particulars is depicted in Figure 1 (vertical lines represent ISA relationships, solid lines indicate a partition). All the universals in the taxonomy in Figure 1 are ‘rigid’ (in the sense that their instances cannot migrate over time to another universal) except for $o b j$ , $f o b j p$ , and $o b j a g g$ .

Figure 1.

Taxonomy of Basic Formal Ontology (bfo) (Vertical Lines Stand for ISA Relationships, Solid Lines Indicate a Partition).

Table 1.

Primitive Relations of bfo.

$x : :_{t} u$	$x$ is an instance of $u$ at time $t$	instanceOf
$EX (x, t)$	$x$ exists at time $t$	existsAt
$cP (x, y, t)$	$x$ is a continuant part of $y$ at time $t$	continuantPartOf
$oP (x, y)$	$x$ is an occurrent part of $y$	occurentPartOf
$mP (x, y)$	$x$ is a member part of $y$	memberPartOf
$tP (x, y)$	$x$ is a temporal part of $y$	temporalPartOf
$stREG (x, y)$	$x$ occupies spatiotemporal region $y$	occupiesSpatiotemporalRegion
$sREG (x, y, t)$	$x$ occupies spatial region $y$ at time $t$	occupiesSpatialRegion
$tREG (x, y)$	$x$ occupies temporal region $y$	occupiesTemporalRegion
$tPROJ (x, y)$	$x$ temporally projects onto $y$	temporallyProjectsOnto
$sPROJ (x, y, t)$	$x$ spatially projects onto $y$ at time $t$	spatiallyProjectsOnto
$OCCIN (x, y)$	$x$ occurs in $y$	occursIn
$LOC (x, y, t)$	$x$ is located in $y$ at time $t$	locatedIn
$SDEP (x, y)$	$x$ specifically depends on $y$	specificallyDependsOn
$CONCR (x, y)$	$x$ concretises $y$	concretises
$GDEP (x, y, t)$	$x$ generically depends on $y$ at time $t$	genericallyDependsOn
$PTC (x, y, t)$	$x$ participates in $y$ at time $t$	participatesIn
$REAL (x, y)$	$x$ realises $y$	realises
$HIST (x, y)$	$x$ is the history of $y$	historyOf
$PREC (x, y)$	$x$ precedes $y$	precedes
$FINST (x, y)$	$x$ is the first instant of $y$	firstInstantOf
$LINST (x, y)$	$x$ is the last instant of $y$	lastInstantOf
$MBAS (x, y, t)$	$x$ is the material basis of $y$ at time $t$	materialBasisOf

Table 2.

Categories of bfo.

$c f b n d$	Continuant Fiat Boundary	$q l t$	Quality
$c n t$	Continuant	$r q l t$	Relational Quality
$d i s p$	Disposition	$r l z e n$	Realisable Entity
$f l n$	Fiat Line	$r o l e$	Role
$f o b j p$	Fiat Object Part	$s d c n t$	Specifically Dependent Continuant
$f p t$	Fiat Point	$s i t e$	Site
$f s f$	Fiat Surface	$s r e g$	Spatial Region
$f n t$	Function	$s r e g 0$	0d Spatial Region
$g d c n t$	Generically Dependent Continuant	$s r e g 1$	1d Spatial Region
$h i s t$	History	$s r e g 2$	2d Spatial Region
$i d c n t$	Independent Continuant	$s r e g 3$	3d Spatial Region
$i m e n$	Immaterial Entity	$t r e g$	Temporal Region
$m t e n$	Material Entity	$t r e g 0$	0d Temporal Region
$o b j$	Object	$t r e g 1$	1d Temporal Region
$o b j a g g$	Object Aggregate	$s t r e g$	Spatiotemporal Region
$o c c$	Occurrent	$t i n s t$	Temporal Instant
$p b n d$	Process Boundary	$t i n t$	Temporal Interval
$p r o c$	Process

The axioms considered in $B$ – with the exception of the ones forcing the rigidity of the $bfo$ -categories and the taxonomical constraints depicted in Figure 1 – are reported in Appendix where the third column indicates the label originally adopted in $bfo$ to refer to the axiom.⁹ The syntactic definitions (d $_{b}$ 1)-(d $_{b}$ 8) will be used along the paper (notation: ‘ $ϕ := ψ$ ’ stands for ‘ $ϕ$ is syntactically defined by $ψ$ ’ and ‘ $x : :_{t} y$ ’ for ‘ at time $t$ , $x$ is an instance of $y$ ’, see Section 4.1).

2.2. dolce: CL Version

We write $D$ for the logical theory consisting of all the axioms in the CL-version of dolce (see Appendix).¹⁰ With respect to the original version of dolce introduced in Masolo et al. (2003), from now on called dolce-d18, $D$ presents two main differences following the dolce-iso version:

(1)
Modality operators are not used as they are not part of the language of CL (since dolce-d18 is a first order modal theory relying on the modal logic QS5 with constant domain, the lack of modal operators in $D$ changes the intended models of dolce);
(2)
The mereological fusion operator (operator $σ$ in dolce-d18) is not available in the language of CL (for each property expressible in the system, dolce-d18 enforces the existence of the mereological sum of all the entities that satisfy that property; this cannot be ensured in $D$ due to the lack of the fusion operator.)
The first simplification weakens several notions of dependence which are strongly grounded on modality. To partially overcome this difference, $D$ has the additional primitive of temporary existential dependence ( $E X D$ ) which, however, compensates only in part the lack of modal operators.

Concerning the second simplification, $D$ is based on extensional mereologies, rather than general extensional mereologies assumed in $dolce - d 18$ . Note that $D$ does not enforce the closure of the domain under (binary) sum and product. It is left to the user to add sum and product operators depending on modelling needs. Additionally, some notions that in dolce-d18 are defined via the mereological fusion operator, are introduced in $D$ as primitives. In particular, in $D$ we have the temporal relation $T L C (x, t)$ , read as ‘ $x$ is (exactly) located at time $t$ ’, and the temporary spatial relation $S L C (x, s, t)$ , ‘at time $t$ , $x$ is (exactly) located at space $s$ ’.

Two additional simplifications, with respect to $dolce - d 18$ , are adopted in $D$ (again following dolce-iso): –
only direct qualities are considered ( $D Q T$ );
–
the one-to-one link between quality types (e.g., temporal location, colour location) and quality spaces (e.g., time interval, colour region) assumed in dolce-d18¹¹ is not enforced anymore. The same quality kind can be linked to several quality spaces, a given colour location can be located in an RGB colour-space, a colour spindle space, etc.
Table 3 lists the primitive relations of $D$ , Table 4 lists the categories of $D$ , and Figure 2 shows the taxonomy of $D$ (vertical lines stand for ISA relationships, solid lines indicate a partition).

Table 3.
Primitive Relations of dolce.

$D Q T (x, y)$ $x$ is a direct quality of $y$

$E X D (x, y, t)$ $x$ is existentially dependent on $y$ at time $t$

$K (x, y, t)$ $x$ constitutes $y$ at time $t$

$P (x, y)$ $x$ is part of $y$

$P C (x, y, t)$ $x$ participates in $y$ at time $t$

$Q L (x, y)$ $x$ is the immediate quale of $y$

$S L C (x, y, t)$ $x$ is (exactly) located at space $y$ at time $t$

$T L C (x, t)$ $x$ is (exactly) located at time $t$

$t P (x, y, t)$ $x$ is part of $y$ at time $t$

$t Q L (x, y, t)$ $x$ is the temporary quale of $y$ at time $t$

Figure 2.
Taxonomy of Descriptive Ontology for Linguistic and Cognitive Engineering (dolce) (Vertical Lines Stand for ISA Relationships, Solid Lines Indicate a Partition).

Table 4.
Categories of dolce.

$ab$ Abstract $ped$ Physical Endurant

$acc$ Accomplishment $pob$ Physical Object

$ach$ Achievement $pq$ Physical Quality

$apo$ Agentive Physical Object $pr$ Physical Region

$aq$ Abstract Quality $pro$ Process

$ar$ Abstract Region $q$ Quality

$as$ Arbitrary Sum $r$ Region

$aso$ Agentive Social Object $s$ Space Region

$ed$ Endurant $sag$ Social Agent

$ev$ Event $sc$ Society

$f$ Feature $sob$ Social Object

$m$ Amount Of Matter $sl$ Spatial Location

$mob$ Mental Object $st$ State

$napo$ Non-agentive Physical Object $stv$ Stative

$naso$ Non-agentive Social Object $t$ Time Interval

$nped$ Non-physical Endurant $tq$ Temporal Quality

$npob$ Non-physical Object $tl$ Temporal Location

$pd$ Perdurant $tr$ Temporal Region

The axioms considered in $D$ – with the exception of the ones concerning the taxonomical constraints depicted in Figure 2 – are reported in Appendix. The syntactic definitions (d $_{d}$ 1)-(d $_{d}$ 7) will be used along the paper. When the context is clear, we will use $D$ and $dolce$ interchangeably.

2.3. Notation

In the paper we adopt the following notation to referencing formulas: (a $x$ ), (t $x$ ) and (d $x$ ), followed by an integer, identify axioms, theorems, and syntactic definitions, respectively, in the order in which they are listed in the theories. More specifically,

(a $_{b}$ $x$ ), (t $_{b}$ $x$ ), (d $_{b}$ $x$ ) are used for axioms, theorems, and definitions of $B$ (index $b$ stands for $bfo$ );

(a $_{d}$ $x$ ), (t $_{d}$ $x$ ), (d $_{d}$ $x$ ) are used for axioms, theorems, and definitions of $D$ (index $d$ stands for $dolce$ );

(d $_{db}$ $x$ ) are used for the mappings from $D$ to $B$ ;

(d $_{bd}$ $x$ ) are used for the mappings from $B$ to $D$ ;

(t $_{db}$ $x$ ) are used for theorems of the theory $D_{b}$ (an extension of $D$ that adds the mappings to $B$ , see Section 3.1 for an explanation of what is exactly meant with ‘extension’) that include some predicate of the mappings;

(t $_{bd}$ $x$ ) are used for theorems of the theory $B_{d}$ (an extension of $B$ that adds the mappings to $D$ , see Section 6.1 for a definition) that include some predicate of the mappings.

3. General Strategy and Role of Methodological Assumptions in Aligning TLOs

Before introducing the mappings and the difficulties we encountered, we provide the assumptions, strategy, and further considerations behind this work. These observations motivate the choices made in building the mappings and determine in which sense the result is correct.

The approach is centred on the CL-versions of the two ontologies. These, with their explanatory documentation, are taken as the primary sources of information on the ontologies and are considered in our strategy from the start. Here are the steps that characterise an alignment strategy¹²:

(S1)
analyse the CL-axioms together with the available documentation¹³ to ensure proper understanding of the overall ontologies and the intended interpretations of the primitives in each;
(S2)
establish and document the methodological choices;
(S3)
introduce formal mappings from one ontology to the other (and vice versa) with a description of what is covered;
(S4)
test (manual and with theorem provers) that the set of mappings is coherent and aligns what is intended;
(S5)
evaluate if the obtained set of mappings can be further generalised.

The strategy characterised by steps (S1)–(S5) is clearly underspecified. To become operative, one has to give the methodological choices which determine the kind of alignment sought (and how it can be verified). For instance, one may want to align the terminology, the primitives, the concepts, the inferences, the (intended) domains or even the whole models of the ontologies. This kind of choice leads to paying attention to some features of these systems, leaving aside others. Generally speaking, steps (S1)–(S5) may generate incompatible mappings when applied to preserve distinct features. In particular, one has to state what happens in case of inconsistencies across the available documentation. One may decide that the description in natural language is the most reliable of the authors’ intentions. Others may insist that the formal theory has priority since it is the only one that can be tested for consistency. Furthermore, the documentation might not be precise or detailed on aspects relevant for the alignment since the latter depends also on how the other ontology is developed. For instance, during the construction of the bfo and dolce alignment that we present in the next sections, the intended interpretation of some concepts was unclear to the alignment developers and clarifying questions were sent to the ontology authors to collect further information. This approach might not always be possible and, even so, it might not solve all cases (sometimes the authors of an ontology might not have a ready answer especially if the question raises foundational problems). In this paper, we keep bfo and dolce as is, that is, no extensions or modifications of the original ontologies have been considered to improve the mappings (even though some suggestions are proposed in Section 5.2 and Section 6.2). This is an important requirement in the context of the OntoCommons ontology ecosystem that contains several mid- and domain-levels ontologies already aligned with bfo and dolce.

Here are the assumptions adopted to align bfo and dolce. (M1)
Given an analysis of the documentation and the examples in the ontologies, any elicited informal correspondence across the notions of the two ontologies is assumed to provide a basis for a mapping of categories and relations of one ontology into the other. For instance, occurrents are described and used, in the bfo formal system and accompanying documentation, in a way that is conceptually similar to that of perdurants in the dolce formal system and documentation. This similarity is taken as an informal correspondence and leads to the consideration of the alignment of the bfo occurrent category to the dolce perdurant category. (Note that such a correspondence might be suggested by common examples in the two ontologies, or even be based on the comparison of relevant relations which are, perhaps for different reasons, considered similar like the bfo relation continuantPartOf and the dolce relation temporary parthood).
(M2)
A mapping aims to embed all (or most of) the members of a category of the source ontology (e.g., $D$ in the case of Section 5) in the domain of quantification of the target ontology ( $B$ in Section 5). In other terms, the purpose is to maximise the coverage of the entities of one ontology by the domain of the other ontology. Given this scenario, the study of which axioms of the target ontology hold or fail after the mappings from point (M1) are formalised, highlights genuine differences between the ontological commitments of the two ontologies (at least relatively to the CL language), and which entities of the source ontology are problematic in, or even incompatible with, the target ontology.
(M3)
Only direct mappings that can be formalised in FOL as syntactic definitions are considered, that is, a mapping is a FOL syntactic definition of a primitive of the target ontology in terms of the primitives of the source ontology. This choice allows us to use theorem provers to verify which axioms of the target ontology are preserved by the mappings. Meta-modelling techniques, like the application of abstraction processes or set-theoretical (second-order) constructions to enrich the domain of the source ontology with additional entities, are not considered. Analogously for embeddings of the target and source ontologies into richer ontologies that would serve as bridges between them, see (Chui & Grüninger, 2014). The analysis presented in this paper can be seen as a prerequisite to the application of these other techniques.

Note that the assumptions (M2) and (M3) are interrelated and are seen from the perspective of an interactive development of mappings that starts with the analytical step (M1). In particular, (M2) emphasises that the alignment is domain focussed in the sense that the goal is to maximise coverage of the entities of the source ontology by the domain of the target ontology.
3.1. General Observations From the Alignment of bfo and dolce

The alignment between large ontologies presents a formal and a conceptual challenge: The formal challenge consists of the identification and the verification of the mappings; the conceptual challenge refers to the choice among alternative mapping options. For instance, in Sections 5.2 and 6.2 we discuss some alternative mappings which have not been adopted in our alignment. These mappings modify (by restricting or expanding the mappings proposed in, respectively, Sections 5.1 and 6.1) the way some notions of the target ontology are modelled in terms of the ones of the source ontology. In particular, these alternative mappings present possible solutions (or improvements) to the partiality of the alignments developed in Sections 5 and 6. Furthermore, formal constructions (definitely more complex) can be implemented to extend the domain of the source ontology to resemble more closely the domain of the target ontology, facilitating a richer mapping across these systems. This result can be achieved also by allowing for the definition of primitives of the target ontology in the source ontology, via reference to newly introduced entities. This case is not specific to the alignment of bfo and dolce. It is a choice to consider when specialising an alignment strategy.

Assumption (M3) may be better understood if we compare two approaches to extend a theory via definitions. Recall that the goal is to have formulas in the source ontology that capture (or best approximate) the concepts in the target ontology. In this example, we take $D$ as the source ontology and $B$ as the target ontology. (Analogous considerations hold for the other direction.)

The first approach, which we adopt in this paper, is to extend theory $D$ with a set of syntactic definitions – the mappings in Section 5.1 –, which inject $B$ primitives into $D$ , that is, these definitions are introduced as a way to ‘understand’ the $B$ primitives in the dolce language. We use the symbol $:=$ for these syntactic definitions and treat them as ‘parametric macros’. That is, one can simply substitute at the syntactic level the definiens for the definendum. Note that these syntactic definitions have parameters which must be suitably matched. For instance, suppose we aim to define the primitive of parthood on occurrents in $B$ via formula $oP (x, y) := ϕ (x, y)$ . As we know, the lefthand side (namely, $oP (x, y)$ ) is a primitive in $B$ . Let us assume that $ϕ$ is an expression in the language of $D$ with $x$ and $y$ as the only free variables. In this case, $x$ and $y$ are treated as parameters and the formula $\forall z w (oP (z, w) \land oP (w, z) \to z = w)$ in the language of $B$ becomes formula $\forall z w (ϕ (z, w) \land ϕ (w, z) \to z = w)$ in the language of $D$ . Similarly, $B$ -formula $oP (p r o c # 1, p r o c # 2)$ becomes $D$ -formula $ϕ (p r o c # 1, p r o c # 2)$ .

The second approach consists in adding these definitions as new formulas in the source ontology, obtaining a definitional extension of the source theory. It suffices to turn our syntactic definitions into biconditionals rather than syntactic definitions as described above. Syntactically, this means to use the symbol $\leftrightarrow$ (if and only if) instead of the $:=$ symbol, and to close the expression by adding universal quantifiers for all the free variables. For example, in the previous example one would add the entire formula $\forall x y (oP (x, y) \leftrightarrow ϕ (x, y))$ directly into the source theory. The advantage of using syntactic definitions instead of extensions by definitions is that the vocabulary of the theory in which we introduce the syntactic definition does not change. Using the ‘if and only if’ clause automatically adds the defined predicates to the ontology language (e.g., we would add the $bfo$ -predicate $oP$ into the $dolce$ vocabulary when using the biconditional in the previous example). In Section 4.1 we will see a case where the latter approach adds new ontological commitments into the theory with important consequences on the view of universals.

Once $D$ has been extended with these syntactic definitions (and possibly further syntactic definitions already present in $B$ ) – we dub $D_{b}$ such extension – it is possible to check how much of the theory $B$ is preserved: Each axiom in $B$ expressible¹⁴ in $D_{b}$ is proved or disproved in $D_{b}$ . The analysis in Section 5.2 of the preserved/non-preserved axioms allows, modulo the introduced mapping, to highlight and understand similarities and divergences between the two ontologies. The mapping in the other direction, that is, the extension $B_{d}$ with the syntactic definitions of $dolce$ -primitives in terms of $bfo$ -primitives, is formalised in Section 6. The combined analysis of the mappings dolce-into-bfo and bfo-into-dolce points out genuine ontological differences as well as problematic aspects of the adopted technique.

These observations hold beyond the bfo and dolce cases. Also, the general strategy can be iterated to further refine the mappings and possibly solve false cases of agreement and disagreement.

3.2. Use of Theorems Provers and Model Builders

The material presented in the next sections is tested using theorem provers, namely, Prover9¹⁵ and Vampire¹⁶. For the generation of models and countermodels, the software Mace4¹⁷ was used. According to the literature (Sutcliffe, 2016) and in our experience, Vampire is usually, but not always, faster than Prover9. The proofs produced by Prover9 are generally shorter and easier to read (not least because Prover9 offers the possibility of removing universal quantification from the start of formulas – Prover9 assumes by convention that any free variable in a formula is implicitly universally quantified). To take advantage of these differences, we used both theorem provers.

Our methodology is as follows. We rewrite all axioms and definitions of $D$ and $B$ in the syntax accepted by the software (Vampire accepts tptp (Sutcliffe, 2016), Prover9 uses its own syntax). To prove a theorem regarding the mappings from dolce to bfo, we add to the tptp or Prover9-syntax version of dolce the encoding, in the appropriate syntax, of both the mappings in Section 5.1 and the formula to be proven (i.e., we rewrite the whole $D_{b}$ plus the formula to be proven). Then we submit this large theory to the prover and ask if the formula is a theorem in that theory, that is, if it follows from $D_{b}$ . We proceed similarly in the case of the mappings from bfo to dolce. The documentation provided in Appendix of Masolo et al. (2023) refers to these automatically generated proofs. When the provers do not find a proof of a statement, and this happens in several cases, we provide a manual proof. Some of the manually generated proofs are verified by at least one prover by adding intermediate lemmas (which are themselves automatically verified).

To formally verify counterexamples of relevant sentences, we produce a counterexample by hand and then proceed in the following way: We write axioms (in the prover syntax) enforcing the existence of the exact number of individual constants required by the counterexample, as well as each and every relation holding among them. For the sake of brevity, some of the relations are skipped by exploiting taxonomical axioms. That is, once we add the axioms of the $D$ (or $B$ ) taxonomy, it suffices to specify to which leaf-class each constant belongs: the constant will automatically belong to each superclass and not belong to disjoint classes, thanks to the ISA relationship axioms holding between the classes of the taxonomy. Additionally, the disjunction axioms between the taxonomical classes spare us from stating that individuals belonging to disjoint classes are different (non-identity among different individual constants belonging to the same class must be still forced through appropriate axioms). In this way, we obtain a theory that syntactically describes the domain and the relationships at the core of the counterexample, which is complete by construction. At this point, Mace4 is used with these axioms as input to verify that the given (small) set of axioms is consistent and to generate an explicit model. Then, for each axiom of $D$ (or $B$ ), we verify that it holds in the model, by asking the provers if the axiom follows from the axioms that specify the model, thus proving that the model is a model of $D$ ( $B$ ). Lastly, we check that in this model the sentence that we want to disprove is actually false.

Note that the standard way to generate counterexamples with Mace4, that is, by asking Mace4 to find a model of all the axioms of $D$ ( $B$ ) with the addition of the negation of the sentence to be disproved, does not work in most of the cases we encountered perhaps due to the complexity of these ontologies.

All the proofs and models relative to our alignments are collected in Masolo et al. (2023).

4. Preliminary Considerations

This section focuses on points specific to the alignment of bfo and dolce. This allows us to introduce two problems related to the technical choices made in these systems, and to discuss the different levels at which these theories investigate some ontological classes.

4.1. Representation of Categories

In $dolce$ the categories in Table 4 are represented by means of FOL unary predicates. These categories are disjoint and assumed to correspond to rigid properties: if an entity belongs to one of these categories, it must belong to that category from the time it starts to exist to the time it ceases to exist (if any). To state that an entity $x$ is an endurant, one formally writes $ed (x)$ . Similarly for the other categories.

In $bfo$ , all the universals in Table 2 are in the domain of quantification and a temporary instance-of primitive relation (written $: :_{}$ ) is introduced to represent when an individual is an instance of a universal at a given time. For instance, the fact that ‘at time $t$ , $x$ is a continuant’ is formally written $x : :_{t} c n t$ , where $c n t$ corresponds to the universal being a continuant. bfo universals are non-empty and rigid through time with the exception of $o b j$ , $o b j a g g$ , and $f o b j p$ . For instance, a material entity could belong to $o b j$ at some time, and later to $o b j a g g$ (or $f o b j p$ ) and, perhaps, change again later, provided at each point in time it is classified by one and only one of these three universals.

These different representational choices raise an initial problem because, according to (M3), one should individuate to which kind of dolce entities the bfo universals correspond (Section 5.2 adds further considerations on this point). We consider only the $bfo$ -universals present in the taxonomy, and start from the subset that can be defined in $dolce$ . For each universal $u$ , a syntactic definition of form $x : :_{t} u := ϕ (x, t)$ is introduced. Note that here the ‘parameters’ are $x$ and $t$ , while $u$ is a constant. This means that, first, we do not define the notion of instance-of but define only the instantiation of a given $u$ . That is, in general, the definitions of $x : :_{t} u_{1}$ and $x : :_{t} u_{2}$ could be different. Second, as discussed earlier, $u$ will not appear in $ϕ (x, t)$ and thus will not become an individual in the domain of $dolce$ . If we were to use the biconditional conditions, writing $x : :_{t} u \leftrightarrow ϕ (x, t)$ in the theory, both the predicate $: :_{}$ and the individual constant $u$ would be added to the vocabulary of $dolce$ , and this would imply having some universal in the domain of $dolce$ .

A way to avoid this problem is to substitute $U (x, t) := ϕ (x, t)$ for $x : :_{t} u \leftrightarrow ϕ (x, t)$ , that is, to map the needed bfo categories to dolce predicates, and the instance-of relation to (logical) predication. We adopt the first strategy because it is closer to the formalisation in $B$ , and it avoids including universals in the domain of $dolce$ as well as the relation instance-of among the primitives of $dolce$ .

In this perspective, $bfo$ axioms quantifying over universals are disregarded by the mappings. Weaker versions of these axioms are introduced by considering the (finite) set ${u_{1}, \dots, u_{n}}$ of those universals explicitly used to generate the mappings. For instance, $\exists x t (x : :_{t} u_{1}) \land \dots \land \exists x t (x : :_{t} u_{n})$ can replace the axiom (a $_{b}$ 6).

4.2. Different Ontological Focus and Resolution

The informal presentations of bfo occurrents and dolce perdurants are very close. This observation is further supported by the fact that both the ontologies introduce a primitive of parthood simpliciter for these entities (relation $P$ in $dolce$ and $oP$ in $bfo$ ). Analogously, we notice a similarity between bfo continuants and dolce endurants, given that both ontologies conceive the temporary parthood relation as a primitive ( $t P$ in $dolce$ and $cP$ in $bfo$ ). Things are different for temporal/spatial regions and qualities. At first sight, these categories appear to be similar. Formally, they are classified in different ways in the two ontologies. $bfo$ classifies qualities (and, more generally, specific dependent continuants) and spatial regions under continuants while temporal regions are classified under occurrents. In $dolce$ , temporal regions, spatial regions, and qualities are neither endurants nor perdurants.¹⁸ In particular, temporal regions and spatial regions are abstract entities in $dolce$ . This difference – mainly grounded on the way the distinction between endurants/continuants and perdurants/occurents is characterised – complicates the comparison and needs to be taken into account in defining the mappings (this can be seen, for instance, in the case of the definition (d $_{db}$ 1) in $D_{b}$ relative to the primitive $EX$ of $B$ ).

How the most general categories (endurants/continuants on the one hand, perdurants/occurrents on the other hand) are specialised diverges considerably in the two ontologies:

On perdurants vs. occurrents

In dolce perdurants are specialised mainly on the basis of two notions, both extensively discussed in the linguistic and philosophical literature: Homeomericity (roughly, any temporal part of a perdurant of a certain kind is a perdurant of the same kind) and cumulativity (roughly, the mereological sum of perdurants of a certain kind is a perdurant also of the same kind); in bfo processes are distinguished from process boundaries mainly based on the dimensionality of their temporal locations and on the fact that they are temporal proper parts of other occurrents.

On endurants vs. continuants

The spatial and material dimensions of these kinds of entities play a central role in both dolce and bfo (see Section 5.2 for their differences). dolce presents a finer taxonomy mainly aimed to cover the notions of agentivity and sociality. bfo, which is driven by the distinction between fiat vs. bona fide entities, explicitly introduces the notion of aggregate, and relies on the dimensionality of the spatial (rather than temporal) location to distinguish sites vs. continuant fiat boundaries.

On qualities

The branch of the taxonomy for qualities in dolce is detached from that of endurants and continuants, differently from bfo, and is motivated by the comparability principle: It makes sense to compare the colour of a rose and the colour of a vase, while it does not make sense to compare the colour of a rose and the weight of a vase. Qualities are clustered in terms of maximal comparability, for example, colours, weights, lengths, shapes, etc. form different quality types. Spaces of regions have a structure and are associated accordingly, for example, for colours, the space has regions for red, blue, green, etc. Instead, bfo distinguishes classes of specifically dependent continuants according to the existence, the nature of, and the participants in their realisation processes. These different ways of classifying entities are not incompatible per se. For instance, one could consider cumulativity, agentivity, comparability in bfo, and dimensionality of temporal/spatial regions and realisation processes in dolce. But, clearly, this approach requires extending bfo and dolce, a choice that should be pondered carefully. The alignment strategy based on ontology extension is not exploited in the work we present here. The consequence is that some primitive notions and categories of the target ontology cannot be defined in terms of those in the source ontology.

5. The Mapping From dolce to bfo

This section presents the technical results of the establishment of a mapping from dolce to bfo, that is, it shows how to define in $dolce$ the categories and primitive relations of $bfo$ . As anticipated, the mapping does not cover all categories and relations.¹⁹ In other terms, the starting point is the domain of dolce, and the goal is to classify and relate the entities of this domain in terms of the categories and relations of bfo.

The first part of the section, Section 5.1, reports the elements covered by the mapping and the conceptual motivations for its limitations. This part makes technically clear the theoretical and formal barriers to completing the coverage of the ontology in the kind of mapping that our general strategy and related assumptions can generate. At the end, we list the primitive relations and the categories of $bfo$ which are covered by the mappings with the corresponding syntactic definitions in $dolce$ . Next, we verify whether the axioms of $bfo$ hold in $dolce$ when extended with the given syntactic definitions.

The second part, Section 5.2, provides an analysis of the achieved results, the limitations and possible alternative strategies.

5.1. The Definitions of bfo Primitives in the Language of dolce

According to our previous discussion and point (M3) of Section 3, our goal is to introduce syntactic definitions of $bfo$ primitives in terms of $dolce$ primitives.

First of all, $D$ lacks the language to refer to the dimensionality of the instances of a given category. This implies that these distinctions cannot be modelled in this theory, thus:

(i)
the subcategories of $s r e g$ and of $c f b n d$ cannot be distinguished;
(ii)
the distinction between $s i t e$ and $c f b n d$ cannot be introduced (sites are three-dimensional while continuant fiat boundaries are two-, one-, or zero-dimensional);
(iii)
the distinction between $t i n t$ and $t i n s t$ cannot be fully characterised.

Concerning (ii) we introduce a definition only for the disjunction of $s i t e$ and $c f b n d$ (written $s i t e \cup c f b n d$ ), see (d $_{db}$ 12). $s i t e \cup c f b n d$ is clearly not among the categories in the bfo taxonomy and it might not be acceptable as a bfo universal. It is used in the mapping with a technical role: $x : :_{t} s i t e \cup c f b n d$ is a shortcut for $x : :_{t} s i t e \lor x : :_{t} c f b n d$ . Concerning (iii) we identify temporal instants (intervals) with $D$ atomic (non-atomic) time intervals, see (d $_{db}$ 9) and (d $_{db}$ 10). Admittedly, this is a very rough characterisation. First, temporal atoms can have the same dimensionality of the times they are part of. Second, in bfo the finite sum of (distinct) zero-dimensional temporal regions is still zero-dimensional while the sum of (distinct) atomic times is always not atomic, that is, according to (d $_{db}$ 9) and (d $_{db}$ 10), it is an interval. Third, bfo time intervals are convex while dolce non-atomic time intervals are not necessarily convex. Thus, (d $_{db}$ 10) seems to approximate the category $t r e g 1$ better than $t i n t$ . At the same time, if all the non-atomic entities are instances of $t r e g 1$ , then $t r e g 0$ and $t i n s t$ collapse. For these reasons, we omit $t r e g 1$ and $t r e g 0$ and consider only the rough definitions of $t i n s t$ and $t i n t$ . Note that, in bfo, the convexity of intervals is characterised by means of the primitive of precedence ( $PREC$ ). To define $PREC$ in dolce one should extend the theory with an order relation defined on time intervals. Similarly for $FINST$ (firstInstantOf) and $LINST$ (lastInstantOf). It follows that the mapping does not cover the relations $PREC$ , $FINST$ , and $LINST$ .

As anticipated earlier, see also assumption (M1) in Section 3, the category of specifically dependent continuants ( $s d c n t$ ) seems to correspond to the dolce category of qualities. However, as observed in Section 4.2, bfo and dolce distinguish the subclasses of these categories based on different criteria. In bfo, the subcategories of $s d c n t$ are mainly characterised by means of the primitives $REAL$ (realises) and $MBAS$ (materialBasisOf) for which, however, a complete characterisation is missing.²⁰ As a consequence, $REAL$ , $MBAS$ , and the subcategories of $s d c n t$ are not covered by the mapping.

A similar situation holds for the subcategories of material entities ( $m t e n$ ). In particular, object aggregates are intimately connected to the $mP$ (memberPartOf) primitive. None of these notions can be defined without an extension of dolce. It follows that also $mP$ and the subcategories of $m t e n$ are not covered by the mapping.

Other cases are more subtle. The primitive $HIST$ (historyOf) seems to be naturally defined in $D$ by:
$HIST (x, y) := \forall z (P (z, x) \leftrightarrow \forall t (P R E (z, t) \to P C (y, z, t)))$
However the effectiveness of this definition depends on the existential assumptions on perdurants. For instance, assume that $y$ participates only in some perdurant $p$ and only for some time at the beginning of $p$ , and, moreover, that there is no perdurant which is proper part of $p$ , in particular there is no ‘beginning’ of $p$ (this can happen because dolce does not commit to the existence of all the temporal slices of a perdurant). Then $y$ would not have a history, since the only candidate to be the $x$ in the definition would be $p$ , for which the definient is false (if $x = p = z$ , then there is a time, say the end of $p$ , where $p$ is present but $y$ does not participate in $p$ ). These technical difficulties, and the fact that histories seem to have a marginal role in the bfo ontology, suggest leaving out also $HIST$ and $h i s t$ .

Spatiotemporal regions are compatible but not enforced in dolce. One could introduce them among the regions together with the corresponding qualities. The projections regulating the relationships with spatial and temporal regions (corresponding to the bfo $tPROJ$ and $sPROJ$ ) would also be necessary. Alternatively, violating (M3), spatiotemporal regions could be constructed (at the semantic level, for instance) as pairs $⟨$ time interval, space region $⟩$ . As we do not exploit constructive extensions, we do not consider them here even though, from the expressive power viewpoint, spatiotemporal regions seem not to change the language. This suggests that their introduction might be, at least technically, less controversial. More details on spatiotemporal regions can be found in Masolo et al. (2023).

The definition (d $_{db}$ 17) of $CONCR$ (and the ones of $g d c n t$ and $GDEP$ which are grounded on it) is just an approximation that introduces a clear link between $bfo$ concretisation and $dolce$ $E X D$ . In particular, while the first argument of the original concretisation can also be a process (see (a $_{b}$ 105) in the Appendix), (d $_{db}$ 17) contemplates only specifically dependent continuants. It is not clear to us (also because the $bfo$ documentation contains very few examples of generically dependent continuants concretised by processes) how processes can be taken into account starting from $dolce$ .

Finally, following the discussion in Section 4.1, instance-of ( $: :_{}$ ) is not directly defined. Instead, we define in $D$ the instantiation of the needed universals. We also define the primitive predicate $par$ and $uni$ of $bfo$ , introduced to distinguish particulars from universals, even though $uni$ turns out to be empty in $D$ (when at least a temporal interval exists, see (t $_{db}$ 2) in Section 5.2).

Summing up, among the bfo notions, in the following we introduce: (i)
syntactic definitions for the primitive predicates: $EX$ , $cP$ , $oP$ , $tP$ , $sREG$ , $tREG$ , $OCCIN$ , $LOC$ , $SDEP$ , $CONCR$ , $GDEP$ , $PTC$ , $par$ , $uni$ ; and
(ii)
syntactic definitions of form $x : :_{t} u$ for each category $u \in {c n t$ , $o c c$ , $i d c n t$ , $g d c n t$ , $s d c n t$ , $m t e n$ , $i m e n$ , $s i t e \cup c f b n d$ , $s r e g$ , $p r o c$ , $p b n d$ , $t r e g$ , $t i n s t$ , $t i n t}$ .

These syntactic definitions are given below together with a short informal description. (Once a definition has been introduced, it may be used only in definitions given later to avoid circularity.) A deeper analysis about these definitions and their impact on the preservation of the axioms of bfo is in Section 5.2. d $_{db}$ 1
$EX (x, t) := P R E (x, t) \lor (t (x) \land P (t, x)) \lor (ab (x) \land \neg t (x) \land t (t))$

$EX$ coincides with $P R E$ on $ed$ s, $pd$ s, and $q$ s ( $P R E$ is defined in (d $_{d}$ 6)). Time intervals $EX$ -exist at every subinterval of themselves while the other abstract entities $EX$ -exist at every time. This extension matches the fact that $EX$ is defined on both temporal regions and spatial regions (which seem very close to dolce time intervals and space regions, respectively, see (d $_{db}$ 7) and (d $_{db}$ 13)).
d $_{db}$ 2
$oP (x, y) := P (x, y) \land ((pd (x) \land pd (y)) \lor (t (x) \land t (y)))$

$oP$ is a restriction of $P$ (the latter applies also to $ab$ s). The definition preserves the fact that in bfo $oP$ is defined only on occurrents (that include temporal regions but not spatial regions).
d $_{db}$ 3
$tP (x, y) := oP (x, y) \land \forall z (oP (z, y) \land \forall t (EX (z, t) \to EX (x, t)) \to oP (z, x))$ ²¹

This is the classical definition of temporal part or slice, that is, $x$ is the maximal part of $y$ during the temporal extension of $x$ .
d $_{db}$ 4
$tREG (x, t) := pd (x) \land T L C (x, t)$

$tREG$ is the restriction of $T L C$ to $pd$ s (in dolce $T L C$ is defined for all the entities present in time, that is, also for $ed$ s and $q$ s).
d $_{db}$ 5
$x : :_{t} p b n d := pd (x) \land \exists y (tP (x, y) \land x \neq y) \land T L C (x, t) \land A T (t)$

A process boundary is a temporally atomic perdurant ( $A T$ is defined in (d $_{d}$ 2)), that is a temporal proper part of at least another perdurant. As said, the atomicity of the temporal location of a perdurant is an approximation of its instantaneity.
d $_{db}$ 6
$x : :_{t} p r o c := pd (x) \land P R E (x, t) \land \neg (x : :_{t} p b n d)$

Processes are perdurants that are not process boundaries (all the perdurants are present at some time (t $_{d}$ 1)).
d $_{db}$ 7
$x : :_{t} t r e g := t (x) \land EX (x, t)$

Temporal regions coincide with dolce time intervals.
d $_{db}$ 8
$x : :_{t} o c c := x : :_{t} p b n d \lor x : :_{t} p r o c \lor x : :_{t} t r e g$

As said, spatiotemporal regions are ruled out. An occurrent is any entity among process boundaries, processes and temporal regions (whose definitions are given above).
d $_{db}$ 9
$x : :_{t} t i n s t := x : :_{t} t r e g \land A T (x)$

Temporal instants are atomic time intervals.
d $_{db}$ 10
$x : :_{t} t i n t := x : :_{t} t r e g \land \neg A T (x)$

Temporal intervals are non-atomic time intervals (in bfo they are self-connected but this property cannot be defined in dolce).
d $_{db}$ 11
$x : :_{t} m t e n := ed (x) \land P R E (x, t) \land \exists u (P R E (x, u) \land \neg A T (u)) \land \forall u (P R E (x, u) \to \exists y s r ($ $m (y) \land S L C (x, s, u) \land S L C (y, r, u) \land P (r, s)))$

Material entities are non instantaneous (to match (a $_{b}$ 8) in Appendix) endurants that during their whole life are (at least partially) spatially co-localised with an amount of matter.
d $_{db}$ 12
$x : :_{t} (s i t e \cup c f b n d) := f (x) \land P R E (x, t) \land \exists s (S L C (x, s, t)) \land \forall u (P R E (x, u) \to \neg \exists y s r (m (y) \land S L C (x, s, u) \land S L C (y, r, u) \land P (r, s)))$

Both sites and continuant fiat boundaries are dolce features localised in space that during their whole life are never (partially) spatially co-localised with an amount of matter.
d $_{db}$ 13
$x : :_{t} s r e g := s (x) \land EX (x, t)$

Spatial regions coincide with dolce space regions.
d $_{db}$ 14
$x : :_{t} i m e n := x : :_{t} (s i t e \cup c f b n d) \lor x : :_{t} s r e g$
d $_{db}$ 15
$x : :_{t} i d c n t := x : :_{t} m t e n \lor x : :_{t} i m e n$
d $_{db}$ 16
$x : :_{t} s d c n t := q (x) \land P R E (x, t) \land \exists y (y : :_{t} i d c n t \land \neg s (y) \land D Q T (x, y))$

Specifically dependent continuants are dolce qualities inhering (in the sense of $D Q T$ ) in an independent continuant (as defined in (d $_{db}$ 15)) that is not a spatial region.
d $_{db}$ 17
$CONCR (x, y, t) := x : :_{t} s d c n t \land nped (y) \land \neg \exists s (S L C (y, s, t)) \land E X D (y, x, t)$

Concretisation is a form of dolce $E X D$ between a non-physical endurant $y$ that does not have a spatial localisation ( $S L C$ ) and a specifically dependent continuant (as defined in (d $_{db}$ 16)) $x$ .
d $_{db}$ 18
$x : :_{t} g d c n t := P R E (x, t) \land \forall u (P R E (x, u) \to \exists y (CONCR (y, x, u)))$

Generic dependent continuants are non-physical endurants (from (d $_{db}$ 17)) that are concretised during their whole life.
d $_{db}$ 19
$x : :_{t} c n t := x : :_{t} i d c n t \lor x : :_{t} s d c n t \lor x : :_{t} g d c n t$
d $_{db}$ 20
$cP (x, y, t) := x : :_{t} c n t \land y : :_{t} c n t \land (t P (x, y, t) \lor P (x, y) \lor \exists z u (D Q T (x, z) \land D Q T (y, u) \land t P (z, u, t)))$

According to (d $_{db}$ 15), (d $_{db}$ 16), (d $_{db}$ 18), and (d $_{db}$ 19), continuants include $ed$ s, $s$ s, and $q$ s. For $ed$ s, $cP$ coincides with $t P$ . For $s$ s, $cP$ coincides with $P$ . dolce does not define a parthood relation on $q$ s but it is defined on endurants. One can use the latter to infer a parthood relation on qualities (according to dolce each quality inheres in a single entity, $D Q T (x, y) \land D Q T (x, z) \to y = z$ ).²²
d $_{db}$ 21
$sREG (x, s, t) := x : :_{t} i d c n t \land \neg s (x) \land S L C (x, s, t)$

$sREG$ is the restriction of the $S L C$ to independent continuants (as defined in (d $_{db}$ 15)) that are not spatial regions.
d $_{db}$ 22
$PTC (x, y, t) := x : :_{t} c n t \land \neg s (x) \land y : :_{t} p r o c \land P C (x, y, t)$

$PTC$ (the $bfo$ participation) is the restriction of $P C$ (the $dolce$ participation) to continuants that are not spatial regions and to processes (as defined above).
d $_{db}$ 23
$OCCIN (x, y) := pd (x) \land \exists t (y : :_{t} m t e n \lor y : :_{t} s i t e \cup c f b n d) \land \forall t (P R E (x, t) \to \exists s r (S L C (x, s, t) \land S L C (y, r, t) \land P (s, r)))$

$OCCIN (x, y)$ holds when the spatial location of the perdurant $x$ is always included in the one of the material entity/site/continuant fiat boundary $y$ (this definition closely corresponds to the formal one provided in the documentation of bfo).
d $_{db}$ 24
$LOC (x, y, t) := x : :_{t} i d c n t \land \neg s (x) \land y : :_{t} i d c n t \land \neg s (y) \land \exists s r (S L C (x, s, t) \land S L C (y, r, t) \land P (s, r))$

At time $t$ , an independent continuant (that is not a space region) is located in another independent continuant (that is not a space region) when the spatial location (at $t$ ) of the first continuant is included in the spatial location (at $t$ ) of the second continuant (this definition closely corresponds to the formal one provided in the documentation of $bfo$ ).
d $_{db}$ 25
$SDEP (x, y) := x : :_{} s d c n t \land D Q T (x, y)$

$SDEP$ is the restriction of the direct quality $D Q T$ to specifically dependent continuants (as defined in (d $_{db}$ 16)).
d $_{db}$ 26
$GDEP (x, y, t) := x : :_{t} g d c n t \land y : :_{t} i d c n t \land \neg s (y) \land \exists z s (P (s, t) \land D Q T (z, y) \land CONCR (z, x, s))$

At time $t$ , the generic dependent continuant $x$ generically depends on the independent continuant (that is not a spatial region) $y$ , when it is concretised (during a part $s$ of $t$ ) by a specifically dependent continuant $z$ inhering in $y$ .
d $_{db}$ 27
$par (x) := \exists t (EX (x, t))$

Particulars are entities that $EX$ -exist in time (to match (a $_{b}$ 4) and (a $_{b}$ 7) in Appendix).
d $_{db}$ 28
$uni (x) := \neg par (x)$

Universals are non-particulars (to match (a $_{b}$ 1) and (a $_{b}$ 2) in Appendix).

$D_{b} = D \cup {$ (d $_{db}$ 1),…,(d $_{db}$ 28) $}$ indicates the theory $D$ extended with the definitions listed above.

As said, some bfo-axioms involve relations or categories that have not been defined in the mappings. When possible and relevant we considered approximations of these axioms as expressible in the dolce language, otherwise we set them aside. The first column in the tables in Appendix shows which axioms (or their approximations) are preserved, which are not, and which are disregarded (because some of the notions involved have not been mapped). Additional details as well as the proofs of all the theorems can be found in Masolo et al. (2023). In the following analysis we mainly focus on the results that point out some ontological differences between $dolce$ and $bfo$ .
5.2. Analysis

The list of the bfo axioms, including the information on whether and how they are preserved by the mapping, is presented in Appendix. Note that the axioms forcing the rigidity of the $bfo$ -categories and the taxonomical constraints depicted in Figure 1 are also preserved (relatively to the universals considered in the mappings) but are not listed in Appendix. We note that the percentage of preserved axioms is not a truly informative evaluation of the mapping since this number would not account for: (i) the reasons for the (non-)preservation of the axioms; (ii) the ontological correctness of the mappings; and (iii) the main differences between the two ontologies. Here we provide a ‘qualitative’ evaluation which in our view is ontologically more informative, even though it remains partial due to the complexity of the ontologies and of the mapping.

We begin our analysis by considering how the entities in the domain of $D$ are classified by the categories of bfo as encoded by our definitions. Theorem (t $_{db}$ 1) shows that endurants, perdurants, and qualities are all bfo particulars (in the sense of the bfo notion of particular, $par$ defined in (d $_{db}$ 27)). The case of abstracts is more complex. (t $_{db}$ 2) shows that if there exists at least a time interval then all the $dolce$ abstracts are bfo particulars too. This is due to the definition of $EX$ (d $_{db}$ 1) that assures that $dolce$ abstracts exist at every time. However, while in dolce the existence of endurants, perdurants, and qualities requires them to have a temporal location (and then to be present in time), see (a $_{d}$ 19) and (t $_{d}$ 1), this does not hold for abstracts, that is, it is possible to have models of dolce that contain only abstracts and no time intervals. In this particular case we would not have bfo particulars, only universals (t $_{db}$ 3).

t $_{d}$ 1 $D ⊨ (ed (x) \lor pd (x) \lor q (x)) \to \exists t (P R E (x, t))$

t $_{d b}$ 1 $D_{b} ⊨ (ed (x) \lor pd (x) \lor q (x)) \to par (x)$

t $_{d b}$ 2 $D_{b} ⊨ \exists u (t (u)) \to \forall x (par (x))$

t $_{d b}$ 3 $D_{b} ⊨ \neg \exists u (t (u)) \to \forall x (uni (x))$

(t $_{db}$ 1) seems to conform to both (M1) and (M2), by corroborating the idea that dolce particulars roughly correspond to bfo particulars, and that all the particulars of dolce are ‘imported’ into the ones of bfo. However, (t $_{db}$ 3) introduces some doubts about the nature of abstracts. The definition of $EX$ (d $_{db}$ 1), starting from the fact that temporal and spatial regions are particulars in bfo, extended this idea to all regions (and to all abstracts), that is, there is a presupposition that all the regions have a uniform nature, they are all particulars in this case (even though, in bfo, temporal and spatiotemporal regions are occurrents while spatial regions are continuants). However, other options are possible. One could consider, for instance, the following two variants of (d $_{db}$ 1):

$EX (x, t) := P R E (x, t) \lor (t (x) \land P (t, x)) \lor (s (x) \land t (t))$

$EX (x, t) := P R E (x, t)$

In the first case time intervals and space regions become bfo particulars as before (matching the fact that temporal and spatial regions are particulars in bfo) but, according to (d $_{db}$ 27) and (d $_{db}$ 28), the rest of the abstracts would be included as universals. This possibility is interesting because the examples for dolce (spaces of) regions are colours, weights, shapes, etc., while, in bfo, being red, being blue, being round, etc., are universals. In this perspective, one can also presuppose that the dolce parthood relation $P$ holding between regions (in a given space) represents a sort of (intensional) ISA relation, while $t Q L$ – or, maybe better, the composition of $D Q T$ and $t Q L$ – represents instantiation (at a time). This option deserves a detailed analysis even though it introduces differentiation between time intervals and space regions on the one side, and the remaining regions on the other side.

The second option excludes all abstracts, including time intervals and space regions, from particulars. Even in this case one could see the dolce $P$ relation between regions as a sort of ISA relation and $T L C$ and $S L C$ as sorts of instantiation relations (here note that the (a $_{d}$ 23) and (a $_{d}$ 79) go in the direction of considering $T L C$ and $S L C$ as compositions of $D Q T$ and $t Q L$ as suggested in the previous case also).

In both these cases, the fact that (some) regions become universals is grounded on (d $_{db}$ 27) and (d $_{db}$ 28). The latter is motivated by (a $_{b}$ 1) and (a $_{b}$ 2), that is, by the fact that the entities in the domain of bfo are partitioned into universals and particulars. However, one could decide to reject (a $_{b}$ 1) and assume that some regions are neither bfo particulars nor bfo universals. They would form a kind of entity that bfo does not consider. Also this option deserves a deeper analysis.

There are also more subtle correspondences to consider. Theorem (t $_{db}$ 4) shows that perdurants are the union of processes and process boundaries. However, in $D_{b}$ , the bfo axioms (a $_{b}$ 43), (a $_{b}$ 45), (a $_{b}$ 47), (a $_{b}$ 60), and (a $_{b}$ 62) are not preserved making evident that the distinction between processes and process boundaries behaves quite differently from the one in $B$ .

t $_{d b}$ 4 $D_{b} ⊨ pd (x) \leftrightarrow (\exists t (x : :_{t} p r o c) \lor \exists t (x : :_{t} p b n d))$

bfo presupposes that processes and process boundaries have a different temporal nature, and constrains their relationship, which is quite complex, via a set of axioms. On the other hand, (d $_{db}$ 9) and (d $_{db}$ 10) – together with (d $_{db}$ 5) and (d $_{db}$ 6) – reduce this difference to atomicity and to the existence of strictly larger (relatively to temporary parthood) perdurants. Looking at the counterexamples that cause several BFO axioms not to be preserved, this different behaviour about processes and process boundaries seems mainly due to the poor approximation of the notions of temporal instant and temporal interval provided by (d $_{db}$ 9) and (d $_{db}$ 10) together with the low commitment of dolce on the existence of perdurants.

For instance, in dolce it is possible to have three temporally co-localised perdurants $p_{1}$ , $p_{2}$ , and $p_{12}$ all with atomic temporal locations and such that $p_{12}$ is the mereological sum of $p_{1}$ and $p_{2}$ . To fix the idea with an example, consider $p_{1} =$ ‘Yesterday John saw the first ray of sunshine coming in over the mountain at dawn’, $p_{2} =$ ‘Yesterday Mary saw the first ray of sunshine coming in over the mountain at dawn’, and $p_{12} =$ ‘Yesterday John and Mary saw the first ray of sunshine coming in over the mountain at dawn’. There can also be two additional perdurants $p_{3}$ and $p_{123}$ such that the temporal location of $p_{3}$ does not overlap the one of $p_{1}$ and $p_{123}$ is the mereological sum of $p_{12}$ and $p_{3}$ (e.g., $p_{3} =$ ‘Today John saw again the first ray of sunshine’). In this scenario, according to (d $_{db}$ 6) and (d $_{db}$ 7), $p_{1}$ is a process because it is not a process boundary, and it is not a process boundary because, though it has an atomic temporal location, it is not a temporal proper part of anything (because $p_{1}$ is part of $p_{12}$ , but it is a non-maximal part, since $p_{2}$ exists); $p_{12}$ is a process boundary (against (a $_{b}$ 43) and (a $_{b}$ 47)) because it has an atomic temporal location and it is a proper temporal part of $p_{123}$ . For another example, in dolce it is possible to have perdurants that are not proper temporal parts of any other perdurant and such that all their parts are temporally co-localised with them (possibly with an atomic temporal location) and in their turn are not proper temporal part of any other perdurant (e.g., consider $p_{1}, p_{2}$ and $p_{12}$ in the previous example). According to (d $_{db}$ 5) and (d $_{db}$ 6), these perdurants as well as all their parts are classified as processes against (a $_{b}$ 45), (a $_{b}$ 60), and (a $_{b}$ 62). These examples may seem peculiar, yet they prevent the preservation of several axioms, and are not easy to rule out. One could get rid of some of these cases by requiring that processes have a non-atomic temporal location. Then, one needs to force the removal of (t $_{db}$ 4), otherwise it would be possible to have perdurants with an atomic temporal location that are not temporal proper part of any other perdurant.

There is a further difference concerning the ‘temporal behavior’ of dolce perdurants vs. bfo occurrents. In bfo, occurrent parthood between processes or process boundaries is equivalent to occurrent parthood between the corresponding spatiotemporal regions, therefore different processes or process boundaries cannot be spatiotemporally co-localised. dolce makes the opposite choice and allows for spatiotemporally co-localised perdurants. A similar situation arises between dolce endurants and bfo continuants as highlighted by the fact that neither (a $_{b}$ 78) nor (a $_{b}$ 20) can be proved in $D_{b}$ . In dolce, for instance, an amount of matter constituting a statue at a given time $t$ is different from the statue and it is not a $t P$ -part of the statue at $t$ (and vice versa) even though the two endurants are spatially co-localised at $t$ (and possibly during their whole life), see (a $_{d}$ 88) and (t $_{d}$ 2).

$t_{d} 2 K (x, y, t) \to x \neq y$

Similarly, in dolce, a sum of bricks is different from a wall even though they can mereologically coincide at a given time. This view allows for the co-existence of distinct entities in the same spatial and temporal locations. Such entities are further distinguished on the basis of their ‘modal’ properties. In comparison, bfo embraces a ‘non-multiplicativist’ perspective by assuming that a given spatial or spatiotemporal region cannot be the location of different continuants or occurrents (see in particular the treatment of the example of the statue and the clay in Otte et al. (2022). In other words, space and time locations are not fundamental for the identity of entities in dolce. Thus, at first sight endurants and occurrents on the one hand, and $t P$ and $cP$ on the other, seem to be different ways to capture the ‘same’ ontological category. Nonetheless, a conceptual and formal analysis shows that $D_{b} ⊭ (a_{b} 20)$ , highlighting that the views embraced by these systems, while apparently similar, remain incompatible.

These are not the only differences, of course. From $D_{b} ⊭ (a_{b} 15)$ we see that the $cP$ (as defined in (d $_{db}$ 20)) does not satisfy the supplementation principle, and from $D_{b} ⊭ (a_{b} 16)$ that the existence of the product is not guaranteed. Note that the existence of products cannot be inferred for $oP$ either since $D_{b} ⊭ (a_{b} 41)$ .

According to (d $_{db}$ 20) and the definitions of the subclasses of $c n t$ , for independent continuants that are not spatial regions, $cP$ reduces to $t P$ . However, for independent continuants that are not object aggregates, the original $cP$ is antisymmetric, but is not so the relation defined by (d $_{db}$ 20), that in this case is equivalent to $t P$ . As we have seen, this fact has an important impact on the entities that are classified as endurant or as continuant in the two theories. One could recover the antisymmetry by changing the definition of $cP$ . This amounts to breaking the correspondence between $t P$ and $cP$ for independent continuants by ‘injecting’ antisymmetry into (d $_{db}$ 20), for example,

$cP (x, y, t) := x : :_{t} c n t \land y : :_{t} c n t \land ((t P (x, y, t) \land (\neg t P (y, x, t) \lor x = y)) \lor P (x, y) \lor$

$\exists z u (D Q T (x, z) \land D Q T (y, u) \land t P (z, u, t)))$

This alternative definition has some advantages: (i) it preserves antisymmetry as in the original bfo; and (ii) it states explicitly one difference between

cP

and

t P

. However, some differences remain. We can have endurants that in dolce satisfy

t P

and are mapped to

i d c n t

but do not satisfy the newly defined

cP

. Take our previous example, the (sum of the) bricks and the wall do not satisfy the new

cP

. In all these cases, (a

_{b}

78) fails.

Another approach is to specialise the definition of $cP$ to take into account the different cases, for example,

$cP (x, y, t) := x : :_{t} c n t \land y : :_{t} c n t \land ((t P (x, y, t) \land (\neg t P (y, x, t) \lor x = y)) \lor$

$\exists s r (S L C (x, s, t) \land S L C (y, r, t) \land P (s, r)) \lor$

$P (x, y) \lor \exists z u (D Q T (x, z) \land D Q T (y, u) \land t P (z, u, t)))$

Note that the antisymmetry of

cP

is again lost: The bricks and the wall

cP

-coincide at

t

even though they are different. One could further change the definition of

sREG

stating that the bricks (or the wall) have no spatial location at

t

, or that at

t

they have different spatial locations. One could proceed similarly in the case of the statue and the clay. However, this option seems to go against the natural interpretation of

sREG

bfo

.²³

These examples suggest to follow a different approach, possibly closer to the original commitments of the two ontologies. Consider again the example of the statue and the clay, or the bricks and the wall. There are two different endurants that are spatially coincident at least at a given time. One can think that (a $_{b}$ 78) and (a $_{b}$ 20) aim at ruling out these kinds of examples: It is not a matter of avoiding spatial coincidence or parthood between the bricks and the wall, their goal, one could argue, is to rule out one of these two entities, that is, to rule out from the domain of quantification of $bfo$ , either the bricks or the wall (both of them are in the domain of $dolce$ ).²⁴ One can then adopt a strategy that ‘filters out’ some of the dolce endurants. Setting this filter is not trivial. For the case of the statue and the clay, one can rely on the fact that constitution is a sort of order relation in dolce. One can maintain the substratum (the clay) as an element in the domain, and discard the statue due to the fact that it is the substratum that constitutes the statue. However, in the case of the bricks and the wall we cannot use $t P$ to do the same, because $t P$ is not asymmetric while constitution is. One needs to find a different relation or some other principle to rule out one of these. But this is not all. Let us assume that we do not import the statue into bfo. Does it mean that bfo cannot talk about statues or that it relies on a different representation? After all, it classifies the clay under amount of matter as well as under statue. One would need to translate the dolce claims about the statue into bfo claims about the amount of clay (since it is the only element left in the domain of bfo). The consequences of this approach – in particular how to track statues through the change of their substratum – deserve more investigation. It is however important to note that this first analytical step allows us to understand the differences and to individuate the main problems that a mapping needs to address.

The analysis of more refined correspondences, like (t $_{db}$ 5), (t $_{db}$ 6), and (t $_{db}$ 7), confirms that temporally extended amounts of matters and physical objects are material entities. The other direction does not hold since non-physical endurants could very well be material entities. However, (t $_{db}$ 4), (t $_{db}$ 5), together with (t $_{db}$ 8), (t $_{db}$ 9), and (t $_{db}$ 10), show that there are endurants and qualities, all of which are particulars (see (t $_{db}$ 1)), that are neither continuants nor occurrents. This means that the partition of particulars into continuants and occurrents, assumed by bfo, is not preserved by the mapping: some endurants and qualities end up in an ontological ‘limbo’.

t $_{d b}$ 5 $D_{b} ⊭ (m (x) \lor pob (x)) \to \exists t (x : :_{t} c n t)$

t $_{d b}$ 6 $D_{b} ⊨ (m (x) \lor pob (x)) \land \exists t (T L C (x, t) \land \neg A T (t)) \to \exists t (x : :_{t} m t e n)$

t $_{d b}$ 7 $D_{b} ⊭ \exists t (x : :_{t} m t e n) \to ped (x)$

t $_{d b}$ 8 $D_{b} ⊭ f (x) \to \exists t (x : :_{t} c n t)$

t $_{d b}$ 9 $D_{b} ⊭ q (x) \to \exists t (x : :_{t} c n t)$

t $_{d b}$ 10 $D_{b} ⊭ nped (x) \to \exists t (x : :_{t} c n t)$

On the other hand, the imported entities do not necessarily cover all the categories of bfo. There are at least two reasons for that, one factual and one structural. The factual reason is that some of the dolce categories may be empty. For instance, if there are no features, then $i m e n$ would be empty. Consequently, axiom (a $_{b}$ 6), which states that all universals are non-empty, is not preserved. The structural reason is that, according to the mapping, some categories (as defined in the definitions) are necessarily empty. This is the case of universals (assuming that there is at least a time in the domain of quantification, see (t $_{db}$ 2)). One solution is to consider some types of entities, for example, those that earlier we said are in an ontological ‘limbo’, as bfo universals. We already saw that some regions (e.g., abstracts) could be seen as universals. Similarly, one could assume that specific subclasses of non-physical endurant ( $nped$ ) are actually concepts behaving like bfo universals. Note that this approach has an important impact on the theorems one can prove.

One way to choose among the alternative approaches in developing the mapping, is to look at what the mapping optimises. For instance, strict and restrictive mappings, carefully set to not allow exchanges of entities that would be in the ontological ‘limbo’ of the target ontology, might be preferred in the context of data transfer, they are safer in this context. Mappings focussing on ontological significance and the maximisation of the number of imported entities are instead arguably better for the goals of comparing ontologies, highlighting core differences, and establishing general interoperability results.

6. The Mapping From bfo to dolce

6.1. The Definitions of dolce Primitives in the Language of bfo

In this section we introduce syntactic definitions of dolce notions in terms of bfo primitives. The starting point is the domain of bfo. We aim to classify and relate the entities in this domain in terms of the categories and relations of dolce. Analogously to the dolce to bfo direction in Section 5 and with similar motivations (see the analysis of Section 6.2), we obtain only a partial mapping covering a subset of the categories and primitives of dolce.

As discussed in Section 4.2, in dolce the agentive and social dimensions play an important role in characterising the subcategories of physical object ( $pob$ ) and non-physical endurant ( $nped$ ) but those dimensions are not considered in bfo. Similarly, the subcategories of perdurant ( $pd$ ) rely on the notions of homeomericity and cumulativity, but these notions are beyond the scope of bfo. This leads to excluding these subcategories from the mapping. Furthermore, while it is not clear how the distinction between amounts of matter and physical objects can be made, regarding features we can rely on the bfo categories of site, continuant fiat boundary and fiat object part. Thus, within the category of physical endurants ( $ped$ ) we include in the mapping only the category of features ( $f$ ).

We will see that physical endurants correspond to independent continuants that are not regions, see (d $_{bd}$ 3), while the only entities that can be mapped to non-physical endurants are generically dependent continuants, see (d $_{bd}$ 5). In dolce, arbitrary sums ( $as$ ) have necessarily a physical and a non-physical part, see (a $_{d}$ 41). To match this axiom, in bfo we should find continuants that are not spatial regions and are neither independent nor generically dependent continuants. The only option is that of specifically dependent continuants. However, following our guidelines in Section 3, these are mapped to dolce physical qualities, as formalised in (d $_{bd}$ 6). As a result, the category $as$ of arbitrary sums would be empty. For this reason, $as$ is not covered in the mapping.

In Section 5.2 we have seen that one of the main differences between dolce and bfo concerns the reduction of the parthood relations to spatial and spatiotemporal inclusions. In particular, in bfo there are no spatially co-localised distinct independent continuants (that are not object aggregates) and there are no spatiotemporally co-localised distinct occurrents. We then lack one of the main basis to build a constitution relation among endurants and perdurants. In principle, one could see the relation between a generically dependent continuant and the mereological sum of its carriers at a given time as a form of constitution. This solution is debatable and would model only a very limited notion of constitution, quite different from the general one in dolce. Thus, we refrain from introducing $K$ in the mapping.

Concerning qualities, bfo accepts only qualities inhering in independent continuants. From the point of view of dolce, this restricts the mapping to physical qualities only, see (d $_{bd}$ 7).

Regarding regions, there are time intervals and space regions. To locate entities in time and space we need to rely on $T L C$ and $S L C$ only because dolce’s temporal and spatial locations have no correspondent entities in bfo. In particular, the $Q L$ and $t Q L$ relations do not make sense in this setting. Alternatively, as previously discussed, one could import some bfo universals into dolce regions and assume that instance-of corresponds to ( $D Q T$ composed with) $t Q L$ . In this case, the ISA relation would correspond to the primitive $P$ , that in dolce is defined on regions. This alternative, which we do not investigate here, seems worth developing.

Finally, the categories for facts and for sets, that in the original taxonomy of dolce (Masolo et al., 2003) appear under abstract ( $ab$ ), have not been taken into account in dolce-cl, thus we ignore them here.

Summing up, in the following we discuss these dolce notions:

(i)
syntactic definitions for the primitive relations: $P$ , $t P$ , $T L C$ , $S L C$ , $P C$ , $D Q T$ , $E X D$ ; and
(ii)
syntactic definitions for the categories: $ed$ , $pd$ , $q$ , $ab$ , $f$ , $ped$ , $nped$ , $pq$ , $r$ , $tr$ , $pr$ , $t$ , and $s$ .

Below we list these syntactic definitions providing just short informal descriptions, a deeper analysis about these definitions and their impact on the preservation of the axioms of dolce is done in Section 6.2. d $_{{bd}}$ 1
$pd (x) := x : :_{} p r o c \lor x : :_{} p b n d$

Perdurants coincide with the disjunction of processes and process boundaries (see (d $_{b}$ 2) for the definition of $: :_{}$ ).
d $_{{bd}}$ 2
$ed (x) := x : :_{} c n t \land \neg (x : :_{} s r e g) \land \neg (x : :_{} s d c n t)$

We rule out from endurants spatial regions and specifically dependent continuant that are mapped, respectively, to space regions and physical qualities, see (d $_{bd}$ 10) and (d $_{bd}$ 6).
d $_{{bd}}$ 3
$ped (x) := x : :_{} i d c n t \land \neg (x : :_{} s r e g)$

Physical endurants are independent continuants that are not spatial regions.
d $_{{bd}}$ 4
$f (x) := x : :_{} s i t e \lor x : :_{} c f b n d \lor x : :_{} f o b j p$

Features are the union of sites, continuant fiat boundaries, and fiat object parts.
d $_{{bd}}$ 5
$nped (x) := x : :_{} g d c n t$

Non-physical endurants coincide with generically dependent continuants.
d $_{{bd}}$ 6
$pq (x) := x : :_{} s d c n t$

Physical qualities coincide with specifically dependent continuants. Note that relational qualities and realisable entities, like roles and dispositions, are imported into physical qualities.
d $_{{bd}}$ 7
$q (x) := pq (x)$

Only physical qualities exist (bfo has only qualities of independent continuants).
d $_{{bd}}$ 8
$t (x) := x : :_{} t r e g$

Time intervals coincide with temporal regions. One could consider a stronger definition, that is, assume that $t$ corresponds to $t i n t$ . However, following (M2) we aim to import all the temporal regions.
d $_{{bd}}$ 9
$tr (x) := t (x)$

Among temporal regions there are only time intervals.
d $_{{bd}}$ 10
$s (x) := x : :_{} s r e g$

Space regions coincide with spatial regions.
d $_{{bd}}$ 11
$pr (x) := s (x)$

Among physical regions there are only space regions.
d $_{{bd}}$ 12
$r (x) := tr (x) \lor pr (x)$

Regions are temporal regions or spatial regions.
d $_{{bd}}$ 13
$ab (x) := r (x)$

Among abstracts there are only time intervals and space regions.
d $_{{bd}}$ 14
$T L C (x, t) := (pd (x) \lor ed (x) \lor q (x)) \land t (t) \land \forall u (EX (x, u) \leftrightarrow tP (u, t))$

The temporal location of $x$ is the maximal time at which $x$ exists. (In bfo, $tREG$ is defined only on processes and process boundaries).
d $_{{bd}}$ 15
$P (x, y) := (((pd (x) \land pd (y)) \lor (t (x) \land t (y))) \land oP (x, y)) \lor (s (x) \land s (y) \land \forall t (EX (x, t) \to cP (x, y, t)))$

For perdurant and time intervals $P$ coincides with $oP$ while for space regions it reduces to constant parthood, that is, $x$ is a continuant part of $y$ during its whole existence (note that in bfo, all the spatial regions exist at least at a time).
d $_{{bd}}$ 16
$t P (x, y, t) := ed (x) \land ed (y) \land cP (x, y, t)$

For endurants $t P$ coincides with $cP$ .
d $_{{bd}}$ 17
$P C (x, y, t) := ed (x) \land pd (y) \land \exists z (tP (y, z) \land PTC (x, z, t))$

$PTC$ is not defined on process boundaries while dolce does not impose any constraint on the kind of the process involved in $P C$ . The existential quantification on $z$ aims to mitigate this difference.
d $_{{bd}}$ 18
$D Q T (x, y) := INH (x, y)$

The relation of direct quality coincides with inheritance (see (d $_{b}$ 8)).
d $_{{bd}}$ 19
$E X D (x, y, t) := (SDEP (x, y) \land EX (x, t)) \lor GDEP (x, y, t) \lor PTC (x, y, t) \lor PTC (y, x, t)$

$E X D$ is the generalisation of $SDEP$ , $GDEP$ , and $PTC$ ( $PTC$ counts as a sort of mutual dependence).
d $_{{bd}}$ 20
$S L C (x, s, t) := (x : :_{t} i d c n t \land \neg (x : :_{t} s r e g) \land sREG (x, s, t)) \lor (x : :_{t} g d c n t \land \exists y (GDEP (x, y, t) \land \forall z (GDEP (x, z, t) \to cP (z, y, t)) \land sREG (y, s, t))) \lor (q (x) \land \exists y (INH (x, y) \land \forall z (INH (x, z) \to cP (z, y, t)) \land sREG (y, s, t))) \lor (pd (x) \land \exists y (stREG (x, y) \land sPROJ (y, s, t)))$

For independent continuants that are not spatial regions, $S L C$ coincides with $sREG$ (first disjunct). The spatial location, at $t$ , of a generically dependent continuant $x$ is the spatial region of the maximal entity (if it exists) on which $x$ generically depends on at $t$ (second disjunct). The spatial location of a quality $x$ at $t$ is the spatial region of the maximal (at $t$ ) entity (if it exists) in which $x$ inheres (third disjunct). The spatial location of a perdurant is the spatial projection of its spatiotemporal location (fourth disjunct). Note that in bfo, no axiom guarantees that a specifically dependent continuant $x$ inheres in a unique continuant, therefore for qualities we define the spatial location only when there is a ‘maximal continuant’ in which $x$ inheres in. A similar argument applies for generic dependent continuants.

One may think that the mapping given by these definitions is too restrictive: In dolce physical and non-physical endurants are not limited to, respectively, independent continuants and generically dependent continuants (the latter are a quite special kind of entities), and so on. This may suggest to include $x : :_{} i d c n t \land \neg (x : :_{} s r e g) \to ped (x)$ as well as $x : :_{} g d c n t \to nped (x)$ , but not the converse formulas. However, we need to remember that we are considering the mapping from bfo to dolce. The starting point is the domain of bfo, that is, we need first of all to try to classify the entities that belong to the domain of bfo in terms of the categories of dolce. By looking at the mappings it is easy to see that all the particulars²⁵ of bfo are classified in terms of dolce categories except for spatiotemporal regions:²⁶ (i) independent continuants which are not spatial regions are mapped to physical endurants; (ii) spatial regions to space regions; (iii) generically dependent continuants to non-physical endurants; (iv) specifically dependent continuants to dolce qualities; (v) process and process boundaries to perdurants; and (vi) temporal regions to time intervals. The fact that dolce intuitively accepts, for instance, additional physical or non-physical endurants suggests that, in general, dolce has a domain of particulars larger than the domain of particulars of bfo. Our methodological choice (M3) does not allow the mappings to ‘enrich’ the domain of bfo with new entities. However, by introducing the mapping at the semantic level, that is, in this case, as an operator translating any bfo-structure into a dolce-structure, one could enrich the original domain of bfo by set-theoretically building new entities. This is the approach followed in the literature to map theories of time based on points to theories based on intervals, see (Van Benthem, 1983). The theory based on intervals does not admit points, but points can be built as sets of intervals satisfying a certain relation definable in the theory of intervals. Analogously, one can think of building some entities, for example, statues as opposed to amounts of clay, starting from the amounts of clay and the specific kinds of universals they instantiate. Like in Section 5, the investigation of this kind of ‘semantic mapping’ is not considered in this work.

Furthermore, notice that (a $_{b}$ 6) states that all the universals are non-empty. From an applicative perspective, this is a strong constraint because it forces the user to model even entities which might not be relevant to the application (and perhaps time consuming to analyse). Note that, once (a $_{b}$ 6) is removed, the existential constraints in $bfo$ are compatible with the instantiation of only some categories. From a technical perspective, (a $_{b}$ 6) requires very large models that make the identification and management of counterexamples very difficult even with the support of dedicated software. For these reasons, we do not consider (a $_{b}$ 6) in the comparison.

In the following, $B_{d}$ is the set $B ∖ {$ (a $_{b}$ 6) $}$ with the definitions of Section 6.1, that is, $B_{d} = {B ∖ {$ (a $_{b}$ 6) $}} \cup {$ (d $_{db}$ 1),…,(d $_{db}$ 20) $}$ . Some axioms of dolce use relations or categories that have not been defined in the mappings. When possible and relevant we considered approximations of these axioms as expressible in the dolce language, otherwise we set them aside. As already said, the first column in the tables in Appendix shows which axioms (or their approximations) have been preserved, non preserved, or disregarded. Additional details as well as the proofs of all the theorems are in Masolo et al. (2023). Again, in the following analysis we mainly focus on the results that point out some ontological differences between $dolce$ and $bfo$ .
6.2. Analysis

The list of dolce axioms, including the information on whether and how they are preserved by the mapping, is presented in Appendix. Note that the axioms concerning the taxonomical constraints depicted in Figure 2 are also preserved (relatively to the categories considered in the mappings) but are not listed in Appendix. Following what done in Section 5.2, we start our qualitative analysis by considering where bfo entities end up in dolce via the mapping. With the exception of the spatiotemporal regions, all the particulars of bfo find their place in dolce, in the sense that each instance of a bfo universal is mapped to be an instance of some dolce category. Spatiotemporal regions are not mapped to some dolce category even though, as already anticipated, one could extend dolce with a category for spatiotemporal regions. Furthermore, it is not clear to us, in terms of expressive power, what spatiotemporal regions add to temporal and spatial regions. On the other hand, the universals of bfo are not mapped into dolce. However, bfo universals could be mapped in dolce using alternative mapping strategies, some of which have been suggested already: for example mapping universals to regions or to non-physical endurants. Both alternatives would require to reconsidering the mappings (d $_{bd}$ 5) and (d $_{bd}$ 12), and perhaps (d $_{bd}$ 9) and (d $_{bd}$ 11).

From the opposite point of view, that is, analysing what happens to dolce categories by following the mapping from bfo, one notes that some of these are empty (i.e. no entity of bfo can instantiate them). This is the case of $as$ , $ar$ , $tq$ , and $aq$ . Other categories are drastically reduced or expanded: physical qualities/regions collapse to spatial locations/space regions, temporal intervals are mapped to time regions. In agreement with earlier observations, the reduction or emptiness of some categories together with the multiplicativist approach adopted by dolce²⁷ suggest that dolce accepts a larger domain of particulars. Whether this larger variety of entities translates into a higher expressive power needs to be further investigated (but see (Otte et al., 2022) and (Borgo et al., 2022a) for an analysis of how classical representation examples are treated in $bfo$ and $dolce$ ).

Concerning the preservation of the axioms of dolce, our results show that few, and quite technical, differences between $bfo$ and $dolce$ prevent the preservation of several axioms. In dolce, $P R E$ is defined only for the entities that have a temporal extension, see (d $_{d}$ 6), while in bfo $EX$ is a primitive relation.²⁸ In bfo an entity may exist at two non overlapping temporal regions without existing at any bigger temporal region. In these situations the condition $\forall u (EX (x, u) \leftrightarrow tP (u, t))$ in the definition of $T L C (x, t)$ , see (d $_{bd}$ 14), is never satisfied, and consequently the relation $P R E$ is not satisfied. This difference hampers the preservation of several axioms of dolce because $P R E$ is heavily used in the characterisation of the primitives of dolce (in particular $B_{d} ⊭ (a_{d} 19)$ ). At the same time, the difference seems to have a technical, more than ontological, nature; after all, in both ontologies the entity exists at both times. A similar problem can be seen in axioms like (a $_{d}$ 35) and (a $_{d}$ 55) where the holding of a relation at two times does not suffice to infer that the relation holds also at the sum of those times (provided such sum exists). However, the fact that an entity exists at two times but not at their sum prevents, for the majority of relations, the possibility for the relation to hold at the sum. The bfo relation $sREG$ is one of these relations: A continuant can occupy spatial regions (even the same spatial region) at two given times without having a spatial location at the sum of these times. This fact, together with the definition of $S L C$ (d $_{bd}$ 20), clarifies why (a $_{d}$ 84) and several other dolce theorems involving $S L C$ are non preserved.

These difficulties may suggest that a different mapping technique could be preferred. Rather than encapsulating the relation between $EX$ and $T L C$ into the mapping (d $_{bd}$ 14), one could take a more articulated procedure: first introduce a direct mapping between $EX$ and $P R E$ , then define $T L C$ by using $P R E$ (as defined in the mapping), for example,

$P R E (x, t) := (pd (x) \lor ed (x) \lor q (x)) \land EX (x, t)$

$T L C (x, t) := \forall u (P R E (x, u) \leftrightarrow P (u, t))$

In this way, entities that, for instance, exist at two times but not at their mereological sum would still lack a temporal location

T L C

but this would not prevent

P R E

from holding when applied to them (due to the first mapping). We can then try to recover some theorems that do not require

T L C

at the price of possibly losing the connection between

P R E

and

T L C

originally present in

dolce

. The applicability of this mapping technique to other primitives and its actual consequences are not further studied in this paper.

The problems highlighted up to this point were discussed because of their impact on the mapping but are primarily of technical nature. The mapping highlights also genuine ontological differences. First, the defined $P$ , like $oP$ , does not satisfy the supplementation axiom (a $_{d}$ 7) assumed in dolce. Second, the relation $INH$ is not equivalent to the original $D Q T$ , in particular it does not satisfy (a $_{d}$ 9), that is, the fact that (direct) qualities inhere in a unique bearer. For relational qualities this can be problematic if, for instance, one wants to distinguish ‘Mary’s love for John’ from ‘John’s love for Mary’: in both cases we obtain a relational quality inhering in both John and Mary. Third, the reflexivity of the defined $t P$ , like the one of $cP$ , does not hold for all the continuants. It follows that in bfo one can have continuants for which $cP$ is not defined. Fourth, while in dolce all the perdurants must have participants at every time they exist (a $_{d}$ 56), bfo guarantees the existence of participants for processes but not for process boundaries (see (a $_{b}$ 113)). Furthermore, in bfo, continuants do not necessarily participate in processes while in dolce all the endurants participate in a process when they exist (a $_{d}$ 57).

7. Grounding OWL Mappings on FOL Mappings

For both $bfo$ and $dolce$ an OWL version exists. These versions are used when usability and tractability become important applicative factors that prevail over the deep and explicit characterisation of ontological commitments. Given the low expressive power of OWL, the majority of the axioms in the FOL versions and the majority of the mappings introduced in the previous sections – mappings that, in their turn, are expressed as FOL syntactic definitions – cannot be preserved or can be only very roughly approximated. The semantic correspondences established via the FOL mappings can however be used to ground and justify OWL mappings.

In OWL, $s u b C l a s s O f$ mappings are arguably among the most important ones. A $s u b C l a s s O f$ mapping assures that a class of an ontology is subsumed by a class of another ontology. To justify, for instance, a $s u b C l a s s O f$ mapping from $C_{b}$ to $C_{d}$ (where $C_{b}$ is a $bfo$ category and $C_{d}$ is a $dolce$ category) the following two conditions must hold (where $S U B (C_{d})$ is the set of all the subcategories of $C_{d}$ in the $dolce$ taxonomy in Figure 2 that have been explicitly considered in the mapping from $bfo$ to $dolce$ ):

(c1) $B_{d} ⊨ x : :_{} C_{b} \to C_{d} (x)$

(c2) $B_{d} ⊭ x : :_{} C_{b} \to C (x)$ , for all $C \in S U B (C_{d})$

Condition (c1) assures that

C_{b}

is subsumed by

C_{d}

while (c2) assures that

C_{b}

is not subsumed by any subcategory of

C_{d}

, that is, (c1)+(c2) guarantee that

C_{d}

is the minimal

dolce

category subsuming

C_{b}

For instance, the holding of:

$B_{d} ⊨ x : :_{} m t e n \to ed (x)$

$B_{d} ⊭ x : :_{} m t e n \to ped (x)$

$B_{d} ⊭ x : :_{} m t e n \to nped (x)$

justifies a

s u b C l a s s O f

mapping from

bfo

material entities to

dolce

endurants (the category

as

of arbitrary sums has been ruled out from the mapping from

bfo

dolce

A similar reasoning can be done for $d i s j o i n t W i t h$ and $s u b P r o p e r t y O f$ mappings. Note however that sub-properties mappings often require to restrict the domain and range of the source relation to conjunctions of classes. To explicitly express this kind of mappings, the Semantic Web Rule Language (SWRL)²⁹ might be needed.

The OWL-versions of $bfo$ and $dolce$ and all the identified OWL-mappings are available at the GitHub repository at https://github.com/OntoCommons/OntologyFramework.

8. Conclusion

The construction of an ontology ecosystem for information classification and exchange requires formal alignments across ontologies. From the theoretical viewpoint, the most essential alignments are those across foundational ontologies. This paper has presented a general strategy and has motivated some methodological assumptions for such a construction. Furthermore, it has applied this approach to two well-known ontologies, namely bfo and dolce, which might seem to provide an ideal test for formal alignments due to their overall similarity. The analysis has revealed that similarities may hide deep differences and that even apparently minor modelling differences have a relevant impact when formal alignments are sought.

The applied ontology research community has not yet investigated in depth the formal alignment of foundational ontologies. One can imagine the development of a toolkit of strategies, assumptions and methodologies to guide the construction of formal ontology alignments depending on what one aims to preserve across the systems. Some alternatives have been already highlighted in the paper, including a discussion of their consequences. Yet, there are many alternatives and we lack even a general framework to systematically classify them, leaving aside comparing them. Overall, the study in this paper has made clear that the strong interactions existing across the notions used in a foundational ontology, let them be categories or relations, may turn even small changes in the adopted definitions into important changes in how much of the two systems the mapping may hope to align.

As foundational ontologies mature in terms of their formalisation and conceptual coherence, the exploitation of formal alignments across these systems acquires more relevance and gets the community closer to the construction of an ontology-based marketplace for reliable data and information exchange.

In the future, we plan to deepen the analysis here presented comparing what can be gained and lost depending on the strategy, assumptions and methodologies. The deliverable D2.7 of the OntoCommons project (Masolo et al., 2023) investigates formal alignments between $dolce$ and the ‘Elementary Multiperspective Material Ontology’ (emmo)³⁰ that embraces a completely different ontological commitment.

Footnotes

Acknowledgement

The authors thank the participants of the OntoCommons project for their support and in particular Emanuele Ghedini, Francesco A. Zaccarini, Luca Biccheri, Nicola Guarino, Daniele Porello, Emilio M. Sanfilippo, and Laure Vieu.

ORCID iDs

Francesco Compagno

Stefano Borgo

Claudio Masolo

Funding

The author(s) received the following financial support for the research, authorship and/or publication of this article: This article has been developed within the OntoCommons project (GA 958371, ontocommons.eu) and in part within the project ERC Advanced Grant C-FORS (GA 101054836).

Declaration of Conflicting Interests

The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

Notes

‘ $+$ ’: preserved axiom

‘ $\sim$ ’: preserved a weaker version of the axiom (the version proved in reported between ‘[ $\dots$ ]’)

‘°’: non preserved axiom

‘ ’: axiom discarded because it contains non-mapped primitives

The Theory

B

and Axioms Preservation from

D_{b}

$+$	a $_{b}$ 1	eto	$par (x) \lor uni (x)$
$+$	$a_{b}$ 2	qkp	$par (x) \to \neg uni (x)$
$\sim$	$a_{b}$ 3	ekp	$x : :_{t} u \to par (x) \land uni (u) \land tm (t)$ [only for the universals considered in the mapping]
$+$	$a_{b}$ 4	oap	$EX (x, t) \to par (x) \land tm (t)$
$\sim$	$a_{b}$ 5	bee	$EX (x, t) \leftrightarrow \exists u (x : :_{t} u)$ [only for the universals considered in the mapping]
°	$a_{b}$ 6	mbf	$uni (u) \to \exists x t (x : :_{t} u)$
$+$	$a_{b}$ 7	nmq	$par (x) \to \exists t (EX (x, t))$
$\sim$	$a_{b}$ 8	zuw	$x : :_{} m t e n \to \exists t (t : :_{t} t r e g 1 \land EX (x, t))$ [ $\exists t (x : :_{t} m t e n) \to \exists t (t : :_{t} t i n t \land EX (x, t))$ ]
°	$a_{b}$ 9	nis	$tm (t) \to \exists x u (x \neq t \land x : :_{t} u)$
$\sim$	$a_{b}$ 10	qaf	$x : :_{t} u \land tP (t^{'}, t) \to x : :_{t^{'}} u$ [only for the universals considered in the mapping]
$+$	$a_{b}$ 11	vgn	$(x : :_{} c n t \lor x : :_{} o c c) \to ent (x)$
$+$	$a_{b}$ 12	bdd	$cP (x, y, t) \to x : :_{t} c n t \land y : :_{t} c n t \land tm (t)$
$+$	$a_{b}$ 13	mcd	$x : :_{t} i d c n t \to cP (x, x, t)$
$+$	$a_{b}$ 14	plp	$cP (x, y, t) \land cP (y, z, t^{'}) \land tP (t, t^{'}) \to cP (x, z, t)$
°	$a_{b}$ 15	fyf	$cP (x, y, t) \land x \neq y \to \exists z (cP (z, y, t) \land z \neq y \land \neg cO (z, x, t))$
°	$a_{b}$ 16	gzr	$cO (x, y, t) \to \exists z (\forall w (cP (w, z, t) \leftrightarrow cP (w, x, t) \land cP (w, y, t)))$
$+$	$a_{b}$ 17	mqp	$cP (x, y, t) \land tP (t^{'}, t) \to cP (x, y, t^{'})$
$+$	$a_{b}$ 18	uns	$cP (x, y, t) \land EX (y, t) \to EX (x, t)$
	$a_{b}$ 19	glc	$\exists t (x : :_{t} o b j a g g \land cP (x, y, t) \land cP (y, x, t)) \land \forall t (cP (x, y, t) \leftrightarrow cP (y, x, t)) \to x = y$
°	$a_{b}$ 20	tab	$\exists t (x : :_{t} i d c n t \land y : :_{t} i d c n t \land \neg (x : :_{t} o b j a g g) \land \neg (y : :_{t} o b j a g g) \land cP (x, y, t) \land cP (y, x, t)) \to x = y$
	$a_{b}$ 21	yir	$x : :_{t} f o b j p \leftrightarrow \neg (x : :_{t} i m e n) \land \exists y (y : :_{t} o b j \land cPP (x, y, t))$
$\sim$	$a_{b}$ 22	cez	$cP (x, y, t) \to (x : :_{t} i d c n t \leftrightarrow y : :_{t} i d c n t)$ [ $cP (x, y, t) \land x : :_{t} i d c n t \to y : :_{t} i d c n t$ ]
°	$a_{b}$ 23	adm	$x : :_{t} m t e n \land \exists y (cP (y, x, t) \land x \neq y) \to \exists y (cP (y, x, t) \land x \neq y \land \neg (y : :_{t} i m e n))$
°	$a_{b}$ 24	mic	$x : :_{t} m t e n \land cP (y, x, t) \to (y : :_{t} m t e n \lor y : :_{t} s i t e \lor y : :_{t} c f b n d)$
$+$	$a_{b}$ 25	dok	$x : :_{t} m t e n \land cP (x, y, t) \to y : :_{t} m t e n$
	$a_{b}$ 26	mjj	$x : :_{t} s i t e \land cP (y, x, t) \to (y : :_{t} s i t e \lor y : :_{t} c f b n d)$
	$a_{b}$ 27	izr	$x : :_{t} s i t e \land cP (x, y, t) \to (y : :_{t} s i t e \lor y : :_{t} m t e n)$
$+$	$a_{b}$ 28	kbr	$cP (x, y, t) \to (x : :_{t} s r e g \leftrightarrow y : :_{t} s r e g)$
	$a_{b}$ 29	fzg	$x : :_{t} s r e g 3 \land cP (y, x, t) \to y : :_{t} s r e g$
	$a_{b}$ 30	hbn	$x : :_{t} s r e g 2 \land cP (y, x, t) \to (y : :_{t} s r e g 2 \lor y : :_{t} s r e g 1 \lor y : :_{t} s r e g 0)$
	$a_{b}$ 31	wne	$x : :_{t} s r e g 1 \land cP (y, x, t) \to (y : :_{t} s r e g 1 \lor y : :_{t} s r e g 0)$
	$a_{b}$ 32	bfv	$x : :_{t} s r e g 0 \land cP (y, x, t) \to (y : :_{t} s r e g 0)$
	$a_{b}$ 33	ixo	$x : :_{t} c f b n d \land cP (y, x, t) \to y : :_{t} c f b n d$
	$a_{b}$ 34	ysp	$x : :_{t} f s f \land cP (y, x, t) \to y : :_{t} c f b n d$
	$a_{b}$ 35	cwp	$x : :_{t} f l n \land cP (y, x, t) \to (y : :_{t} f l n \lor y : :_{t} f p t)$
	$a_{b}$ 36	jgo	$x : :_{t} f p t \land cP (y, x, t) \to x = y$
$+$	$a_{b}$ 37	zmr	$oP (x, y) \to x : :_{} o c c \land y : :_{} o c c$
$+$	$a_{b}$ 38	hbj	$x : :_{} o c c \to oP (x, x)$
$+$	$a_{b}$ 39	xlu	$oP (x, y) \land oP (y, x) \to x = y$
$+$	$a_{b}$ 40	kad	$oP (x, y) \land oP (y, z) \to oP (x, z)$
°	$a_{b}$ 41	hpc	$oO (x, y) \to \exists z (\forall w (oP (w, z) \leftrightarrow oP (w, x) \land oP (w, y)))$
$+$	$a_{b}$ 42	ybr	$oP (x, y) \land EX (x, t) \to EX (y, t)$
°	$a_{b}$ 43	csk	$x : :_{} p r o c \land oP (x, y) \to y : :_{} p r o c$
$+$	$a_{b}$ 44	ccz	$x : :_{} p r o c \land oP (y, x) \to (y : :_{} p r o c \lor y : :_{} p b n d)$
°	$a_{b}$ 45	aff	$x : :_{} p r o c \to \exists y (y : :_{} p b n d \land oP (y, x))$
$+$	$a_{b}$ 46	ptm	$x : :_{} p b n d \land oP (x, y) \to (y : :_{} p b n d \lor y : :_{} p r o c)$
°	$a_{b}$ 47	hdk	$x : :_{} p b n d \land oP (y, x) \to y : :_{} p b n d$
$+$	$a_{b}$ 48	gjl	$oP (x, y) \to (x : :_{} t r e g \leftrightarrow y : :_{} t r e g)$
	$a_{b}$ 49	myl	$oP (x, y) \to (x : :_{} s t r e g \leftrightarrow y : :_{} s t r e g)$
$+$	$a_{b}$ 50	ruj	$tP (x, y) \to x : :_{} o c c \land y : :_{} o c c$
$+$	$a_{b}$ 51	lyx	$tREG (x, t) \to (x : :_{} p r o c \lor x : :_{} p b n d) \land tm (t)$
$+$	$a_{b}$ 52	bvr	$x : :_{} o c c \to tP (x, x)$
$+$	$a_{b}$ 53	zdq	$tP (x, y) \land tP (y, x) \to x = y$
$+$	$a_{b}$ 54	bfq	$tP (x, y) \land tP (y, z) \to tP (x, z)$
$+$	$a_{b}$ 55	vbw	$x : :_{x} t r e g \land y : :_{y} t r e g \land tPP (x, y) \to \exists z (tPP (z, y) \land \neg tO (z, x))$
$+$	$a_{b}$ 56	bal	$tP (x, y) \to oP (x, y)$
$+$	$a_{b}$ 57	jqz	$tP (x, y) \land EX (x, t) \to EX (y, t)$
$+$	$a_{b}$ 58	cmy	$x : :_{} t r e g \land y : :_{} t r e g \to (tP (x, y) \leftrightarrow oP (x, y))$
$+$	$a_{b}$ 59	njq	$t^{'} : :_{t} t r e g \to tP (t, t^{'})$
°	$a_{b}$ 60	esh	$x : :_{} p b n d \leftrightarrow \exists y (tP (x, y) \land y : :_{} p r o c) \land \exists t (tREG (x, t) \land t : :_{t} t i n s t)$
$+$	$a_{b}$ 61	atz	$x : :_{} p b n d \land tREG (x, t) \to t : :_{t} t i n s t$
°	$a_{b}$ 62	fzy	$x : :_{} p r o c \land tREG (x, t) \to \exists t^{'} (t^{'} : :_{t^{'}} t i n t \land tP (t^{'}, t))$
$+$	$a_{b}$ 63	tao	$(x : :_{} p r o c \lor x : :_{} p b n d) \land tm (t) \to (tREG (x, t) \leftrightarrow \forall y t^{'} (oP (y, x) \land tREG (y, t^{'}) \to oP (t^{'}, t)) \land \neg \exists t^{'} (oPP (t^{'}, t) \land t^{'} \neq t \land tREG (x, t^{'})))$
$+$	$a_{b}$ 64	jiv	$oP (x, y) \land tREG (x, t) \land tREG (y, t^{'}) \to oP (t, t^{'})$
$+$	$a_{b}$ 65	aqu	$tPP (x, y) \to \neg tPP (y, x)$
$+$	$a_{b}$ 66	mns	$tPP (x, y) \land tPP (y, z) \to tPP (x, z)$
	$a_{b}$ 67	dvq	$mP (x, y, t) \to x : :_{t} o b j \land y : :_{t} o b j a g g \land tm (t)$
	$a_{b}$ 68	yip	$mP (x, y, t) \land tP (t^{'}, t) \to mP (x, y, t^{'})$
	$a_{b}$ 69	ibd	$x : :_{} o b j a g g \to \exists y z t (y \neq z \land mP (y, x, t) \land mP (z, x, t))$
	$a_{b}$ 70	uhs	$x : :_{t} o b j a g g \to \exists y (mP (y, x, t))$
	$a_{b}$ 71	evk	$mP (x, y, t) \leftrightarrow x : :_{t} o b j \land y : :_{t} o b j a g g \land cP (x, y, t) \land \forall z (mP (z, y, t) \to (z = x \lor \neg cO (z, x, t)))$
	$a_{b}$ 72	fsy	$cPP (x, y, t) \land y : :_{t} o b j a g g \to \exists z (mP (z, y, t) \land cO (z, x, t))$
$+$	$a_{b}$ 73	lzw	$sREG (x, y, t) \to x : :_{t} i d c n t \land \neg (x : :_{t} s r e g) \land y : :_{t} s r e g \land tm (t)$
$+$	$a_{b}$ 74	bge	$LOC (x, y, t) \to x : :_{t} i d c n t \land \neg (x : :_{t} s r e g) \land y : :_{t} i d c n t \land \neg (y : :_{t} s r e g) \land tm (t)$
$+$	$a_{b}$ 75	zls	$sREG (x, y, t) \land sREG (x, z, t) \to y = z$
°	$a_{b}$ 76	mud	$sREG (x, y, t) \land tP (t^{'}, t) \to sREG (x, y, t^{'})$
$+$	$a_{b}$ 77	uas	$LOC (x, y, t) \to \exists t^{'} r s (tP (t^{'}, t) \land sREG (x, r, t^{'}) \land sREG (y, s, t^{'}) \land cP (r, s, t^{'}))$
°	$a_{b}$ 78	scr	$x : :_{t} m t e n \land y : :_{t} m t e n \land sREG (x, r, t) \land sREG (y, r, t) \to cP (x, y, t) \land cP (y, x, t)$
°	$a_{b}$ 79	put	$LOC (x, y, t) \land tP (t^{'}, t) \to LOC (x, y, t^{'})$
°	$a_{b}$ 80	xlm	$LOC (x, y, t) \land LOC (y, z, t^{'}) \land tP (t, t^{'}) \to LOC (x, z, t)$
$+$	$a_{b}$ 81	evu	$LOC (x, y, t) \land cP (y, z, t) \to LOC (x, z, t)$
°	$a_{b}$ 82	wty	$LOC (x, y, t) \land cP (z, x, t) \to LOC (z, y, t)$
$+$	$a_{b}$ 83	bao	$x : :_{t} i d c n t \land \neg (x : :_{t} s r e g) \land y : :_{t} i d c n t \land \neg (y : :_{t} s r e g) \land cP (x, y, t) \to LOC (x, y, t)$
	$a_{b}$ 84	vvo	$stREG (x, y) \to (x : :_{} p r o c \lor x : :_{} p b n d) \land y : :_{} s t r e g$
	$a_{b}$ 85	cvr	$tPROJ (x, y) \to x : :_{} s t r e g \land tm (y)$
	$a_{b}$ 86	blj	$sPROJ (x, y, t) \to x : :_{t} s t r e g \land y : :_{t} s r e g \land tm (t)$
$+$	$a_{b}$ 87	tfw	$OCCIN (x, y) \to (x : :_{} p r o c \lor x : :_{} p b n d) \land (y : :_{} m t e n \lor y : :_{} s i t e)$
	$a_{b}$ 88	qyy	$(x : :_{} p r o c \lor x : :_{} p b n d) \to \exists r (stREG (x, r))$
	$a_{b}$ 89	uqt	$stREG (x, y) \land stREG (x, z) \to y = z$
	$a_{b}$ 90	iqe	$oP (x, y) \land stREG (x, r) \land stREG (y, s) \to oP (r, s)$
	$a_{b}$ 91	kqv	$(x : :_{} p r o c \lor x : :_{} p b n d) \land (y : :_{} p r o c \lor y : :_{} p b n d) \to (oP (x, y) \leftrightarrow \exists r s (stREG (x, r) \land stREG (y, s) \land oP (r, s)))$
	$a_{b}$ 92	fdb	$sPROJ (x, s, t) \land sPROJ (x, r, t) \to s = r$
	$a_{b}$ 93	geq	$x : :_{t} s t r e g \to \exists s t^{'} (tP (t^{'}, t) \land sPROJ (x, s, t^{'}))$
	$a_{b}$ 94	txf	$x : :_{} s t r e g \land y : :_{} s t r e g \to (oP (x, y) \leftrightarrow \exists t u (tPROJ (x, t) \land tPROJ (y, u) \land tP (t, u)) \land \forall v (EX (x, v) \to \exists w s r (tP (w, v) \land sPROJ (x, s, w) \land sPROJ (y, r, w) \land cP (s, r, w))))$
$+$	$a_{b}$ 95	dxv	$OCCIN (x, y) \land EX (x, t) \to EX (y, t)$
°	$a_{b}$ 96	jil	$OCCIN (x, y) \land oP (z, x) \to OCCIN (z, y)$
°	$a_{b}$ 97	czc	$OCCIN (x, y) \land \forall t (EX (x, t) \leftrightarrow cP (y, z, t)) \to OCCIN (x, z)$
$+$	$a_{b}$ 98	yex	$OCCIN (x, y) \land \forall t (EX (x, t) \leftrightarrow LOC (y, z, t)) \to OCCIN (x, z)$
$+$	$a_{b}$ 99	kkl	$SDEP (x, y) \to x : :_{} s d c n t \land (y : :_{} s d c n t \lor (y : :_{} i d c n t \land \neg (y : :_{} s r e g)))$
$+$	$a_{b}$ 100	nfe	$SDEP (x, y) \to \neg \exists t (cO (x, y, t))$
$+$	$a_{b}$ 101	myu	$SDEP (x, y) \land SDEP (y, z) \land x \neq z \to SDEP (x, z)$
$+$	$a_{b}$ 102	iyu	$SDEP (x, y) \to \exists t (EX (x, t) \land EX (y, t)) \land \forall t (EX (x, t) \to EX (y, t))$
$+$	$a_{b}$ 103	ilw	$x : :_{t} i d c n t \leftrightarrow x : :_{t} c n t \land \neg \exists y t^{'} (SDEP (x, y) \lor GDEP (x, y, t^{'}))$
$+$	$a_{b}$ 104	akq	$x : :_{t} s d c n t \leftrightarrow x : :_{t} c n t \land \exists y (y : :_{t} i d c n t \land \neg (y : :_{t} s r e g) \land SDEP (x, y))$
°	$a_{b}$ 105	rog	$CONCR (x, y, t) \to (x : :_{t} s d c n t \lor x : :_{t} p r o c) \land y : :_{t} g d c n t \land tm (t)$
$+$	$a_{b}$ 106	ekp	$GDEP (x, y, t) \to x : :_{t} g d c n t \land y : :_{t} i d c n t \land \neg (y : :_{t} s r e g) \land tm (t)$
$+$	$a_{b}$ 107	ibk	$x : :_{t} g d c n t \to \exists y t^{'} (tP (t^{'}, t) \land CONCR (y, x, t^{'}))$
$+$	$a_{b}$ 108	nyz	$CONCR (x, y, t) \land tP (t^{'}, t) \to CONCR (x, y, t^{'})$
$+$	$a_{b}$ 109	otx	$GDEP (x, y, t) \to \exists z t^{'} (tP (t^{'}, t) \land INH (z, y) \land CONCR (z, x, t^{'}))$
$+$	$a_{b}$ 110	cik	$CONCR (x, y, t) \land INH (x, z) \to GDEP (y, z, t)$
°	$a_{b}$ 111	fmm	$x : :_{t} g d c n t \land PTC (x, p, t) \to \exists y t^{'} (tP (t^{'}, t) \land CONCR (y, x, t^{'}) \land ((y : :_{t^{'}} s d c n t \land \exists z (SDEP (y, z) \land PTC (z, p, t^{'}))) \lor (oP (y, p) \land EX (y, t^{'}))))$
$+$	$a_{b}$ 112	ild	$PTC (x, y, t) \to x : :_{t} c n t \land \neg (x : :_{t} s r e g) \land y : :_{t} p r o c \land tm (t)$
°	$a_{b}$ 113	trl	$x : :_{t} p r o c \to \exists y (PTC (y, x, t))$
$+$	$a_{b}$ 114	yjm	$PTC (x, y, t) \land tP (t^{'}, t) \to PTC (x, y, t^{'})$
$+$	$a_{b}$ 115	cgn	$x : :_{t} s d c n t \land PTC (x, p, t) \to \exists y t^{'} (tP (t^{'}, t) \land y : :_{t^{'}} i d c n t \land \neg (y : :_{t^{'}} s r e g) \land SDEP (x, y) \land PTC (y, p, t^{'}))$
	$a_{b}$ 116	rph	$HIST (x, y) \to x : :_{} h i s t \land y : :_{} m t e n$
	$a_{b}$ 117	zek	$HIST (x, y) \land HIST (x, z) \to y = z$
	$a_{b}$ 118	woe	$HIST (x, z) \land HIST (y, z) \to x = y$
	$a_{b}$ 119	vvy	$x : :_{t} h i s t \to \exists y (HIST (x, y))$
	$a_{b}$ 120	okt	$x : :_{t} m t e n \to \exists y (HIST (y, x))$
	$a_{b}$ 121	lga	$HIST (x, y) \land EX (y, t) \to PTC (y, x, t)$
	$a_{b}$ 122	uzz	$HIST (x, y) \to (EX (x, t) \leftrightarrow EX (y, t))$
	$a_{b}$ 123	oot	$REAL (x, y) \to x : :_{} p r o c \land y : :_{} r l z e n$
	$a_{b}$ 124	grx	$REAL (x, y) \land INH (y, z) \to \exists t (PTC (z, x, t))$

The Theory $D$ and Axiom Preservation from $B_{d}$

$+$	$a_{d}$ 1	$P (x, y) \to (ab (x) \land ab (y)) \lor (pd (x) \land pd (y))$
$+$	$a_{d}$ 2	$P (x, y) \to (t (x) \leftrightarrow t (y))$
$+$	$a_{d}$ 3	$P (x, y) \to (s (x) \leftrightarrow s (y))$
$+$	$a_{d}$ 4	$(ab (x) \lor pd (x)) \to P (x, x)$
$+$	$a_{d}$ 5	$P (x, y) \land P (y, x) \to x = y$
$+$	$a_{d}$ 6	$P (x, y) \land P (y, z) \to P (x, z)$
°	$a_{d}$ 7	$(ab (x) \lor pd (x)) \land \neg P (x, y) \to \exists z (P (z, x) \land \neg O (z, y))$
$\sim$	$a_{d}$ 8	$D Q T (x, y) \to (tq (x) \land pd (y)) \lor (pq (x) \land ped (y)) \lor (aq (x) \land nped (y))$ [ $D Q T (x, y) \to pq (x) \land ped (y)$ ]
°	$a_{d}$ 9	$D Q T (x, y) \land D Q T (x, z) \to y = z$
$+$	$a_{d}$ 10	$q (x) \to \exists y (D Q T (x, y))$
°	$a_{d}$ 11	$pd (x) \leftrightarrow \exists y (D Q T (y, x) \land tl (y))$
°	$a_{d}$ 12	$ped (x) \leftrightarrow \exists y (D Q T (y, x) \land sl (y))$
	$a_{d}$ 13	$Q L (x, y) \to tr (x) \land tq (y)$
	$a_{d}$ 14	$tq (x) \to \exists y (Q L (y, x))$
	$a_{d}$ 15	$Q L (x, y) \land t (x) \to tl (y)$
	$a_{d}$ 16	$tl (x) \to \exists y (t (y) \land Q L (y, x))$
	$a_{d}$ 17	$Q L (x, y) \land Q L (z, y) \land t (x) \land t (z) \to x = z$
$+$	$a_{d}$ 18	$T L C (x, t) \to (ed (x) \lor pd (x) \lor q (x)) \land t (t)$
°	$a_{d}$ 19	$(ed (x) \lor pd (x) \lor q (x)) \to \exists t (T L C (x, t))$
$+$	$a_{d}$ 20	$T L C (x, t) \land T L C (x, u) \to t = u$
$+$	$a_{d}$ 21	$P (x, y) \land T L C (x, t) \land T L C (y, u) \to P (t, u)$
$+$	$a_{d}$ 22	$D Q T (x, y) \land T L C (x, t) \land T L C (y, u) \to P (t, u)$
	$a_{d}$ 23	$pd (x) \to (T L C (x, t) \leftrightarrow \exists y (D Q T (y, x) \land Q L (t, y) \land t (t)))$
	$a_{d}$ 24	$sl (x) \land D Q T (x, y) \land T L C (x, t) \land T L C (y, u) \to t = u$
	$a_{d}$ 25	$t Q L (x, y, t) \to ((pr (x) \land pq (y)) \lor (ar (x) \land aq (y))) \land t (t)$
	$a_{d}$ 26	$t Q L (x, y, t) \to P R E (y, t)$
	$a_{d}$ 27	$(pq (x) \lor aq (x)) \land P R E (x, t) \to \exists y (t Q L (y, x, t))$
	$a_{d}$ 28	$t Q L (x, y, t) \land P (u, t) \to \exists z (t Q L (z, y, u) \land P (z, x))$
	$a_{d}$ 29	$t Q L (x, y, t) \land s (x) \to sl (y)$
	$a_{d}$ 30	$sl (x) \land P R E (x, t) \to \exists y (s (y) \land t Q L (y, x, t))$
	$a_{d}$ 31	$t Q L (x, y, t) \land t Q L (z, y, t) \land s (x) \land s (z) \to x = z$
$+$	$a_{d}$ 32	$t P (x, y, t) \to ed (x) \land ed (y) \land t (t)$
°	$a_{d}$ 33	$t P (x, y, t) \to P R E (x, t) \land P R E (y, t)$
$+$	$a_{d}$ 34	$t P (x, y, t) \land P (u, t) \to t P (x, y, u)$
°	$a_{d}$ 35	$t P (x, y, t) \land t P (x, y, u) \land S U M (s, t, u) \to t P (x, y, s)$
°	$a_{d}$ 36	$ed (x) \land P R E (x, t) \to t P (x, x, t)$
$+$	$a_{d}$ 37	$t P (x, y, t) \land t P (y, z, t) \to t P (x, z, t)$
°	$a_{d}$ 38	$ed (x) \land ed (y) \land P R E (x, t) \land P R E (y, t) \land \neg t P (x, y, t) \to \exists z (t P (z, x, t) \land \neg t O (z, y, t))$
$+$	$a_{d}$ 39	$ped (x) \leftrightarrow \exists y t (t P (y, x, t)) \land \forall y t (t P (y, x, t) \to ped (y))$
°	$a_{d}$ 40	$nped (x) \leftrightarrow \exists y t (t P (y, x, t)) \land \forall y t (t P (y, x, t) \to nped (y))$
	$a_{d}$ 41	$as (x) \to \exists y z u t (t P (y, x, t) \land ped (y) \land t P (z, x, u) \land nped (z))$
	$a_{d}$ 42	$m (x) \land t P (y, x, t) \land P R E (x, u) \to t P (y, x, u)$
	$a_{d}$ 43	$K (x, y, t) \to t (t) \land ((ped (x) \land ped (y)) \lor (nped (x) \land nped (y)) \lor (pd (x) \land pd (y)))$
	$a_{d}$ 44	$K (x, y, t) \to P R E (x, t) \land P R E (y, t)$
	$a_{d}$ 45	$K (x, y, t) \land P (u, t) \to K (x, y, u)$
	$a_{d}$ 46	$K (x, y, t) \land K (x, y, u) \land S U M (s, t, u) \to K (x, y, s)$
	$a_{d}$ 47	$K (x, y, u) \land P R E (y, t) \to \exists z v (P (v, t) \land K (z, y, v))$
	$a_{d}$ 48	$K (x, y, t) \to \neg K (y, x, t)$
	$a_{d}$ 49	$K (x, y, t) \land K (y, z, t) \to K (x, z, t)$
	$a_{d}$ 50	$K (x, y, t) \land t P P (z, y, t) \to \exists w (t P P (w, x, t) \land K (w, z, t))$
	$a_{d}$ 51	$K (x, y, t) \land K (z, y, t) \to (x = z \lor K (x, z, t) \lor K (z, x, t))$
$+$	$a_{d}$ 52	$P C (x, y, t) \to ed (x) \land pd (y) \land t (t)$
°	$a_{d}$ 53	$P C (x, y, t) \to P R E (x, t) \land P R E (y, t)$
$+$	$a_{d}$ 54	$P C (x, y, t) \land P (u, t) \to P C (x, y, u)$
°	$a_{d}$ 55	$P C (x, y, t) \land P C (x, y, u) \land S U M (s, t, u) \to P C (x, y, s)$
°	$a_{d}$ 56	$pd (x) \land P R E (x, t) \to \exists y u (P (u, t) \land P C (y, x, u))$
°	$a_{d}$ 57	$ed (x) \land P R E (x, t) \to \exists y u (P (u, t) \land P C (x, y, u))$
°	$a_{d}$ 58	$P C (x, y, t) \land P (y, z) \to P C (x, z, t)$
°	$a_{d}$ 59	$E X D (x, y, t) \to P R E (x, t) \land P R E (y, t)$
°	$a_{d}$ 60	$E X D (x, y, t) \land P (u, t) \to E X D (x, y, u)$
°	$a_{d}$ 61	$E X D (x, y, t) \land E X D (x, y, u) \land S U M (s, t, u) \to E X D (x, y, s)$
°	$a_{d}$ 62	$E X D (x, y, u) \land P R E (x, t) \to \exists z v (P (v, t) \land E X D (x, z, v))$
	$a_{d}$ 63	$K (x, y, t) \to E X D (y, x, t)$
$+$	$a_{d}$ 64	$P C (x, y, t) \to E X D (x, y, t) \land E X D (y, x, t)$
°	$a_{d}$ 65	$D Q T (x, y) \to S D (x, y)$
°	$a_{d}$ 66	$nped (x) \land P R E (x, t) \to \exists y u (ped (y) \land P (u, t) \land E X D (x, y, u))$
	$a_{d}$ 67	$mob (x) \to \exists y (apo (y) \land S D (x, y))$
	$a_{d}$ 68	$naso (x) \land P R E (x, t) \to \exists y u (sc (y) \land P (u, t) \land E X D (x, y, u))$
	$a_{d}$ 69	$sc (x) \land P R E (x, t) \to \exists y u (sag (y) \land P (u, t) \land K (y, x, u))$
	$a_{d}$ 70	$sag (x) \land P R E (x, t) \to \exists y u (apo (y) \land P (u, t) \land E X D (x, y, u))$
	$a_{d}$ 71	$f (x) \land P R E (x, t) \to \exists y u (napo (y) \land P (u, t) \land E X D (x, y, u))$
	$a_{d}$ 72	$apo (x) \land P R E (x, t) \to \exists y u (napo (y) \land P (u, t) \land K (y, x, u))$
	$a_{d}$ 73	$napo (x) \land P R E (x, t) \to \exists y u (m (y) \land P (u, t) \land K (y, x, u))$
$\sim$	$a_{d}$ 74	$S L C (x, s, t) \to ((ed (x) \land \neg as (x)) \lor pq (x) \lor pd (x)) \land s (s)$ [ $S L C (x, s, t) \to (ed (x) \lor pq (x) \lor pd (x)) \land s (s)$ ]
°	$a_{d}$ 75	$S L C (x, s, t) \to P R E (x, t)$
$+$	$a_{d}$ 76	$S L C (x, s, t) \land S L C (x, r, t) \to s = r$
$+$	$a_{d}$ 77	$S L C (x, s, u) \land S L C (x, r, t) \land P (u, t) \to P (s, r)$
°	$a_{d}$ 78	$S L C (x, s, u) \land P R E (x, t) \to \exists r (S L C (x, r, t))$
	$a_{d}$ 79	$ped (x) \to (S L C (x, s, t) \leftrightarrow \exists y (D Q T (y, x) \land sl (y) \land t Q L (s, y, t)))$
	$a_{d}$ 80	$pq (x) \to (S L C (x, s, t) \leftrightarrow \exists y (D Q T (x, y) \land S L C (y, s, t)))$
$+$	$a_{d}$ 81	$nped (x) \land S L C (x, s, t) \to \exists y (ped (y) \land E X D (x, y, t) \land S L C (y, s, t))$
°	$a_{d}$ 82	$P C (x, y, t) \land S L C (x, s, t) \to \exists r (S L C (y, r, t))$
$+$	$a_{d}$ 83	$P C (x, y, t) \land S L C (x, r, t) \land S L C (y, s, t) \to P (r, s)$
°	$a_{d}$ 84	$t P (x, y, t) \land S L C (x, s, t) \to \exists r (S L C (y, r, t))$
$+$	$a_{d}$ 85	$t P (x, y, t) \land S L C (x, r, t) \land S L C (y, s, t) \to P (r, s)$
°	$a_{d}$ 86	$P (x, y) \land S L C (x, s, t) \to \exists r (S L C (y, r, t))$
$+$	$a_{d}$ 87	$P (x, y) \land S L C (x, r, t) \land S L C (y, s, t) \to P (r, s)$
	$a_{d}$ 88	$K (x, y, t) \to \forall s (S L C (x, s, t) \leftrightarrow S L C (y, s, t))$

References

Arp

Smith

Spear

A. D.

(2015). Building ontologies with basic formal ontology. The MIT Press.

Borgo

Ferrario

Gangemi

Guarino

Masolo

Porello

Sanfilippo

E. M.

Vieu

(2022a). DOLCE: A descriptive ontology for linguistic and cognitive engineering. Applied Ontology, 17(1), 45–69.

Borgo

Galton

Kutz

(2022b). Foundational ontologies in action. Applied Ontology, 17(1), 1–16.

Chui

Grüninger

(2014). Merging the dolce and psl upper ontologies. In Proceedings of the international joint conference on knowledge discovery, knowledge engineering and knowledge management - volume 2, IC3K 2014, (pp. 16–26). SCITEPRESS - Science and Technology Publications.

Euzenat

Shvaiko

(2013). Ontology matching. Berlin, Heidelberg: Springer.

Fernández-López

Gomez-Perez

Juristo

(1997). Methontology: From ontological art towards ontological engineering. Engineering Workshop on Ontological Engineering (AAAI97), AAAI Technical Report SS-97-06, 33–40.

Gardner

S. P.

(2005). Ontologies and semantic data integration. Drug Discovery Today, 10(14), 1001–1007.

Grenon

Smith

Goldberg

(2004). Biodynamic ontology: Applying bfo in the biomedical domain. Studies in Health Technology and Informatics, 102, 20–38.

Guarino

(2017). BFO and DOLCE: So far, so close.... Cosmos+Taxis, 4(4), 10–18.

10.

ISO 21838-2 (2021). Information technology – top-level ontologies (tlo) – part 2: Basic formal ontology. Standard ISO/IEC 21838-2:2021, International Organization for Standardization, Geneva, CH.

11.

ISO 21838-3 (2023). Information technology – top-level ontologies (tlo) – part 3: Descriptive ontology for linguistic and cognitive engineering (dolce). Standard ISO/IEC 21838-3:2023, International Organization for Standardization, Geneva, CH.

12.

ISO 24707 (2007). Information technology – common logic (cl): A framework for a family of logic-based languages. Standard ISO/IEC 24707:2007, International Organization for Standardization, Geneva, CH.

13.

Jarrar

Meersman

(2009). Ontology engineering – The DOGMA approach. In T. S. Dillon, E. Chang, R. Meersman, & K. Sycara (Eds.), Advances in web semantics I: Ontologies, web services and applied semantic web (pp. 7–34). Springer. https://doi.org/10.1007/978-3-540-89784-2_2.

14.

Masolo

Borgo

Gangemi

Guarino

Oltramari

(2003). WonderWeb deliverable D18: Ontology library. Technical report, CNR.

15.

Masolo

Zaccarini

F. A.

Compagno

Borgo

Ghedini

Guarino

Sanfilippo

E. M.

Biccheri

(2023). OntoCommons deliverable D2.7: Top reference ontology final release. Technical report, CNR.

16.

Otte

J. N.

Beverley

Ruttenberg

(2022). BFO: Basic formal ontology. Applied Ontology, 17(1), 17–43.

17.

Ouksel

Sheth

(1999). Semantic interoperability in global information systems: A brief introduction to the research area and the special section. SIGMOD Record, 28, 5–12.

18.

Smith

Almeida

Bona

Brochhausen

Ceusters

Courtot

Dipert

Goldfain

Grenon

Hastings

Hogan

Jacuzzo

Johansson

Mungall

Natale

Neuhaus

Overton

Petosa

Rovetto

Ruttenberg

Ressler

Rudniki

Seppala

Schulz

Zheng

(2020). Basic formal ontology 2020 - specification and user’s guide (revised version from september 9, 2020). Technical report.

19.

Suárez-Figueroa

M. C.

Gómez-Pérez

Fernández-López

(2012). The NeOn methodology for ontology engineering. In M. C. Suárez-Figueroa, A. Gómez-Pérez, E. Motta, & A. Gangemi (Eds.), Ontology engineering in a networked world (pp. 9–34). Springer. https://doi.org/10.1007/978-3-642-24794-1_2.

20.

Sutcliffe

(2016). The CADE ATP system competition - CASC. AI Magazine, 37(2), 99–101.

21.

Van Benthem

(1983). The logic of time. Kluwer Academic Publisher.

22.

W3C OWL Working Group (2012). OWL 2 web ontology language document overview (second edition).

$D Q T (x, y)$	$x$ is a direct quality of $y$
$E X D (x, y, t)$	$x$ is existentially dependent on $y$ at time $t$
$K (x, y, t)$	$x$ constitutes $y$ at time $t$
$P (x, y)$	$x$ is part of $y$
$P C (x, y, t)$	$x$ participates in $y$ at time $t$
$Q L (x, y)$	$x$ is the immediate quale of $y$
$S L C (x, y, t)$	$x$ is (exactly) located at space $y$ at time $t$
$T L C (x, t)$	$x$ is (exactly) located at time $t$
$t P (x, y, t)$	$x$ is part of $y$ at time $t$
$t Q L (x, y, t)$	$x$ is the temporary quale of $y$ at time $t$

$ab$	Abstract	$ped$	Physical Endurant
$acc$	Accomplishment	$pob$	Physical Object
$ach$	Achievement	$pq$	Physical Quality
$apo$	Agentive Physical Object	$pr$	Physical Region
$aq$	Abstract Quality	$pro$	Process
$ar$	Abstract Region	$q$	Quality
$as$	Arbitrary Sum	$r$	Region
$aso$	Agentive Social Object	$s$	Space Region
$ed$	Endurant	$sag$	Social Agent
$ev$	Event	$sc$	Society
$f$	Feature	$sob$	Social Object
$m$	Amount Of Matter	$sl$	Spatial Location
$mob$	Mental Object	$st$	State
$napo$	Non-agentive Physical Object	$stv$	Stative
$naso$	Non-agentive Social Object	$t$	Time Interval
$nped$	Non-physical Endurant	$tq$	Temporal Quality
$npob$	Non-physical Object	$tl$	Temporal Location
$pd$	Perdurant	$tr$	Temporal Region