Representing a reference foundational ontology of events in SROIQ

Abstract

In recent years, there has been a growing interest in the application of foundational ontologies, i.e., formal ontological theories in the philosophical sense, to provide a theoretically sound foundation for improving the theory and practice of conceptual modeling and knowledge representation. This paper addresses one particular foundational theory of events termed UFO-B, which has been successfully employed as a reference model for addressing problems from complex media management, enterprise architecture, software engineering, and modeling of events in petroleum exploration. Despite its success, there is still no formalization of UFO-B in a decidable knowledge representation language that could support reasoning about complex events and event relations. We address this gap by proposing a number of alternative translations from UFO-B’s original axiomatization (in first-order logic and in the Alloy formal language) to the description logic $SROIQ$ , which is the formal underpinning of OWL 2 DL. Additionally, to support practical applications, we translated these $SROIQ$ theories to OWL 2 DL TBoxes, which were validated by showing that all the intended models of UFO-B (the logical models of the UFO-B specification in Alloy) that we generated are consistent with these UFO-B TBoxes. In a sense, the specification in Alloy implements the specification in first-order logic, while the OWL 2 TBoxes implement the $SROIQ$ specifications. Incidentally, the methodology that we designed for the translation from UFO-B’s original axiomatization in FOL and Alloy to $SROIQ$ came to be a key contribution of this work by providing us evidence of the inadequacy of DLs for the specification of comprehensive foundational ontologies.

Keywords

Ontology of Events Description Logics SROIQ OWL SAT

1. Introduction

The theory and practice of conceptual modeling and knowledge representation can be improved by means of specially designed foundational ontologies (i.e., formal ontological theories in the philosophical sense), which can provide a theoretically sound foundation for the modeling constructs and methodologies of the languages developed in these fields. Foundational ontologies used for these purposes address a number of pervasive domain-independent notions including objects, properties, relations, qualities, and events. The latter ontological category enlarges the variety of entities in the world to include not only its “ordinary citizens” (such as animals, physical objects) but also the “things that happen to or are performed by them” (Casati and Varzi, 2015).

Dealing with the representation of events is key to conceptual modeling and knowledge representation, given the importance of events in cognition, language and, in fact, a large part of human endeavor, which is focused on planning and executing actions, effectively bringing about changes in the world. This has motivated the development of a particular philosophically well-founded ontology of events termed Unified Foundational Ontology – Part B (UFO-B) (Guizzardi et al., 2013). It accounts for events as manifestations of object dispositions, and explicates how objects, situations and events relate to each other.

The latest version of UFO-B (Guizzardi et al., 2013) has been extensively tested in practice and successfully employed as a reference model for addressing problems from enterprise architecture (Santos et al., 2010; Nardi et al., 2014; Azevedo et al., 2015) and software engineering (Guizzardi et al., 2014; Duarte et al., 2016; de Souza et al., 2017). Earlier versions of UFO-B (Guizzardi et al., 2008; Guizzardi and Wagner, 2004) have also been employed in areas such as complex media management (Pena, 2012; Carolo and Burlamaqui, 2011) and the modeling of events in petroleum exploration (Werlang, 2015). Despite that, there is still no formalization of this ontology in terms of a decidable knowledge representation language that could support reasoning about complex events and event relations. In this paper, we address this gap by proposing a number of translations from UFO-B’s original axiomatization (in first-order logic (FOL) and in the Alloy formal language (Jackson, 2012)) to the Description Logic (DL) $SROIQ$ (Horrocks et al., 2006), which is the formal underpinning of the OWL 2 Web Ontology Language (OWL 2 DL) (W3C, 2012). We employ the specification of UFO-B in Alloy as an implementation of the UFO-B FOL theory, and the specifications of UFO-B in OWL 2 DL as implementations of the specifications of UFO-B in $SROIQ$ . By using these technologies, we aim to support the practical application of the foundational ontology UFO-B for knowledge representation in the Semantic Web and to enable decidable reasoning about events based on the well-founded ontology UFO-B.

Incidentally, the methodology that we designed for the translation from UFO-B’s original axiomatization in FOL and Alloy to $SROIQ$ came to be a key contribution of this work by providing us evidence of the inadequacy of DLs for the specification of comprehensive foundational ontologies. Therefore, while the final artifact – a collection of UFO-B formalizations in $SROIQ$ – is a core contribution of this paper, the methodology that we used to build this artifact is also worth presenting and occupies a large part of this article.

The remainder of this paper is structured as follows. Section 2 briefly introduces the challenges of dealing with $SROIQ$ , and presents an overview of our methodology for translating a FOL theory to $SROIQ$ . In Section 3, we present the formalization of UFO-B in FOL. Section 4 shows a translation of the UFO-B FOL theory to a set of $SROIQ$ axioms, discussing the challenges in mapping these two formalisms. In Section 5, we explain the structural restrictions of $SROIQ$ (two syntactic constraints that guarantee decidability) and show that the full set of $SROIQ$ axioms (of Section 4) violates these restrictions. We then discuss the incompatibilities between the various UFO-B $SROIQ$ axioms, showing an encoding of these incompatibilities in propositional logic and the solutions of the related propositional satisfiability problem (SAT), which define 12288 UFO-B $SROIQ$ theories that do not violate the $SROIQ$ restrictions. In Section 6, these 12288 theories are evaluated by means of codifications in OWL 2 DL, on which consistency tests are performed regarding a set of automatically generated intended models of UFO-B (logical models of the UFO-B specification in Alloy). This shows that the codifications do not rule out these intended models. Section 7 discusses some related work, while Section 8 presents some final considerations.

This paper follows the same methodology applied by Benevides et al. (2017), but extends their results by (1) performing an ontological analysis of the UFO-B $SROIQ$ theories (see Section 5.5), and (2) complementing UFO-B with a more comprehensive presentation and philosophical justification of sub-theories dealing with: (i) the differentiation of roles played by objects inside an event (the so-called processual roles (Loebe, 2007, 2003), see Section 3.7); (ii) qualities and quality structures used to predicate qualitative aspects to events (see Section 3.8); (iii) particular aspects of events of the creation, destruction and modification of objects (see Section 3.9).

2. Challenges and methodology

When creating ontologies, there is a trade-off between being faithful to the domain being captured and guaranteeing desirable computational properties, e.g., decidability and tractability of reasoning. A common approach in ontology engineering is to first employ a highly-expressive formal language, like FOL, to create a theory that captures the domain of interest as well as possible. Such a theory is called a reference ontology. The focus of a reference ontology is on representation adequacy: the resulting specifications are intended to be used by humans in tasks such as communication, domain analysis and problem-solving. In this case, an important quality of a reference ontology is its precision, i.e., its ability to rule out unintended models, requiring thus expressiveness of the formalism employed. Then, one can employ a less expressive formalism, like $SROIQ$ , to (often partially) capture a reference ontology as artifacts with desirable computational properties. These artifacts are called lightweight ontologies (Guizzardi, 2006, pp. 36–37).

The goal here is to have $SROIQ$ formalizations of UFO-B. For building these theories, we have to deal with the difference in expressivity between FOL and $SROIQ$ . Moreover, while the scope of syntactic constraints in FOL concerns individual formulae, $SROIQ$ also has syntactic constraints encompassing the whole theory/ontology, the so-called structural restrictions (Krötzsch et al., 2012, p. 9). The two structural restrictions – regularity and simplicity – do not concern each single axiom per se, but the structure of the ontology as a whole. These restrictions guarantee that the reasoning algorithms are correct and terminating (Krötzsch et al., 2012, p. 9). In particular, they guarantee that the satisfiability problem of $SROIQ$ -concepts is decidable (Horrocks et al., 2006, pp. 58, 59).

Concerning the methodology we designed for the translation from FOL to $SROIQ$ , we first perform an unrestricted mapping of the reference ontology. More specifically, we build a set $T$ (read “calligraphic-T”) of $SROIQ$ formulae disconsidering the structural restrictions of $SROIQ$ . We call $T$ the unstructured set of UFO-B $SROIQ$ axioms. In later sections, we argue that $T$ does not fully capture UFO-B because some UFO-B FOL axioms are not expressible in $SROIQ$ (even by disconsidering the structural restrictions).

Next, we show that $T$ disobeys both structural restrictions of $SROIQ$ (viz., regularity and simplicity). The incompatibilities between axioms in $T$ can be expressed in propositional logic by capturing rules like “the inclusion of axiom (ai) implies the exclusion of axiom (aj).” We call “ $I$ ” the set of all incompatibility rules expressed in propositional logic.

Then, we use a SAT solver to find all subsets of $T$ that obey the incompatibility rules and thus ensure both regularity and simplicity. We call them structured subsets of $T$ . Solving the SAT problem, we find 6757902900 structured subsets of $T$ , many of which are not maximal w.r.t. being structured, i.e., to obeying regularity and simplicity.1

¹
A subset of $T$ is maximal w.r.t. obeying regularity and simplicity if and only if (iff) the inclusion of any other axiom generates a subset that is not a $SROIQ$ ontology due to disobeying the regularity or simplicity restrictions.

Such structural non-maximality means that the subset of

T

arbitrarily excludes axioms from UFO-B, losing precision without a reasonable computational justification. Because of this, we are interested in finding the maximally structured subsets, each of which we consider as a possible representation of UFO-B in

SROIQ

. We show that there are 12288 of such maximally structured subsets. As we discuss later (Section 5.5), selecting one particular subset involves sacrificing one or more axioms of UFO-B.

In order to automate the previous steps, we built a tool that, given a textual representation of $T$ , derives the incompatibility rules and returns all the maximally structured subsets of $T$ .

We check these maximally structured subsets of $T$ by (i) codifying the full UFO-B in Alloy; and (ii) codifying each of the 12288 theories as a terminology box (TBox) in OWL 2 DL. Then, (iii) we use the Alloy Analyzer2

https://github.com/AlloyTools/org.alloytools.alloy/releases.

tool to generate a number of models of the full UFO-B Alloy codification; these models can be seen as intended models of UFO-B. (iv) each generated model is then transformed to an OWL 2 DL individual assertion box (ABox). (v) by joining each one of the 12288 TBoxes with each generated ABox, we build a number of OWL 2 DL knowledge base (KBs), on which consistency tests are performed and yield positive results without any exceptions.

3. The formalization of UFO-B in FOL

First, we present some notational conventions: (i) FOL predicates and functions, and DL concepts and roles are denoted in Uppercase typewriter style, e.g., “Person” and “motherOf;” (ii) we employ restricted quantification à la Frege, i.e., “ $\forall x : T (φ)$ ” is a schema for “ $\forall x (T (x) \to φ)$ ,” and “ $\exists x : T (φ)$ ” is a schema for “ $\exists x (T (x) \land φ))$ ;” and (iii) we keep the indexes of the UFO-B formulae originally presented in Guizzardi et al. (2013), appending a prime symbol “ ′ ” to the index whenever we revise such a formula.

UFO-B extended the Unified Foundational Ontology (UFO-A; Guizzardi, 2005) to deal with events. Besides the FOL formalization, Guizzardi et al. (2013) also indicated a publicly available Alloy axiomatization that also formalized subjects not contemplated in that paper. In this section, we present an updated version of UFO-B that also formalizes those subjects. Here, we homogenized the names of relations defined in the original presentation of UFO-B (Guizzardi et al., 2013) by expanding abbreviations and replacing the forms “x-y” or “x_y” with “xY”.

UFO-B is composed of the following sub-theories: the instantiation of universals by individuals (Section 3.1); a definition of a parthood relation for events (Section 3.2); an explanation of the nature of events as manifestations of objects’ dispositions (Section 3.3); constraints on how objects participate in events, and how events depend on objects (Section 3.4); a suggestion of a linear time structure in order to discuss temporal constraints related to event parthood (Section 3.5); the view of events as the entities responsible for world changes, a sort of transition between situations (Section 3.6); the differentiation of roles played by objects inside an event (the so-called processual roles, Section 3.7); qualities and quality structures used to predicate qualitative aspects to events (Section 3.8); and particular aspects of events of the creation, destruction and modification of objects (Section 3.9).

Fig. 1.

Universals and individuals.

3.1. Universals and individuals: (U1)–(U5)

First of all, according to UFO-A, a Thing can be either a Set or an Urelement.3

³
In simple words, an urelement is something that can be an element of a set, but is not a set itself.

An Urelement can be either an Individual or a Universal (Guizzardi, 2005, Fig. 6–12), meaning that Universals are reified in the domain of quantification of our first-order theory (see Fig. 1). Usually, the instantiation relation from Individuals to Universals is temporalized, being able to capture accidental facts like “I am awake now.” However, representing temporally changing information in Description Logic based languages is usually not a trivial task, as there are many possible strategies with different trade-offs (see Zamborlini and Guizzardi (2010); Bourguet et al. (2017)). For this reason, here we employ a (less expressive) atemporal instantiation relation. Such a reduction in expressivity is not a problem for this work because: (i) Events instantiate EventUniversals rigidly, where by (temporal) rigidity we mean that if there is a time t in which x instantiates u, then throughout the occurrence/existence of x, x instantiates u; (ii) while an Object can obviously cease to play a ProcessualRole – where play is a specialization of instantiates –, the temporal information that is neither contained in plays nor in instantiates can be derived from the Participation event that “grounds” the playing of the ProcessualRole by the Object (see Section 3.7).

We assume the following constraints on the (atemporal) instantiation relation (see Fig. 1). Individuals instantiate at least one Universal. Universals in UFO-A (Guizzardi, 2005, Axiom 22, p. 221) are assumed to satisfy the principle of instantiation (Armstrong, 1989, p. 75), which means that it must be possible (in a modal sense) for a universal to have instances. We approximate this assumption by means of a cardinality constraint on the relation instantiates.

Instead of creating many relations specializing instantiates to constrain the kind of instances a Universal can have, we impose the following constraints on the relation instantiates: (i) a QualityUniversal can only be instantiated by Qualities (U1); (ii) an ObjectUniversal can only be instantiated by Objects (U2); (iii) an EventUniversal can only be instantiated by Events (U3); (iv) a ParticipationUniversal can only be instantiated by Participations (U4). The only possible specialization of instantiates that seems relevant enough to be considered as a genuine relation is plays: all instantiates relationships from Objects to ProcessualRoles are plays relationships (U5). As a theorem, we have that all ProcessualRoles are played by at least one Object (t1) (entailed by the codomain cardinality constraint of instantiates, the subsumption taxonomy, (U2) and (U5)).

$\forall x : Thing, y : QualityUniversal (instantiates (x, y) \to Quality (x))$

$\forall x : Thing, y : ObjectUniversal (instantiates (x, y) \to Object (x))$

$\forall x : Thing, y : EventUniversal (instantiates (x, y) \to Event (x))$

$\forall x : Thing, y : ParticipationUniversal (instantiates (x, y) \to Participation (x))$

$\forall x : Object, y : ProcessualRole (instantiates (x, y) \to plays (x, y))$

$\forall x : ProcessualRole (\exists y : Object (plays (y, x)))$

3.2. Event mereology: (M1)–(M9)

Events may be composed of other Events, e.g., “the murder of Caesar” has as parts “the stabbing of Caesar by Brutus” and “Caesar’s death.” Consider a strict partial order (that is, irreflexive (M3), asymmetric (M4) and transitive (M5)) relation hasPart between events.4

⁴
As noted by Frank Loebe (reviewer), this hasPart relation is neither the parthood relation of UFO-A (which holds between objects) nor a general parthood relation. The (co)domain of hasPart is Event. When unifying UFO-A and UFO-B, hasPart should be renamed to eventHasPart.

An Event is atomic iff it has no parts (M1), and complex otherwise (M2).

$\forall e : Event (AtomicEvent (e) \leftrightarrow \neg \exists e^{'} : Event (hasPart (e, e^{'})))$

$\forall e : Event (ComplexEvent (e) \leftrightarrow \neg AtomicEvent (e))$

$\forall e : ComplexEvent (\neg hasPart (e, e))$

$\forall e, e^{'} : ComplexEvent (hasPart (e, e^{'}) \to \neg hasPart (e^{'}, e))$

$\forall e, e^{'} : ComplexEvent, e^{″} : Event ((hasPart (e, e^{'}) \land hasPart (e^{'}, e^{″})) \to hasPart (e, e^{″}))$

UFO-B has two notions of overlapping: mereological overlapping and temporal overlapping. Here, we call them mereologicallyOverlaps and temporallyOverlaps, respectively. The relation of mereological overlapping is usually reflexive and symmetric, holding also for atoms (Casati and Varzi, 1999, p. 37, (3.1), (3.8), (3.9)). mereologicallyOverlaps is implicitly defined by (M7′), in terms of hasPart, being reflexive and symmetric.

$\forall e, e^{'} : Event ($

$mereologicallyOverlaps (e, e^{'}) \leftrightarrow$

$(e = e^{'} \lor hasPart (e, e^{'}) \lor hasPart (e^{'}, e) \lor \exists e^{″} : Event (hasPart (e, e^{″}) \land hasPart (e^{'}, e^{″}))))$

Fig. 2.

Individuals (based on the figures in Guizzardi et al. (2013)).

UFO-B also commits to weak supplementation (Casati and Varzi, 1999, p. 39, (P.4)): a whole mereologically differs from its proper parts, i.e., a whole must have at least two non-overlapping parts (M6); and strong supplementation (Casati and Varzi, 1999, p. 39, (P.5)) (M8), which yields a theory in which any two different entities cannot have all proper parts in common, as represented by the theorem of extensionality (Casati and Varzi, 1999, p. 40, (3.15)) (our (M9)).

$\forall e : ComplexEvent, e^{'} : Event ($

$hasPart (e, e^{'}) \to \exists e^{″} : Event (hasPart (e, e^{″}) \land \neg mereologicallyOverlaps (e^{'}, e^{″})))$

$\forall e, e^{'} : ComplexEvent ($

$(\forall e^{″} : Event (hasPart (e, e^{″}) \to hasPart (e^{'}, e^{″}))) \to$

$(e = e^{'} \lor hasPart (e^{'}, e)))$

$\forall e, e^{'} : ComplexEvent (e = e^{'} \leftrightarrow \forall e^{″} : Event (hasPart (e, e^{″}) \leftrightarrow hasPart (e^{'}, e^{″})))$

3.3. Events as manifestations of object dispositions: (D1′)–(D9)

AtomicEvents are manifestations of (the inverse of manifestedBy) unique Dispositions (D2). Dispositions inheresIn a unique ConcreteIndividual (D1′). Whenever a Disposition inheresIn an Object and is manifestedBy an Event, the Event dependsOn the Object (D4). An Endurant can be presentIn a Situation (see Fig. 2). A Situation (Section 3.6) triggers an AtomicEvent iff there is a Disposition that is activated by (the inverse of activates) the Situation and that is manifestedBy the Event (D3).5

⁵
Originally, UFO-B assumed that Dispositions inheresIn a unique Object. Here, since we have introduced ConcreteIndividuals and our theory of Situations is quite simple, we are more liberal on the nature of the relation inheresIn. For instance: (i) is the life of an object a manifestation of its disposition to exist in time? (ii) is the holding of a situation from $t_{0}$ to $t_{1}$ a manifestation of its disposition to hold? (iii) is the happening of an event from $t_{0}$ to $t_{1}$ a manifestation of its disposition to happen?

$\forall d : Disposition (\exists! o : ConcreteIndividual (inheresIn (d, o)))$

$\forall e : AtomicEvent (\exists! d : Disposition (manifestedBy (d, e)))$

$\forall s : Situation, e : AtomicEvent ($

$triggers (s, e) \leftrightarrow \exists d : Disposition (activates (s, d) \land manifestedBy (d, e)))$

$\forall d : Disposition, e : AtomicEvent, o : Object ($

$(manifestedBy (d, e) \land inheresIn (d, o)) \to dependsOn (e, o))$

Since UFO-A ensured that Objects bear (the inverse of inheresIn) at least one Trope, here we enforce that both Objects and Events bear at least one Trope (D5). Moreover, since the domain of inheresIn (Trope) is not disjoint from its codomain (ConcreteIndividual), we explicitly assert the asymmetry (D6) and intransitivity of inheresIn (D7).6

⁶

inheresIn is also acyclic, and finite acyclicity can be represented in FOL by means of a little set theory (7 axioms). However, exposing such axioms would deviate the focus of this paper into more technicalities. Nevertheless, we enforced the finite acyclicity of inheresIn in our Alloy codification of UFO-B.

$\forall x : ConcreteIndividual ((Object (x) \lor Event (x)) \to \exists y : Trope (inheresIn (y, x)))$

$\forall c, c^{'} : ConcreteIndividual (inheresIn (c, c^{'}) \to \neg inheresIn (c^{'}, c))$

$\forall c, c^{'}, c^{″} : ConcreteIndividual ((inheresIn (c, c^{'}) \land inheresIn (c^{'}, c^{″})) \to$

$\neg inheresIn (c, c^{″}))$

If a Disposition is manifestedBy an Event, the Disposition is presentIn the Situation that triggers the Event and also in the Situation that the Event bringsAbout (D8). Our point of view is that a Disposition d must temporally exist at the endPoint of its manifestations, being present in some Situation that obtainsIn this TimePoint. This is because we assume that the Event of the destruction of d cannot happen while d is manifesting itself. The closest the destruction of d can get to a manifestation of d is when the endPoint of the manifestation is the beginPoint of the destruction, when d still temporally exists. On the other hand, one could assume that dispositions can manifest themselves while being destructed. In this case, “ $bringsAbout (e, s^{'}) \to presentIn (d, s^{'})$ ” should be removed from (D8). We have no strong objections against this point of view. Finally, the bearer of a Disposition – the entity in which the Disposition inheresIn – is presentIn in all Situations which the Disposition is presentIn (D9).

$\forall e : Event, d : Disposition ($

$manifestedBy (d, e) \to (\forall s, s^{'} : Situation ($

$(triggers (s, e) \to presentIn (d, s)) \land (bringsAbout (e, s^{'}) \to presentIn (d, s^{'})))))$

$\forall d : Disposition, o : Object (inheresIn (d, o) \to$

$(\forall s : Situation (presentIn (d, s) \to presentIn (o, s))))$

3.4. On the participation of objects in events: (P1)–(P5)

Objects participate not only in the AtomicEvents that are manifestations of their Dispositions, but also in the ComplexEvents that have such manifestations as parts. For instance, Caesar participates not only in “Caesar’s death,” but also in “the murder of Caesar.” AtomicEvents dependsOn unique Objects (P1). exclusivelyDependsOn generalizes dependsOn to ComplexEvents, whereas these relations are equivalent on AtomicEvents (P2). By composing the relations hasPart and exclusivelyDependsOn, ComplexEvents exclusivelyDependsOn the Objects that its parts exclusivelyDependsOn (P3). A Participation is an Event that exclusivelyDependsOn a unique Object (P4); this yields an orthogonal way to partition Events that collects all and only the ways a specific Object contributes to the manifestation of the atomic (proper and non-proper) parts of an Event. A participationOf relation from Participations to Objects can be implicitly defined by means of exclusivelyDependsOn (P5).

$\forall e : AtomicEvent \exists! o : Object (dependsOn (e, o))$

$\forall e : AtomicEvent, o : Object (exclusivelyDependsOn (e, o) \leftrightarrow dependsOn (e, o))$

$\forall e : ComplexEvent, o : Object ($

$exclusivelyDependsOn (e, o) \leftrightarrow$

$\forall e^{'} : Event (hasPart (e, e^{'}) \to exclusivelyDependsOn (e^{'}, o)))$

$\forall e : Event (Participation (e) \leftrightarrow \exists! o : Object (exclusivelyDependsOn (e, o)))$

$\forall o : Object, p : Participation ($

$participationOf (p, o) \leftrightarrow exclusivelyDependsOn (p, o))$

3.5. Temporal relations between events: (T1)–(T14′)

The set of TimePoints is totally ordered by the relation precedes (T1)–(T4), and the temporal extension of Events and Situations is described by means of the functional relations beginPoint and endPoint (T5′), (T6′). Allen’s temporal relations (1983), which are not present in Fig. 2, are formalized by means of (T7′)–(T13′). The temporal extent of an Event (improperly) includes the temporal extent of all the (proper) parts of the Event (T14′).

$\forall t : TimePoint (\neg precedes (t, t))$

$\forall t, t^{'} : TimePoint (precedes (t, t^{'}) \to \neg precedes (t^{'}, t))$

$\forall t, t^{'}, t^{″} : TimePoint ((precedes (t, t^{'}) \land precedes (t^{'}, t^{″})) \to precedes (t, t^{″}))$

$\forall t, t^{'} : TimePoint ((t \neq t^{'}) \to (precedes (t, t^{'}) \lor precedes (t^{'}, t)))$

$\forall e : Event \exists! t, t^{'} : TimePoint (beginPoint (e, t) \land endPoint (e, t^{'}))$

$\forall e : Event, t, t^{'} : TimePoint ((beginPoint (e, t) \land endPoint (e, t^{'})) \to precedes (t, t^{'}))$

$\forall e, e^{'} : Event (before (e, e^{'}) \leftrightarrow$

$\exists t, t^{'} : TimePoint (endPoint (e, t) \land beginPoint (e^{'}, t^{'}) \land precedes (t, t^{'}))$

$\forall e, e^{'} : Event (meets (e, e^{'}) \leftrightarrow \exists t : TimePoint (endPoint (e, t) \land beginPoint (e^{'}, t)))$

$\forall e, e^{'} : Event (temporallyOverlaps (e, e^{'}) \leftrightarrow$

$\exists t_{0}, \dots, t_{3} : TimePoint (beginPoint (e, t_{0}) \land beginPoint (e^{'}, t_{1}) \land$

$endPoint (e, t_{2}) \land endPoint (e^{'}, t_{3}) \land precedes (t_{0}, t_{1}) \land precedes (t_{1}, t_{2}) \land$

$precedes (t_{2}, t_{3})))$

$\forall e, e^{'} : Event (starts (e, e^{'}) \leftrightarrow$

$\exists t, t^{'}, t^{″} : TimePoint (beginPoint (e, t) \land beginPoint (e^{'}, t) \land endPoint (e, t^{'}) \land$

$endPoint (e^{'}, t^{″}) \land precedes (t^{'}, t^{″}))$

$\forall e, e^{'} : Event (during (e, e^{'}) \leftrightarrow$

$\exists t_{0}, \dots, t_{3} : TimePoint (beginPoint (e, t_{0}) \land beginPoint (e^{'}, t_{1}) \land$

$endPoint (e, t_{2}) \land endPoint (e^{'}, t_{3}) \land precedes (t_{1}, t_{0}) \land precedes (t_{2}, t_{3})))$

$\forall e, e^{'} : Event (finishes (e, e^{'}) \leftrightarrow$

$\exists t, t^{'}, t^{″} : TimePoint (beginPoint (e, t) \land beginPoint (e^{'}, t^{'}) \land endPoint (e, t^{″}) \land$

$endPoint (e^{'}, t^{″}) \land precedes (t^{'}, t))$

$\forall e, e^{'} : Event (equals (e, e^{'}) \leftrightarrow$

$\exists t, t^{'} : TimePoint (beginPoint (e, t) \land beginPoint (e^{'}, t) \land endPoint (e, t^{'}) \land$

$endPoint (e^{'}, t^{'})))$

$\forall e, e^{'} : Event (hasPart (e, e^{'}) \to$

$((\exists t : TimePoint (beginPoint (e, t) \land beginPoint (e^{'}, t)) \lor$

$\exists t, t^{'} : TimePoint (beginPoint (e, t) \land beginPoint (e^{'}, t^{'}) \land precedes (t, t^{'}))) \land$

$(\exists t : TimePoint (endPoint (e, t) \land endPoint (e^{'}, t)) \lor$

$\exists t, t^{'} : TimePoint (endPoint (e, t) \land endPoint (e^{'}, t^{'}) \land precedes (t^{'}, t)))))$

3.6. World changes and situations: (S1′)–(S8)

All Events are triggered by a unique Situation (S3), and every Event bringsAbout a unique Situation (S4). If a Situation triggers an Event, the Situation obtainsIn the same TimePoint that is the beginPoint of the Event (S1′). Similarly, if an Event bringsAbout a Situation, the Situation obtainsIn the same TimePoint that is the endPoint of the Event (S2′). Facts are Situations that obtain (S5). An Event e directlyCauses an Event $e^{'}$ “by means of” a Situation that was brought about by (the inverse of bringsAbout) e and that triggers $e^{'}$ (S6). On (S7), causes should be the transitive closure of directlyCauses, what is inexpressible in FOL. Here, we mitigate this issue by adding a new axiom to the original UFO-B in order to constrain causes to be asymmetric (S8).

$\forall s : Situation, e : Event ($

$triggers (s, e) \to \exists t : TimePoint (obtainsIn (s, t) \land beginPoint (e, t)))$

$\forall s : Situation, e : Event ($

$bringsAbout (e, s) \to \exists t : TimePoint (obtainsIn (s, t) \land endPoint (e, t)))$

$\forall e : Event (\exists! s : Situation (triggers (s, e)))$

$\forall e : Event (\exists! s : Situation (bringsAbout (e, s)))$

$\forall s : Situation (Fact (s) \leftrightarrow \exists t : TimePoint (obtainsIn (s, t)))$

$\forall e, e^{'} : Event (directlyCauses (e, e^{'}) \leftrightarrow$

$\exists s : Situation (bringsAbout (e, s) \land triggers (s, e^{'})))$

$\forall e, e^{″} : Event (causes (e, e^{″}) \leftrightarrow$

$(directlyCauses (e, e^{″}) \lor \exists e^{'} : Event (causes (e, e^{'}) \land causes (e^{'}, e^{″}))))$

$\forall e, e^{'} : Event (causes (e, e^{'}) \to \neg causes (e^{'}, e))$

3.7. Processual roles: (R1)–(R2)

This section deals with an interesting aspect of the interplay between Endurants and Events, the so-called ProcessualRoles (Loebe, 2007, 2003). In UFO-B, ProcessualRoles synchronically classify Endurants w.r.t. the specific ways endurants participate in Events. This means that a synchronic classification is inferred from a diachronic (historical) classification. For instance, mary is a student now because she is studying now.7

⁷
We avoid here the difficult task of providing an epistemological explanation for ongoing events.

Different from ProcessualRoles, relational roles (see Guizzardi (2005)) are inferred from the holding of a specific relationship. For instance, mary is a student now because there is an enrollment relationship between mary and a university that holds now. Notice how different the two meanings of the student roles are in these two examples. It is of fundamental importance to provide an ontological foundation that allows modelers and ontology engineers to disambiguate between ProcessualRoles and relational roles. For instance, while mary qua worker in the relational sense has many rights and obligations and is what matters for the human-resources department, it is mary qua worker in the processual sense that accomplishes goals that are important for her supervisor. In this scenario, an information system for the human-resources department deals with qua-individuals playing relational roles, while an information system for the production department deals with qua-individuals playing processual roles.

As said before, the relation plays is an instantiation relation from Objects to ProcessualRoles. The key notion here is that an Object plays a ProcessualRole inducedBy a ParticipationUniversal, where ParticipationUniversals are Universals that classify Events. A ProcessualRole is inducedBy a unique ParticipationUniversal; and ParticipationUniversals must induce at least one ProcessualRole.

Most importantly, we provide both a necessary and a sufficient condition for an Object to plays a ProcessualRole. On the sufficient condition, if a ProcessualRole r is inducedBy a ParticipationUniversal u and an Object o is the participant of an AtomicEvent p that instantiates u, or p is partOf a Participation that instantiates u, then o plays the ProcessualRole r (R1). Concerning the necessary condition for an Object to plays a ProcessualRole, if an Object o plays a ProcessualRole r, then there is an AtomicEvent p that instantiates a ParticipationUniversal u that induces r, or p is partOf a Participation that instantiates a ParticipationUniversal u that induces r (R2).

$\forall o : Object, p : AtomicEvent, u : ParticipationUniversal, r : ProcessualRole ($

$(dependsOn (p, o) \land inducedBy (r, u) \land$

$(instantiates (p, u) \lor \exists c : Participation (hasPart (c, p) \land$

$instantiates (c, u)))$

$) \to plays (o, r))$

$\forall o : Object, r : ProcessualRole ($

$plays (o, r) \to$

$(\exists p : AtomicEvent, u : ParticipationUniversal ($

$dependsOn (p, o) \land inducedBy (r, u) \land$

$(instantiates (p, u) \lor (\exists c : Participation (hasPart (c, p) \land$

$instantiates (c, u)))))))$

3.8. Qualities and quality structures: (Q1)–(Q3)

Since Events are immutable, their Qualities cannot change. Although “static,” such Qualities may endure through time, which suggests that Qualities of Events must be Endurants. Examples of Qualities inhering in Events include: location, duration, the path of a movement, and the cost of an activity.

As shown in Fig. 1, Qualities are Tropes disjoint with Dispositions. Both Qualities and Dispositions must inhereIn a ConcreteIndividual.

Qualities provide an ontologically parsimonious approach to properties: john and mary have their own immutable and nontransferable weight qualities, which may change by means of quale substitution. Weight qualities are bona fide entities, e.g., john’s-weight and mary’s-weight, which inheresIn john and mary, respectively, and instantiates the QualityUniversal Weight. QualityUniversal is a Universal and is disjoint with ObjectUniversal, and with EventUniversal. Moreover, given a QualityUniversal, a ConcreteIndividual can bear at most one Quality that instantiates this universal (Q1).

$\forall x, y : Quality, z : ConcreteIndividual, w : QualityUniversal ($

$inheresIn (x, z) \land inheresIn (y, z) \land instantiates (x, w) \land instantiates (y, w) \to$

$x = y)$

Quales are AbstractIndividuals that are memberOf QualityStructures, which are Sets. A Quale is memberOf a unique QualityStructure, while a QualityStructure must have at least one Quale.

QualityStructures are associatedWith exactly one QualityUniversal, while a QualityUniversal is associated with at least one QualityStructure. These associatedWith relations serve to constrain the kind of values (Quales) that a quality that is instance of a certain QualityUniversal can have. First, given a Quality x that instantiates a QualityUniversal y associated with a QualityStructure z, there is exactly one Quale q that is memberOf z and is qualeOf x (Q2). Second, if a Quale q is a qualeOf a Quality x, then there is a QualityStructure z associatedWith a QualityUniversal y and s.t. q is memberOf z and x instantiates y (Q3).

Continuing our example, the quale 71KG is a qualeOf of both john’s-weight and mary’s-weight now. The fact that john and mary have the same weight now means that the qualities john’s-weight and mary’s-weight point at the same 71KG quale now (by means of qualeOf). john (or mary) changes his weight by means of quale substitution, e.g., the qualeOf relationship from john’s-weight to 71KG ceases to hold, and a qualeOf relationship from john’s-weight to 70KG starts to hold.8

⁸
Note that by “relationship” we mean a tuple from a relation.

Notice, however, that Qualities of Events are like tropes in the classical sense9

⁹

While a Quality can change, in classical trope theory a trope cannot change. For instance, consider that both john and mary have 70 Kg now. Classical trope theorists would say that john bears his own immutable and nontransferable 70KG-ness trope, which exactly resembles but is numerically different from the 70KG-ness trope of mary. john (or mary) change his weight by means of trope substitution, e.g., john’s 71KG-ness ceases to exist, and a 70KG-ness trope starts inhering in john. Classical tropes are then similar to reified qualeOf relationships, in the sense that in a classical trope-based approach, each qualeOf relationship would be modeled by means of a unique trope. See Daly (1994) for a short introduction.

given that these Qualities can never change because Events are immutable.

Finally, TimePoint is a specialization of AbstractIndividual and may be related to a temporal structure specializing Set, but TimePoint is not a Quale because it is the qualeOf no Quality. Making TimePoint the qualeOf a Quality commits to the idea that existence at a time is a property, which is refused by most philosophers. For example, Armstrong (2004) claims that it is a mistake to recognize states of affairs with the form “a’s existence”, because this will turn existence into a property of a.

3.9. The creation, termination and change of objects: (C1)–(C3)

In this section, we introduce three relations from Objects to Events – viz., createdBy, terminatedBy (meaning “destructed by”) and changedBy – on which we impose no cardinality constraints to avoid necessitating an infinite regress in the creation of Objects, what would result in all models of UFO-B being infinite, and also to allow for eternal objects in infinite models.

Concerning createdBy, an Object createdBy an Event cannot be presentIn a Situation that triggers the Event, but must be presentIn a Situation brought about by the Event, and the Event or one of its proper parts must dependsOn the Object (C1).

$\forall o : Object, e : Event ($

$createdBy (o, e) \to$

$\forall s, s^{'} : Situation ($

$(triggers (s, e) \land bringsAbout (e, s^{'})) \to$

$(\neg presentIn (o, s) \land presentIn (o, s^{'}) \land (dependsOn (e, o) \lor \exists e^{'} : AtomicEvent ($

$hasPart (e, e^{'}) \land dependsOn (e^{'}, o))))))$

Regarding terminatedBy, an Object terminatedBy an Event must be presentIn a Situation that triggers the Event, but cannot be presentIn a Situation brought about by the Event, and the Event or one of its proper parts must dependsOn the Object (C2).

$\forall o : Object, e : Event ($

$terminatedBy (o, e) \to$

$\forall s, s^{'} : Situation ($

$(triggers (s, e) \land bringsAbout (e, s^{'})) \to$

$(presentIn (o, s) \land \neg presentIn (o, s^{'}) \land (dependsOn (e, o) \lor \exists e^{'} : AtomicEvent ($

$hasPart (e, e^{'}) \land dependsOn (e^{'}, o))))))$

Concerning changedBy, an Object changedBy an Event must be presentIn all Situations that triggers the Event or that are brought about by the Event; the Event or one of its proper parts must dependsOn the Object; and in order to explain the change, a Disposition must start or cease to be presentIn the Situations mentioned before (C3). Another possibility would be to explain the change in the object by means of a change in one of its dispositions, instead of an interchange of dispositions. However, one now faces the problem of explaining changes in dispositions.

$\forall o : Object, e : Event ($

$changedBy (o, e) \to$

$\forall s, s^{'} : Situation ($

$(triggers (s, e) \land bringsAbout (e, s^{'})) \to$

$(presentIn (o, s) \land presentIn (o, s^{'}) \land (dependsOn (e, o) \lor \exists e^{'} : AtomicEvent ($

$hasPart (e, e^{'}) \land dependsOn (e^{'}, o))) \land$

$\exists d : Disposition ($

$inheresIn (d, o) \land ((\neg presentIn (d, s) \land presentIn (d, s^{'})) \lor$

$(presentIn (d, s) \land \neg presentIn (d, s^{'})))))))$

Finally, note that our UFO-B FOL theory focuses on legibility, and we may have accidentally added (non-trivial) theorems as axioms. This potentially affects the performance of reasoning with our UFO-B $SROIQ$ theories. We leave an optimization of the theories presented here for future work.

4. The unstructured set of UFO-B $SROIQ$ axioms

In this section, we map each UFO-B FOL axiom to $SROIQ$ , disconsidering the structural restrictions of $SROIQ$ . The result is $T$ , the unstructured set of UFO-B $SROIQ$ axioms (Section 4.2). Let us introduce, in Section 4.1, a bit of the $SROIQ$ syntax required for $T$ .

4.1. Concepts and roles in $SROIQ$

In DL, unary predicates can be represented by means of concepts, and binary predicates by roles. Let C be a set of concept names10

¹⁰
By “name,” we mean a finite string.

and R be a set of role names, where C and R are disjoint. Let “⪋” denote ⩽, =, or ⩾.

Definition 1 (Role).

A role is either a role name R from R or the inverse $⌜ R^{-} ⌝$ of a role name R from R.11

¹¹
We use the symbols “⌜” and “⌝” to denote quasi-quotation. Moreover, note that the role inversion operator “ $^{-}$ ” can only be applied to role names. So, one cannot write “ $R^{- -}$ ” meaning “R.”

The universal role U is a role name in R.

Definition 2 (Concept).

Concepts can be built by means of the operators of complement “¬,” union “⊔,” intersection “⊓,” universal restriction “∀,” existential restriction “∃,” qualified cardinality restriction “⪋,” and local reflexivity “Self.” The top concept “⊤” can be seen as “thing,” the most general predicate. The bottom concept “⊥” can be seen as a type with no instances, and it is useful in the specification of negative constraints, e.g., one can state that Object is pairwise disjoint with Event by stating that their intersection specializes “⊥.”

The set of concepts is the smallest superset of C containing “⊤,” “⊥,” $⌜ \neg C ⌝$ , $⌜ C ⊔ D ⌝$ , $⌜ C ⊓ D ⌝$ , $⌜ \forall R . C ⌝$ , $⌜ \exists R . C ⌝$ , ⌜ $⪋ n R . C$ ⌝, and $⌜ \exists R . Self ⌝$ , where $C, D$ are concepts, R is a role, and n is a numeral denoting a natural number.

In DL, the terminological knowledge is expressed by a TBox, which contains axioms referring to concepts and roles.

Definition 3 (General concept inclusion axiom).

Subsumptions between concepts can be represented by means of general concept inclusions (GCIs), which use the operator “⊑.” For instance, “ $Person ⊑ Animal$ .” If C and D are concepts, then $⌜ C ⊑ D ⌝$ is a GCI.

Definition 4 (Role assertion).

One can specify certain constraints on roles by means of role assertions. For instance, if R and S are roles, then symmetry $⌜ Sym (R) ⌝$ , asymmetry $⌜ Asy (R) ⌝$ ,12

¹²
The construct “Asy” is called “antisymmetry” in Horrocks et al. (2006, p. 59), but we think that the provided semantics of “Asy” is of asymmetry.

transitivity

⌜ Tra (R) ⌝

, reflexivity

⌜ Ref (R) ⌝

, irreflexivity

⌜ Irr (R) ⌝

,13

¹³

Note that irreflexivity and asymmetry usually refer to a relation over a set, i.e., a relation where the domain and the codomain are the same. However, both $SROIQ$ operators “Irr” and “Asy” can be applied to a role having different domain and codomain.

and pairwise disjointness

⌜ Dis (R, S) ⌝

are role assertions.

Definition 5 (Role composition).

Role composition is represented by means of the construct “∘,” e.g., the “maternal grandfather of” relation can be specified as “ $fatherOf \circ motherOf$ .”14

¹⁴
In Horrocks et al. (2006, p. 58), role composition is denoted by the juxtaposition of roles, e.g., “ $fatherOf motherOf$ .” Here, we use the symbol “∘” for clarity.

A string

⌜ τ \circ R ⌝

is a role composition iff R is a role, and τ is a role or role composition.

Definition 6 (Role inclusion axiom).

Subsumption between binary relations can be represented by means of role inclusion axiom (RIAs), which use the operator “⊑.” For instance, “ $motherOf ⊑ parentOf$ .” If R is a role and τ is a role or role composition not including the universal role U, then $⌜ τ ⊑ R ⌝$ is a RIA.

Note that $⌜ Sym (R) ⌝$ is equivalent to $⌜ R^{-} ⊑ R ⌝$ , $⌜ Tra (R) ⌝$ is to $⌜ R \circ R ⊑ R ⌝$ , and $⌜ Irr (R) ⌝$ is to $⌜ ⊤ ⊑ \neg \exists R . Self ⌝$ . Finally, while $⌜ Ref (R) ⌝$ is equivalent to $⌜ ⊤ ⊑ \exists R . Self ⌝$ , the form $⌜ Ref (R) ⌝$ is preferred since $SROIQ$ poses no structural constraint on it (see Section 8).

Definition 7 (TBox).

A role box (RBox) is a finite set of role assertions or RIAs. A concept box (CBox) is a finite set of GCIs. A TBox is the union of an RBox and a CBox.

Since we do not use nominals in this work (the “ $O$ ” in “ $SROIQ$ ”), one could argue that our theories actually fit in the smaller logic $SRIQ$ (Horrocks et al., 2005). However, the presentation of $SRIQ$ in Horrocks et al. (2005) does not provide the construct for asymmetry “Asy,” which we use, and that cannot be enforced by means of RIAs (Horrocks et al., 2006, p. 59). $SRIQ$ provides constructs for symmetry “Sym” and transitivity “Tra” (which can be expressed by means of RIAs), and reflexivity “Ref,” irreflexivity “Irr” and pairwise disjointness “Dis” (which cannot be expressed by means of RIAs) (Horrocks et al., 2005, p. 5).

4.2. The set $T$

First, we present axioms that correspond to Fig. 1 and Fig. 2, then we discuss the axioms of the different subtheories: Universals and individuals (U1)–(U5); Event mereology (M1)–(M9); Events as manifestations of object dispositions (D1′)–(D9); On the participation of objects in events (P1)–(P5); Temporal relations between events (T1)–(T14′); World changes and situations (S1′)–(S8); Processual roles (R1)–(R2); Qualities and quality structures (Q1)–(Q3); and The creation, termination and change of objects (C1)–(C3).

4.2.1. Formalization of Figs 1 and 2

Below, we specify the subsumptions between classes or relations in Fig. 1 and Fig. 2.

$Urelement ⊑ ⊤$

$Set ⊑ ⊤$

$Universal ⊑ Urelement$

$Individual ⊑ Urelement$

$QualityUniversal ⊑ Universal$

$ObjectUniversal ⊑ Universal$

$EventUniversal ⊑ Universal$

$ProcessualRole ⊑ ObjectUniversal$

$ParticipationUniversal ⊑ EventUniversal$

$ConcreteIndividual ⊑ Individual$

$AbstractIndividual ⊑ Individual$

$Event ⊑ ConcreteIndividual$

$Endurant ⊑ ConcreteIndividual$

$Participation ⊑ Event$

$Object ⊑ Endurant$

$Trope ⊑ Endurant$

$Disposition ⊑ Trope$

$Quality ⊑ Trope$

$TimePoint ⊑ AbstractIndividual$

$Quale ⊑ AbstractIndividual$

$QualityStructure ⊑ Set$

$plays ⊑ instantiates$

$Situation ⊑ ConcreteIndividual$

$Fact ⊑ Situation$

$AtomicEvent ⊑ Event$

$ComplexEvent ⊑ Event$

$directlyCauses ⊑ causes$

The pairwise disjointness constraints between classes:

$(Urelement ⊓ Set) ⊑ ⊥$

$(Universal ⊓ Individual) ⊑ ⊥$

$(ConcreteIndividual ⊓ AbstractIndividual) ⊑ ⊥$

$(QualityUniversal ⊓ ObjectUniversal) ⊑ ⊥$

$(QualityUniversal ⊓ EventUniversal) ⊑ ⊥$

$(ObjectUniversal ⊓ EventUniversal) ⊑ ⊥$

$(Endurant ⊓ Event) ⊑ ⊥$

$(TimePoint ⊓ Quale) ⊑ ⊥$

$(Object ⊓ Trope) ⊑ ⊥$

$(Disposition ⊓ Quality) ⊑ ⊥$

$(Endurant ⊓ Situation) ⊑ ⊥$

$(Event ⊓ Situation) ⊑ ⊥$

$(AtomicEvent ⊓ ComplexEvent) ⊑ ⊥$

The completeness constraints that, together with pairwise disjointness, define class partitions:

$⊤ ⊑ (Urelement ⊔ Set)$

$Urelement ⊑ (Universal ⊔ Individual)$

$Individual ⊑ (ConcreteIndividual ⊔ AbstractIndividual)$

$Event ⊑ (AtomicEvent ⊔ ComplexEvent)$

We formalize the domain, codomain and cardinality constraints of relations according to their orientations in the class diagrams presented in Fig. 1 and Fig. 2. Below, the domain constraints.

$\exists instantiates . ⊤ ⊑ Individual$

$\exists memberOf . ⊤ ⊑ Quale$

$\exists inducedBy . ⊤ ⊑ ProcessualRole$

$\exists qualeOf . ⊤ ⊑ Quale$

$\exists plays . ⊤ ⊑ Object$

$\exists associatedWith . ⊤ ⊑ QualityStructure$

$\exists inheresIn . ⊤ ⊑ Trope$

$\exists precedes . ⊤ ⊑ TimePoint$

$\exists beginPoint . ⊤ ⊑ Event$

$\exists endPoint . ⊤ ⊑ Event$

$\exists directlyCauses . ⊤ ⊑ Event$

$\exists causes . ⊤ ⊑ Event$

$\exists presentIn . ⊤ ⊑ Endurant$

$\exists createdBy . ⊤ ⊑ Object$

$\exists terminatedBy . ⊤ ⊑ Object$

$\exists changedBy . ⊤ ⊑ Object$

$\exists activates . ⊤ ⊑ Situation$

$\exists exclusivelyDependsOn . ⊤ ⊑ Event$

$\exists participationOf . ⊤ ⊑ Participation$

$\exists dependsOn . ⊤ ⊑ AtomicEvent$

$\exists mereologicallyOverlaps . ⊤ ⊑ Event$

$\exists hasPart . ⊤ ⊑ ComplexEvent$

$\exists manifestedBy . ⊤ ⊑ Disposition$

$\exists triggers . ⊤ ⊑ Situation$

$\exists bringsAbout . ⊤ ⊑ Event$

$\exists obtainsIn . ⊤ ⊑ Situation$

The codomain constraints:

$⊤ ⊑ \forall instantiates . Universal$

$⊤ ⊑ \forall memberOf . QualityStructure$

$⊤ ⊑ \forall inducedBy . ParticipationUniversal$

$⊤ ⊑ \forall qualeOf . Quality$

$⊤ ⊑ \forall plays . ProcessualRole$

$⊤ ⊑ \forall associatedWith . QualityUniversal$

$⊤ ⊑ \forall inheresIn . ConcreteIndividual$

$⊤ ⊑ \forall precedes . TimePoint$

$⊤ ⊑ \forall beginPoint . TimePoint$

$⊤ ⊑ \forall endPoint . TimePoint$

$⊤ ⊑ \forall directlyCauses . Event$

$⊤ ⊑ \forall causes . Event$

$⊤ ⊑ \forall presentIn . Situation$

$⊤ ⊑ \forall createdBy . Event$

$⊤ ⊑ \forall terminatedBy . Event$

$⊤ ⊑ \forall changedBy . Event$

$⊤ ⊑ \forall activates . Disposition$

$⊤ ⊑ \forall exclusivelyDependsOn . Object$

$⊤ ⊑ \forall participationOf . Object$

$⊤ ⊑ \forall dependsOn . Object$

$⊤ ⊑ \forall mereologicallyOverlaps . Event$

$⊤ ⊑ \forall hasPart . Event$

$⊤ ⊑ \forall manifestedBy . AtomicEvent$

$⊤ ⊑ \forall triggers . Event$

$⊤ ⊑ \forall bringsAbout . Situation$

$⊤ ⊑ \forall obtainsIn . TimePoint$

The domain cardinality constraints:

$Individual ⊑ (⩾ 1 instantiates . Universal)$

$Quale ⊑ (= 1 memberOf . QualityStructure)$

$ProcessualRole ⊑ (= 1 inducedBy . ParticipationUniversal)$

$QualityStructure ⊑ (= 1 associatedWith . QualityUniversal)$

$Trope ⊑ (= 1 inheresIn . ConcreteIndividual)$

$Event ⊑ (= 1 beginPoint . TimePoint)$

$Event ⊑ (= 1 endPoint . TimePoint)$

$Event ⊑ (⩽ 1 exclusivelyDependsOn . Object)$

$Participation ⊑ (= 1 participationOf . Object)$

$AtomicEvent ⊑ (= 1 dependsOn . Object)$

$ComplexEvent ⊑ (⩾ 2 hasPart . Event)$

$Event ⊑ (= 1 bringsAbout . Situation)$

$Situation ⊑ (⩽ 1 obtainsIn . TimePoint)$

$Fact ⊑ (= 1 obtainsIn . TimePoint)$

The codomain cardinality constraints:

$Universal ⊑ (⩾ 1 {instantiates}^{-} . Individual)$

$QualityStructure ⊑ (⩾ 1 {memberOf}^{-} . Quale)$

$ParticipationUniversal ⊑ (⩾ 1 {inducedBy}^{-} . ProcessualRole)$

$Quality ⊑ (⩾ 1 {qualeOf}^{-} . Quale)$

$ProcessualRole ⊑ (⩾ 1 {plays}^{-} . Object)$

$QualityUniversal ⊑ (⩾ 1 {associatedWith}^{-} . QualityStructure)$

$Object ⊔ Event ⊑ (⩾ 1 {inheresIn}^{-} . Trope)$

$AtomicEvent ⊑ (= 1 {manifestedBy}^{-} . Disposition)$

$Event ⊑ (= 1 {triggers}^{-} . Situation)$

$TimePoint ⊑ (⩾ 1 {obtainsIn}^{-} . Situation)$

We have the domain constraint (a55) even tough it is entailed by ${(a27), (a56)}$ ; and similarly for the codomain constraint (a81), which is entailed by ${(a27), (a82)}$ . This is because we do not know (yet) if the structural restrictions make (a27) incompatible with other axioms. For the same reason, we keep (a92) when we introduce (a130), even though ${(a91), (a130)}$ entails (a92). Similarly for (a92) being also entailed by ${(a65), (a131)}$ ; (a90) being entailed by ${(a88), (a140)}$ ; and (a89) being entailed by ${(a88), (a143)}$ .

4.2.2. Universals and individuals: (a121)–(a124)

According to UFO-A, the classes Urelement and Set partition Thing, while Individual and Universal partition Urelement (Guizzardi, 2005, Fig. 6–12). One can see in (a1), (a2) and (a41) that we mapped Thing to the “⊤” DL concept.

Universals in UFO-A (Guizzardi, 2005, Axiom 22, p. 221) are assumed to satisfy the principle of instantiation (Armstrong, 1989, p. 75), which means that it must be possible (in a modal sense) for a universal to have instances. We partially capture this assumption by means of (a111).

Concerning the relation instantiates and its specializations, (U1)–(U4) can be specified in $SROIQ$ as (a121)–(a124), respectively. (U5), the constraint that all instantiates relationships from Objects to ProcessualRoles are plays relationships, seems inexpressible in $SROIQ$ (we can only think of a solution using variables). For this reason, we add an axiom to guarantee that all ProcessualRoles are played by at least one Object (a115), which is a theorem of our first-order theory (t1).

$\exists instantiates . QualityUniversal ⊑ Quality$ (U1)

$\exists instantiates . ObjectUniversal ⊑ Object$ (U2)

$\exists instantiates . EventUniversal ⊑ Event$ (U3)

$\exists instantiates . ParticipationUniversal ⊑ Participation$ (U4)

Moreover, given that the domain of instantiates (Individual) is disjoint with its codomain (Universal, see (a29)), then instantiates is (implicitly) asymmetric and hence irreflexive. We will see in Section 5.1 that, due to the structural restrictions of $SROIQ$ , asserting either $⌜ Irr (R) ⌝$ or $⌜ Asy (R) ⌝$ require R to be simple. Since stating the disjointness of the domain and codomain of R (as in (a29)) has no consequences w.r.t. structural restrictions, we only state $⌜ Irr (R) ⌝$ or $⌜ Asy (R) ⌝$ when the domain of R is not disjoint with its codomain.

4.2.3. Event mereology: (a125)–(a133)

The inexpressibility of mereological notions in $SROIQ$ was already recognized in (Horrocks et al., 2006, p. 67), as its syntactic constraints forbid roles to be asymmetric and transitive. For (M1), the axiom (a25) already guarantees that AtomicEvents are Events, and we capture the necessary condition (indicated by “−”) of AtomicEvent in (a125), and the sufficient condition (indicated by “+”) in (a126). An absence of “−” or “+” means equivalence. (M2) is guaranteed by (a40) and (a44). (M4) is captured by (a127), which also captures (M3) since asymmetry entails irreflexivity.15

¹⁵
Since asymmetry entails irreflexivity, and both “Irr” and “Asy” obey the very same $SROIQ$ syntactic constraints (as we will see in Section 5.1, “Irr” and “Asy” only apply to simple roles), then whenever a role is asymmetric, there is no benefit in also asserting its irreflexivity.

(M5) is captured by (a128).

$AtomicEvent ⊑ \neg \exists hasPart . Event$ (M1)−

$Event ⊓ \neg \exists hasPart . Event ⊑ AtomicEvent$ (M1)+

$Asy (hasPart)$ (M3), (M4)

$Tra (hasPart)$ (M5)

For (M7′), (a129)–(a132) represent the sufficient conditions for mereologicallyOverlaps. The necessary condition for this role seems inexpressible, as the right-hand side of a role inclusion axiom (RIA) can only have a role name. Finally, we assert the symmetry of mereologicallyOverlaps by (a133).

$Event ⊑ \exists mereologicallyOverlaps . Self$ (M7′)+

$hasPart ⊑ mereologicallyOverlaps$ (M7′)+

${hasPart}^{-} ⊑ mereologicallyOverlaps$ (M7′)+

$hasPart \circ {hasPart}^{-} ⊑ mereologicallyOverlaps$ (M7′)+

$Sym (mereologicallyOverlaps)$ (M7′)−

(M6) seems inexpressible even by assuming a $SROIQ$ definition of mereologicallyOverlaps. Intuitively, (M6) would be captured by the expressions “hasAtLeastTwoDisjointParts ≡ hasPart ∘ notMereologicallyOverlap ∘ hasPart $^{-}$ ” and “ $Ref ($ hasAtLeastTwoDisjointParts),” which enforce the existence of a path from a whole, then to a part, then to a non-overlapping entity that is also a part, so that the path comes to a cycle by an inverse of the parthood relation. However, the first formula is excluded by the syntax of $SROIQ$ , which disallows role compositions on the right-hand side of role inclusions. Moreover, the role notMereologicallyOverlap used in this composition is inexpressible in this logic. One could think of trying “ $Dis ($ mereologicallyOverlaps, notMereologically Overlap),” but $SROIQ$ cannot express that one relation would be the set-complement of the other, i.e., the meaning of the non- $SROIQ$ formula “ $U ⊑$ mereologicallyOverlaps ⊔ notMereologicallyOverlap.” More precisely, $SROIQ$ does not allow complementation of roles. Finally, it seems that neither (M8) nor (M9) are expressible, since there is no way to capture an equality on “generic individuals,” as there are no first-order variables in this language. Since we captured neither weak supplementation (M6) nor strong supplementation (M8) in $SROIQ$ , (a107) poses at least a cardinality constraint ensuring that every ComplexEvent has at least two parts.

4.2.4. Events as manifestations of object dispositions: (a134)–(a139)

(D1′) is guaranteed by (a17) and (a101), while (D2) is captured by (a118). As the right-hand side of a RIA can only have a role name, it seems that only the sufficient condition of (D3) can be formalized as (a134). (D4) is captured by (a135). (D5) is guaranteed by (a117). (D6) is captured by (a136). On (D7), since $SROIQ$ provides no role negation, it seems impossible to capture intransitivity. (D8) is captured by (a137) and (a138), while (D9) is captured by (a139).

$activates \circ manifestedBy ⊑ triggers$ (D3)+

${manifestedBy}^{-} \circ inheresIn ⊑ dependsOn$ (D4)

$Asy (inheresIn)$

$manifestedBy \circ {triggers}^{-} ⊑ presentIn$ (D8)−

$manifestedBy \circ bringsAbout ⊑ presentIn$ (D8)−

${inheresIn}^{-} \circ presentIn ⊑ presentIn$ (D9)

4.2.5. On the participation of objects in events: (a140)–(a142)

(P1) is guaranteed by (a106). For (P2), it seems that $SROIQ$ cannot express the subset of the exclusivelyDependsOn relation that has AtomicEvent as its domain. As the domain of dependsOn is AtomicEvent, it seems that only the necessary condition for dependsOn (a140) is expressible, but not the opposite role inclusion. Similarly for (P3) and the subset of the exclusivelyDependsOn relation that has ComplexEvent as its domain. On (P4), the necessary condition for being a Participation is captured by {(a14), (a141)}, while the sufficient condition for being a Participation is captured by (a142).

$dependsOn ⊑ exclusivelyDependsOn$ (P2)−

$Participation ⊑ = 1 exclusivelyDependsOn . Object$ (P4)−

$Event ⊓ (= 1 exclusivelyDependsOn . Object) ⊑ Participation$ (P4)+

Concerning (P5), since participationOf and exclusivelyDependsOn have the same codomain – Object – and the domain of participationOf (Participation) specializes the domain of exclusivelyDependsOn (Event), the left-to-right implication can be captured in (a143). On the other hand, it seems impossible to capture the right-to-left implication, i.e., exclusivelyDependsOn with the domain constrained to Participation specializes participationOf.

$participationOf ⊑ exclusivelyDependsOn$ (P5)+

4.2.6. Temporal relations between events: (a144)–(a174)

Batsakis et al. (2017) discuss the impossibility of expressing Allen’s time interval relations (Allen, 1983) in $SROIQ$ . Therefore, it seems that the best one can do is to provide partial axiomatizations of UFO-B’s temporal relations between Events. (Guizzardi et al., 2013, p. 331) informally defines the domain and codomain of these relations as Event (a144)–(a157).

$\exists before . ⊤ ⊑ Event$

$⊤ ⊑ \forall before . Event$

$\exists meets . ⊤ ⊑ Event$

$⊤ ⊑ \forall meets . Event$

$\exists starts . ⊤ ⊑ Event$

$⊤ ⊑ \forall starts . Event$

$\exists during . ⊤ ⊑ Event$

$⊤ ⊑ \forall during . Event$

$\exists finishes . ⊤ ⊑ Event$

$⊤ ⊑ \forall finishes . Event$

$\exists equals . ⊤ ⊑ Event$

$⊤ ⊑ \forall equals . Event$

$\exists temporallyOverlaps . ⊤ ⊑ Event$

$⊤ ⊑ \forall temporallyOverlaps . Event$

On precedes, (T2) (and (T1)) is captured by (a158), while (T3) is by (a159). Totality (T4) seems inexpressible (at the time, we can only think of a solution using variables). (T5′) is guaranteed by (a102) and (a103). (T6′) is captured by (a160).

$Asy (precedes)$ (T1), (T2)

$Tra (precedes)$ (T3)

${beginPoint}^{-} \circ endPoint ⊑ precedes$ (T6′)

$endPoint \circ precedes \circ {beginPoint}^{-} ⊑ before$ (T7′)+

$endPoint \circ {beginPoint}^{-} ⊑ meets$ (T8′)+

Concerning the Allen relations (T7′)–(T13′), their necessary conditions seem inexpressible because the right-hand side of a RIA can only have a role name. The sufficient conditions for before (T7′) and meets (T8′) are captured by (a161) and (a162), respectively. The sufficient conditions for temporallyOverlaps (T9′), starts (T10′), during (T11′), finishes (T12′), and equals (T13′), seem inexpressible, since they would require a conjunction of role compositions, see formulae (f1)–(f5), respectively. Finally, (T14′) would break even more syntactic constraints, see (f6).

$(beginPoint \circ precedes \circ {beginPoint}^{-}) ⊓ (endPoint \circ {precedes}^{-} \circ$

${beginPoint}^{-}) ⊓ (endPoint \circ precedes \circ {endPoint}^{-}) ⊑ temporallyOverlaps$

(T9′)+

$(beginPoint \circ {beginPoint}^{-}) ⊓ (endPoint \circ precedes \circ {endPoint}^{-}) ⊑ starts$

(T10′)+

$(beginPoint \circ {precedes}^{-} \circ {beginPoint}^{-}) ⊓$

$(endPoint \circ precedes \circ {endPoint}^{-}) ⊑ during$ (T11′)+

$(endPoint \circ {endPoint}^{-}) ⊓ (beginPoint \circ {precedes}^{-} \circ {beginPoint}^{-}) ⊑ finishes$

(T12′)+

$(beginPoint \circ {beginPoint}^{-}) ⊓ (endPoint \circ {endPoint}^{-}) ⊑ equals$ (T13′)+

$hasPart ⊑ (((beginPoint \circ {beginPoint}^{-}) ⊔ (beginPoint \circ precedes \circ {beginPoint}^{-})) ⊓ ((endPoint \circ {endPoint}^{-}) ⊔$

$(endPoint \circ {precedes}^{-} \circ {endPoint}^{-})))$ (T14′)

Since we could capture only a small fraction of the definitions of the Allen relations, we can at least pose some role assertions to capture some properties of these relations: before, starts and during are asymmetric (a163), (a165), (a167) and transitive (a164), (a166), (a168); meets, temporallyOverlaps, and finishes are asymmetric (a169), (a170), (a171); and equals is an equivalence relation on its domain, i.e., reflexive (a172),16

¹⁶
We do not use the role assertion “ $Ref (equals)$ ” because its semantics in $SROIQ$ is stronger than the usual definition of reflexivity, as it enforces the domain of the role name equals to be the whole domain of quantification, i.e., “⊤.” Strictly, the role assertion “ $Ref (R)$ ” reads “the role name R contains the identity relation.”

symmetric (a173) and transitive (a174).

$Asy (before)$

$Tra (before)$

$Asy (starts)$

$Tra (starts)$

$Asy (during)$

$Tra (during)$

$Asy (meets)$

$Asy (temporallyOverlaps)$

$Asy (finishes)$

$Event ⊑ \exists equals . Self$

$Sym (equals)$

$Tra (equals)$

4.2.7. World changes and situations: (a175)–(a179)

(S1′) and (S2′) seem inexpressible in $SROIQ$ , since the right-hand side of a RIA can only have a role name (see (f7) and (f8)). (S3) and (S4) are guaranteed by (a119) and (a108), respectively. On (S5), the necessary condition for being a Fact is captured by (a110), while the sufficient condition is by (a175). On (S6), it is impossible to define a role as the composition of other roles; a role can only include a role composition. Therefore, we capture the sufficient condition for directlyCauses in (a176), but the necessary condition seems inexpressible. Only the sufficient conditions of (S7) seem expressible in $SROIQ$ , as in (a27) and (a177); the necessary condition seems inexpressible due to the same reason as for (S1′).

$triggers ⊑ obtainsIn \circ {beginPoint}^{-}$

$bringsAbout ⊑ endPoint \circ {obtainsIn}^{-}$

$Situation ⊓ (⩾ 1 obtainsIn . TimePoint) ⊑ Fact$ (S5)+

$bringsAbout \circ triggers ⊑ directlyCauses$ (S6)+

$Tra (causes)$ (S7)+

From the strict linear ordering of TimePoints and (T6′), it follows that the beginPoint of an Event must strictly precedes its endPoint. From (S1′), (S2′) and (S6) it follows that directlyCauses is asymmetric (a178). More strongly, it also follows that a chain of directlyCauses is acyclic. Since causes should be the transitive closure of directlyCauses, causes is asymmetric (a179), and transitive (a177).

$Asy (directlyCauses)$

$Asy (causes)$

4.2.8. Processual roles: (a180)–(a181)

We provide both a necessary condition (R2) and a sufficient condition (R1) for an Object to plays a ProcessualRole. (R1) is translated to (a180) and (a181). Unfortunately, (R2) does not seem expressible in $SROIQ$ – see (f9) – as $SROIQ$ forbids both union of roles (and role compositions) and non-role-names on the right-hand side of a RIA.

${dependsOn}^{-} \circ instantiates \circ {inducedBy}^{-} ⊑ plays$ (R1)−

${dependsOn}^{-} \circ {hasPart}^{-} \circ instantiates \circ {inducedBy}^{-} ⊑ plays$ (R1)−

$plays ⊑ ({dependsOn}^{-} \circ instantiates \circ {inducedBy}^{-}) ⊔$

$({dependsOn}^{-} \circ {hasPart}^{-} \circ instantiates \circ {inducedBy}^{-})$ (R2)

4.2.9. Qualities and quality structures

Since it seems that first-order variables are needed to express (Q1), this axiom appears inexpressible in $SROIQ$ . Moreover, discarding the uniqueness constraint in (Q2), it could be captured by (f10), which is not a $SROIQ$ formula because $SROIQ$ forbids role compositions on the right-hand side of a RIA. It seems that the best one can do is to impose a cardinality constraint on the codomain of qualeOf in order to ensure that a Quality has at least one Quale (a114). Similarly to (Q2), (Q3) appears inexpressible in $SROIQ$ , see (f11).

$instantiates \circ {associatedWith}^{-} ⊑ {qualeOf}^{-} \circ memberOf$ (Q2)−

${qualeOf}^{-} ⊑ instantiates \circ {associatedWith}^{-} \circ {memberOf}^{-}$ (Q3)

4.2.10. The creation, termination and change of objects: (a182)–(a185)

(C1) can be partially characterized by (a182). It seems inexpressible in its totality because there are neither role negations nor role disjunctions in $SROIQ$ . Similarly to (C1), (C2) and (C3) appear to be inexpressible in their totality in $SROIQ$ ; see (a183) for (C2), and (a184) and (a185) for (C3).

$createdBy \circ bringsAbout ⊑ presentIn$ (C1)−

$terminatedBy \circ {triggers}^{-} ⊑ presentIn$ (C2)−

$changedBy \circ bringsAbout ⊑ presentIn$ (C3)−

$changedBy \circ {triggers}^{-} ⊑ presentIn$ (C3)−

5. UFO-B $SROIQ$ theories: The maximally structured subsets of $T$

In this section, we determine all the maximally structured subsets of $T$ . Let us introduce, in Section 5.1, the two structural restrictions of $SROIQ$ , viz., regularity and simplicity.

5.1. The structural restrictions of $SROIQ$

It is known that allowing an unrestricted use of roles in an RBox can easily lead to undecidability of reasoning (Horrocks et al., 2006, p. 58). For that reason, $SROIQ$ imposes some additional syntactic constraints – the structural restrictions known as simplicity and regularity – in the construction of axioms in a TBox.

Definition 8 (Simplicity).

We simplify the notion of simplicity presented in (Horrocks et al., 2006, p. 59) in order to qualify only role names in R as simple, instead of qualifying also inverse roles.17

¹⁷
From the original definition of simplicity in (Horrocks et al., 2006, p. 59), the only case in which an inverse role $R^{-}$ is non-simple is when the related role name R is non-simple. Therefore, the simplicity rules for role names can be rewritten in order to take into account also the cases where inverse roles would be considered non-simple.

There are two forms of direct sources of non-simplicity for a role name R: (i) RIAs having a role composition τ on the left-hand side, like

⌜ τ ⊑ R ⌝

; and (ii) the role assertions

⌜ Tra (R) ⌝

and

⌜ Tra (R^{-}) ⌝

. There is one form of indirect source of non-simplicity for a role name R: RIAs like

⌜ S ⊑ R ⌝

and

⌜ S^{-} ⊑ R ⌝

, where S is a non-simple role name. Let “

⊑^{*}

” denote the reflexive transitive closure of the inclusion relation ⊑ over roles (i.e., excluding role compositions). A role name R is simple w.r.t. a TBox iff for any role name S such that

S ⊑^{*} R

S^{-} ⊑^{*} R

, the TBox does not contain

⌜ Tra (S) ⌝

⌜ Tra (S^{-}) ⌝

, and there is no role composition τ such that the TBox contains

⌜ τ ⊑ S ⌝

The syntactic rule called “simplicity” forbids non-simple role names and inverses of non-simple role names to be used in concepts of the form $⌜ \exists R . Self ⌝$ and ⌜ $⪋ n R . C$ ⌝, and role assertions of the form $⌜ Irr (R) ⌝$ , $⌜ Asy (R) ⌝$ , and $⌜ Dis (R, S) ⌝$ .

Regularity enforces the set of RIAs to “induce” a constrained strict partial order on the set of roles, preventing a role hierarchy from containing cyclic dependencies that could lead to undecidability (Horrocks et al., 2006, p. 58).

Definition 9 (Regularity).

A strict partial order ≺ on the set of roles is called regular iff, for all roles R and S, the additional constraint of $⌜ S ≺ R \leftrightarrow S^{-} ≺ R ⌝$ holds. A RIA $⌜ τ ⊑ R ⌝$ is ≺-regular iff R is a role name and $S_{1}, \dots, S_{n}$ are roles different from R and $R^{-}$ such that:

$τ = ⌜ R \circ R ⌝$ , or

$τ = ⌜ R^{-} ⌝$ , or

$τ = ⌜ S_{1} \circ \dots \circ S_{n} ⌝$ and $S_{i} ≺ R$ , for all $1 ⩽ i ⩽ n$ , or

$τ = ⌜ R \circ S_{1} \circ \dots \circ S_{n} ⌝$ and $S_{i} ≺ R$ , for all $1 ⩽ i ⩽ n$ , or

$τ = ⌜ S_{1} \circ \dots \circ S_{n} \circ R ⌝$ and $S_{i} ≺ R$ , for all $1 ⩽ i ⩽ n$ .

A set of RIAs is regular iff there exists a regular order ≺ such that each RIA in the set is ≺-regular. The syntactic rule called “regularity” ensures that the set of all RIAs in a TBox is regular.18

¹⁸
In our implementation, we simplified the notion of regularity in the following way. Let us define a function that extracts the “base role name” of a role: given that the set of roles has only role names and inverses of role names and that $⌜ R^{- -} ⌝$ is not allowed in $SROIQ$ , we define $base (R)$ for any role name R as ⌜ $base (R) ≜ R$ ⌝ and ⌜ $base (R^{-}) ≜ R$ ⌝. Since the right-hand side of a RIA can only have role names, from (1)–(5) there is no constraint on the regular order ≺ enforcing a role to precede the inverse of a role name, i.e., no constraint of the form $S ≺ R^{-}$ . Therefore, instead of qualifying a strict partial order ≺ as regular by means of “ $S ≺ R \leftrightarrow S^{-} ≺ R$ ,” one can restrict the domain of ≺ to role names (instead of roles) and modify rules (3)–(5) by replacing “ $S_{i} ≺ R$ ” with “ $base (S_{i}) ≺ R$ .” In this way, the size of the domain of ≺ is halved, what could improve the performance of techniques for solving partial order constraints such as the one proposed in Codish et al. (2006).

In the following, whenever we speak of a $SROIQ$ TBox, we will implicitly assume that it satisfies the two syntactic restrictions of simplicity and regularity, unless explicitly stated otherwise.

5.2. Incompatibilities between

SROIQ

axioms

In order to track the incompatibilities between axioms in $T = {(a 1), \dots, (a 185)}$ that lead to infringing the $SROIQ$ syntactic rules of regularity or simplicity, we build a very simple meta-level theory $I$ in propositional logic. By means of this meta-level theory, we define the problem of finding subsets of $T$ that satisfy regularity and simplicity as a SAT problem, which is decidable and can be addressed by many SAT solvers (Biere et al., 2009).

5.2.1. Incompatibilities due to regularity

We use the proposition “ $I (i)$ ” to mean that the axiom (ai) is included in the TBox (i.e., “ $I$ ” serves as a “proposition builder”, whereas “i” behaves like an index in the proposition). Moreover, relationships like “ $r ≺ s$ ” can also be seen as propositions. In order to capture the incompatibility between axioms due to regularity, we add a conditional statement for each RIA that, when included in the TBox, implies an ordering constraint. For instance, given an axiom i and roles R and S, the fact that the inclusion of axiom i in the TBox requires both relationships $R ≺ S$ and $R^{-} ≺ S$ to hold is captured by the propositional formula “ $I (i) \to (R ≺ S) \land (R^{-} ≺ S)$ .” The interested reader can find these conditions in Appendix A.

Codish et al. (2006) show how to encode, in propositional logic, constraints for a partial order over a set S by using $| S | \cdot ⌈ {log}_{2} | S | ⌉$ propositional variables. In our case, since there are 66 roles, we need 462 propositional variables for our regularity constraints, which is impracticable for our computational resources (the size of the search space of the SAT problem is $2^{462}$ ). Therefore, we manually dealt with regularity by showing two incompatibilities, and showing two regular orders of roles that reflect the inclusion of one or the other of the two choices of axioms, while obeying regularity for all the other axioms. More specifically, the axiom (a22) is incompatible with both (a180) and (a181), which is captured by the meta axiom (m1). Since we found two strict partial orders satisfying regularity, one for $T ∖ {(a180), (a181)}$ , and another for $T ∖ {(a22)}$ , it is guaranteed that there are no more incompatibilities due to regularity other than those excluded by (m1). The interested reader can find the respective partial orders in Fig. 5(b) and Fig. 5(c) in Appendix A.

$I (22) \to \neg (I (180) \lor I (181))$

5.2.2. Incompatibilities due to simplicity

Given a role name R, we capture the fact that R is non-simple by using the “proposition builder” symbol “ $\bar{S}$ ” to build propositions of the form “ $\bar{S} (R)$ .” We are then able to capture constraints such as “the inclusion of axiom i makes the role name R non-simple,” e.g., by the propositional formula “ $I (i) \to \bar{S} (R)$ ;” and “the non-simplicity of role name R forbids the inclusion of axiom i;” e.g., by “ $\bar{S} (R) \to \neg I (i)$ .”

Since our set $T$ of $SROIQ$ axioms is finite – there are 185 axioms – and the set R of role names is finite – there are 33 role names – then the set of proposition symbols built by means of $I$ and $\bar{S}$ is also finite: $185 + 33 = 218$ proposition symbols (also called propositional variables).

Unfortunately, our computational resources could not handle solving a SAT problem with search space at the magnitude of $2^{218}$ ( $> 10^{65}$ ). We address this issue by deriving incompatibility meta-axioms from the two types of constraints discussed above. By the transitivity of the logical implication operator on pairs of propositional formulae like “ $I (i) \to \bar{S} (r)$ ” and “ $\bar{S} (r) \to \neg I (j)$ ,” we derive a meta-axiom “ $I (i) \to \neg I (j)$ .” In other words, we create a propositional meta-axiom for each $SROIQ$ axiom that, when included in the TBox, forbids the inclusion of another axiom in the TBox (by making a role non-simple).

Indirect sources of non-simplicity, like “ $(I (i) \land \bar{S} (r)) \to \bar{S} (s)$ ,” are more difficult to handle. In the special case where the set of role names made non-simple by direct sources of non-simplicity is disjoint from the set of role names made non-simple by indirect sources of non-simplicity (i.e., the set of role names appearing in the antecedents of the simplicity meta-axioms is disjoint from the set of role names appearing in the consequents), one can replace $\bar{S} (r)$ by a disjunction of its direct sources of non-simplicity: “ $(I (i) \land (I (j) \lor \dots \lor I (k))) \to \bar{S} (s)$ .” In our tool, we first check such disjointness before applying this reduction.

Since our propositional meta-level theory $I$ could be simplified by this technique, $I$ does not include propositions about the simplicity of a role or about partial order constraints. $I$ only concerns incompatibilities between axioms, so that only axioms like “ $I (i) \to \neg I (j)$ ” are included. With this simplification, $I$ requires only 40 propositional variables. Also, since now we use only one “proposition builder” – “ $I$ ” – , we may substitute the notation “ $I (i)$ ” with “i” when the context precludes ambiguity (e.g., in Fig. 3 in Section 5.3).

In what follows, we list the meta-axioms that capture incompatibilities due to simplicity. The interested reader can find the full derivations in Appendix B.

$(I (132) \lor (I (128) \land (I (130) \lor I (131)))) \to \neg I (129)$

$I (134) \to \neg I (119)$

$I (135) \to \neg I (106)$

$(I (160) \lor I (159)) \to \neg I (158)$

$(I (161) \lor I (164)) \to \neg I (163)$

$I (162) \to \neg I (169)$

$I (176) \to \neg I (178)$

$(I (180) \lor I (181)) \to \neg I (115)$

$I (128) \to \neg (I (107) \lor I (127))$

$(I (177) \lor (I (27) \land I (176))) \to \neg I (179)$

$I (166) \to \neg I (165)$

$I (168) \to \neg I (167)$

$I (174) \to \neg I (172)$

$(I (135) \land I (140)) \to \neg (I (104) \lor I (141) \lor I (142))$

$(I (22) \land (I (180) \lor I (181))) \to \neg (I (97) \lor I (111))$

5.3. Finding the structured subsets of $T$

Let $I = {(m1), \dots, (m16)}$ be the set of axioms of our meta-level propositional theory about the $SROIQ$ structural constraints on $T = {(a1), \dots, (a185)}$ . As said before, the proposition “ $I (i)$ ” means that the axiom (ai) is included in the TBox. Since $T$ has 185 axioms, there are also 185 corresponding propositions. However, not all of them are required, we only need the 40 propositions mentioned in $I$ , which we collect in the set ${I (22), I (27), I (97), I (104), I (106), I (107), I (111), I (115), I (119), I (127) – I (132), I (134), I (135), I (140) – I (142), I (158) – I (169), I (172), I (174), I (176) - I (181)}$ . Let $U$ be the set of axioms (ai) corresponding to those propositions $I (i)$ . In a sense, $U$ collects the “unsafe axioms of $T$ ,” where the axioms not mentioned in $I$ would be considered “safe,” since together they are known to obey the structural restrictions of regularity and simplicity. This means that the set $T ∖ U$ obeys both regularity and simplicity (is structured), being a $SROIQ$ theory that partially captures UFO-B.

However, $T ∖ U$ does not seem to maximize precision w.r.t. the formalization of UFO-B in FOL. In order to increase precision, we shall find the subsets of $U$ that are structured, and therefore need not be excluded from $T$ . Nevertheless, the search space related to such subsets is $2^{| U |} = 2^{40} = 1099511627776$ . In practice, each solution of the SAT problem related to $I$ represents a structured subset of $T$ .19

¹⁹
Solving a SAT problem with 40 proposition symbols is still unfeasible for our computational resources.

A further inspection reveals that, within $I$ , there are independent subsets of incompatibility rules. For instance, note that (m3) is about $I$ (119) and $I$ (134), and that no other meta-axiom mentions neither $I$ (119) nor $I$ (134). This means that no other meta-axiom influences the possible truth-values of $I$ (119) and $I$ (134). For example, given a model of (m2) in which $I$ (119) is true, there must be another model that only differs from the first by $I$ (119) being false. $I$ (119) and (m2) are independent, and the same for $I$ (134).

Figure 3 shows the independent subsets of the incompatibility rules, abstracting the meta-axioms into sets of the propositions that they mention. In Fig. 3, $I$ is partitioned into 11 independent sub-theories $I_{i}$ , with $(0 ⩽ i ⩽ 10)$ . The idea is that instead of monolithically evaluating all the incompatibility rules together, it is possible to individually evaluate each independent subset of incompatibility rules, and then combine the results later. More specifically, a solution for $I_{i}$ represents a structured subset of $U$ , and since the sub-theories $I_{i}$ are independent, the consecutive union of one solution per $I_{i}$ also represents a structured subset of $U$ .

Fig. 3.

A partition of $I = {(m1), \dots, (m16)}$ into 11 independent sub-theories.

We solved the SAT problem of each of the 11 sub-theories $I_{i}$ of $I$ , obtaining the respective structured subsets of $U$ . The conclusion is that, from all the $2^{40}$ subsets of $U$ , the number of subsets that are structured is $\prod_{i = 0}^{10} | {m | m is a model of I_{i}} | = 28 \cdot 57 \cdot 3 \cdot 41 \cdot 5 \cdot 5 \cdot 3 \cdot 17 \cdot 3 \cdot 3 \cdot 3 = 6757902900$ . This technique was also implemented in our tool.

5.4. Finding the maximally structured subsets of

T

In order to maximize precision w.r.t. $T$ , from all the structured subsets of $U$ , we focus on the maximally structured subsets, i.e., subsets of $U$ such that the inclusion of any other axiom from $U$ generates an unstructured subset of $U$ due to disobeying the regularity or simplicity structural restrictions. Therefore, from all the models of $I$ , we are interested in the ones that represent maximally structured subsets of $U$ .

In practice, the problem of finding a maximally structured subset of $U$ reduces to finding a model of $I$ that is maximal w.r.t. the truthness of the $I (i)$ propositions about including the axiom (ai) in the TBox – Let us call this property “maximally- $I$ .” In such models, the change of any truth-value assignment from false to true generates an interpretation that does not satisfy the meta-theory $I$ , i.e., which is no model of $I$ . Since the sub-theories $I_{i}$ are independent, the consecutive union of one maximally- $I$ model per $I_{i}$ is a maximally- $I$ model of $I$ , which represents a maximally structured subset of $U$ (our target).

However, a maximally structured subset of $U$ concerns only the axioms that are in $U$ , while the sub-theories $T_{j}$ of $T$ that we aim at building deal with the whole $T = {(a1), \dots, (a185)}$ . Since $T$ has more safe axioms than unsafe axioms, instead of informing which axioms from $U$ a $T_{j}$ includes, we present which axioms from $U$ a $T_{j}$ excludes. Also, since in Fig. 4 (Section 6.2) we will refer to the sets of excluded axioms by their indexes, we use tuples instead of sets: $U_{i}$ is a tuple that orders sets of axioms from $U$ , where the user must pick exactly one set from $U_{i}$ to be excluded from $T$ when creating a $SROIQ$ theory $T_{j}$ . $\begin{array}{l} U_{0} = ⟨ {22, 115}, {180, 181} ⟩; \\ U_{1} = ⟨ {107, 127, 129}, {107, 127, 130, 131, 132}, {128, 129}, {128, 132} ⟩; \\ U_{2} = ⟨ {119}, {134} ⟩; \\ U_{3} = ⟨ {104, 106, 141, 142}, {106, 140}, {135} ⟩; \\ U_{4} = ⟨ {158}, {159, 160} ⟩; \\ U_{5} = ⟨ {161, 164}, {163} ⟩; \\ U_{6} = ⟨ {162}, {169} ⟩; \\ U_{7} = ⟨ {27, 177, 178}, {176, 177}, {176, 179}, {178, 179} ⟩; \\ U_{8} = ⟨ {165}, {166} ⟩; \\ U_{9} = ⟨ {167}, {168} ⟩; \\ U_{10} = ⟨ {172}, {174} ⟩ . \end{array}$

Given the 6757902900 structured subsets of $U$ , the number of subsets that are maximally structured is $2 \cdot 4 \cdot 2 \cdot 3 \cdot 2 \cdot 2 \cdot 2 \cdot 4 \cdot 2 \cdot 2 \cdot 2 = 12288$ , leading to 12288 UFO-B $SROIQ$ theories $T_{j}$ .

5.5. Discussion

Each maximally structured sub-theory $T_{j}$ can be defined by choosing exactly one set from each tuple $U_{i}$ . We will briefly discuss some consequences of these choices, which inevitably result in precision loss when compared to the reference ontology.

On $U_{0}$ , by removing (a180) and (a181), one allows the existence of a ProcessualRole r that is inducedBy a ParticipationUniversal u and an Object o that is the participant of an AtomicEvent p that instantiates u, or that is partOf a Participation that instantiates u, and such that o does not plays the ProcessualRole r.

On $U_{0}$ , by removing (a22) and (a115), one allows the existence of an Object that plays a ProcessualRole without instantiating it, and the existence of a ProcessualRole played by no Object.

On $U_{1}$ , removing (a130) allows a ComplexEvent a to have an Event b as part without mereologically overlapping b. Similarly, removing (a131) allows an Event a to be part of a ComplexEvent b without mereologically overlapping b. Removing (a132) loses pretty much the definition of mereologicallyOverlaps as it would allow a ComplexEvent a to have as part an Event b that is part of a ComplexEvent c and such that a and c do not mereologicallyOverlaps.

On $U_{2}$ , by removing (a134) one allows the existence of a Situation that activates a Disposition manifestedBy an Event but that does not triggers the Event.

On $U_{3}$ , removing (a135) allows an AtomicEvent that manifests a Disposition that inheresIn an Object but such that the AtomicEvent does not dependsOn the Object. Removing (a141) allows a Participation to exclusivelyDependsOn less/more than one Object. Removing (a142) allows an Event that exclusivelyDependsOn exactly one Object to not be a Participation.

On $U_{5}$ , by removing (a161) one allows the existence of an Event the endPoint of which precedes the beginPoint of another Event, but such that the first Event does not happen before the second Event.

On $U_{6}$ , removing (a162) allows the existence of an Event the endPoint of which is the beginPoint of another Event, but such that the first Event does not meets the second Event. Removing (a169) allows an Event to meets itself, which should be forbidden since it is a theorem of UFO-B that Events must perdure, they must have their beginPoints different from their endPoints. Removing (a169) also allows two Events to meets each other, which is forbidden for the same reason just discussed.

On $U_{7}$ , by removing (a176) one allows the existence of an Event that bringsAbout a Situation that triggers an Event, but such that the first Event does not directlyCauses the second Event.

Going back to the issue of (a55) being entailed by ${(a 27), (a 56)}$ and (a81) being entailed by ${(a 27), (a 82)}$ (Section 4.2), note that $I$ (27) is in the first set in $U_{7}$ , so the $SROIQ$ theories built from this set do not have (a27). Similarly for (a92), which is entailed by ${(a 91), (a 130)}$ or ${(a 65), (a 131)}$ , where both $I (130)$ and $I (131)$ are in the second set in $U_{1}$ . Finally, (a90) is entailed by ${(a 88), (a 140)}$ , where $I (140)$ is in the second set in $U_{3}$ .

On the other hand, (a89) is entailed by ${(a 88), (a 143)}$ , but neither (a88) nor (a143) are excluded in any set of any $U_{i}$ . This means that we can safely add an optional tuple $U_{11}$ to remove (a89) from $T$ : $\begin{array}{l} U_{11} = ⟨ {89} ⟩ . \end{array}$

Note that while $\approx 0.614628 %$ of the subsets of $U$ are structured, only $\approx 0.000001 %$ of them are maximally structured. Given that finding the structured subsets of $U$ is already a difficult task in terms of time complexity, is it worth to also solve the task of finding the maximally structured subsets?20

²⁰
We thank Frank Loebe (reviewer) for asking for an explanation on the trade-off of guaranteeing structural maximality.

In other words, how bad is it to produce sub-theories

T_{j}

T

that arbitrarily exclude axioms from UFO-B, losing precision without a reasonable computational justification? For instance, just by removing all the 40 unsafe axioms (see

U

) from

T

, one can be sure that the resultant sub-theory

T ∖ U

conforms to regularity and simplicity (is a structured subset of

T

), and so that reasoning on it is decidable. On the other hand, the maximally structured sub-theories remove only 14 to 23 unsafe axioms from

T

Since UFO-B is infrequently updated, selecting the maximally structured $SROIQ$ formalizations is also an infrequent task, and we believe it is not too much of a burden to do it, aiming at sub-theories that capture as much as possible of the reference formalization of UFO-B.

Finally, a problem that is equivalent to the one we dealt with in this section is the problem of finding all the Maximal Satisfiable Subset (MSSes) (Liffiton and Sakallah, 2008) of $U \cup I$ and then collecting only the ones that model $I$ . This is because all axioms in $I$ must be satisfied, while the satisfiability of $U$ should be maximized.

Concerning implementation, we built a (free and open source) Haskell stack package that, given a text file with an ASCII representation of $T$ (using a syntax that we defined), derives both the regularity and simplicity meta-axioms. Since the SAT problem for regularity is hard to solve computationally by means of the technique presented in Codish et al. (2006), but may be easy to solve by hand (as in our case), we also allow the user to provide pre-computed meta-axioms for regularity in a separate file.21

²¹

The user may also provide as input all the meta-axioms for regularity and simplicity (our ${(m1), \dots, (m16)}$ ), instead of $T$ .

The tool returns the tuples

U_{i}

together with some extra data, e.g., on the amount of propositions used and quantities of structured and maximally structured subsets of

U

per

I_{i}

. Regarding computational times, on a machine equipped with Ubuntu 18.10, Intel^® Core™ i7-3520M CPU @ 2.90 GHz × 4, and 5.7 GiB of RAM, and providing

T

and (m1) as input, computing the tuples

U_{i}

took 0.48s of CPU time. The source code is available at https://osf.io/kmvna/, as well as the files used/generated for this paper.

6. Validation

Preparing for expounding the validation in Section 6.2, let us first introduce the final part of the syntax of $SROIQ$ in Section 6.1.

6.1. Individuals in $SROIQ$

Beyond the terminological knowledge, it is often also useful to predicate upon specific individuals (constants) from the universe of discourse. An example in FOL could be “ $Person (Mary)$ .” In $SROIQ$ , this is done by means of an ABox. Let I be a set of individual names, where the sets C (concept names), R (role names), and I (individual names) are mutually disjoint.

Definition 10 (Individual assertion).

Assertions on individuals declare which concepts apply to them and how they relate to each other. Examples are “ $mary : Person$ ,” “ $(mary, john) : motherOf$ ,” “ $(john, mary) : \neg motherOf$ ,” and “ $mary \neq john$ .” More generally, an individual assertion is a formula like $⌜ a : C ⌝$ , $⌜ (a, b) : R ⌝$ , $⌜ (a, b) : \neg R ⌝$ , or $⌜ a \neq b ⌝$ , with $a, b \in I$ , R a role, and C a concept.

Definition 11 (ABox).

An ABox is a finite set of individual assertions.

ABox consistency for $SROIQ$ is decidable (Horrocks et al., 2006).

6.2. Validation by means of ABoxes

In order to empirically evaluate the theories $T_{j}$ derived in the previous section, we codified the $SROIQ$ axioms in OWL 2 DL and checked if they are consistent with instances generated from the reference codification of UFO-B in Alloy.

First, we built a full TBox in OWL 2 DL, which is possibly undecidable since the corresponding set of $SROIQ$ axioms $T = {(a1), \dots, (a185)}$ (presented in Section 4.2) violates both regularity and simplicity. Then, we manually annotated each OWL 2 DL axiom with a label so to have a bijection between the $SROIQ$ axioms of $T$ and the axioms of the full TBox in OWL 2 DL. Thereafter, we used a script supported by the OWLAPI22

²²
http://owlcs.github.io/owlapi/.

to automatically generate, from

T

, an OWL 2 DL TBox_j for each one of the 12288

SROIQ

theories

T_{j}

(as explained in Section 5.5).

For the generation of instances, we used the Alloy Analyzer tool version 5.0.0.1 with a new Alloy codification that exactly corresponds to the FOL axioms shown in Section 3.23

²³

We are not using the original Alloy extended version of UFO-B (Guizzardi et al., 2013).

These models are “fully-consistent,” in the sense that they have at least one instance for each class and relation. In practice, this means that we added to the Alloy codification a new axiom composed of several conjunctions of existential quantifications, one per class or relation of UFO-B. Using Alloy Analyzer, we generated 11 models of the FOL theory, with scope-size – i.e., the cardinality of the domain of quantification – from 25 to 35, where 25 is the minimum scope-size where the Alloy codification is satisfiable, and a maximum of 35 was chosen due to computational time constraints (generating such an instance took more than 24 hours).24

²⁴

Note that, while being models in the technical sense, the models generated by the Alloy Analyzer tool concerning the specification of UFO-B in Alloy are different from the models found by the SAT solver for $I$ .

Each Alloy model was parsed as a collection of individual assertions composing an ABox (using OWLAPI) and joined to each TBox $_{j}$ to form an OWL 2 DL KB. In total, this process produced $12288 \times 11 = 135168$ KBs. We used the DL reasoner Pellet version 2.4.0 to test the consistency of these KBs, all of which are consistent. For each KB, 5 executions of the consistency test were performed,25

²⁵

On a machine equipped with an Intel Core at 3.30 GHz, Ubuntu 15.04, and Sun Java 1.8.

totaling 675840 executions. We present execution times in Fig. 4, in which each

U_{i, k}

represents the sum of all the execution times of TBoxes that remove the k-th set of axioms of the tuple

U_{i}

, for each one of the 11 ABoxes but taking the average of the 5 executions.

Fig. 4.

Execution times concerning the sets $U_{i, k}$ .

In Fig. 4, one can note the difference between the values for $U_{1, 0}$ or $U_{1, 1}$ and the values for $U_{1, 2}$ or $U_{1, 3}$ . What $U_{1, 0}$ and $U_{1, 1}$ have in common is the exclusion of ${107, 127}$ . Interestingly, (a107) is the only axiom in $T$ that states a “ $⩾ 2$ ” cardinality constraint and the cases in which (a107) is removed have the two shortest averages of execution times. On the other hand, “Asy” is removed in other cases, with worse average of execution times. Therefore, it seems that either “ $⩾ 2$ ” alone is an “expensive” operator, or the interplay between “ $⩾ 2$ ” and “Asy” is the culprit. Finally, for all the $U_{i}$ , the sum of the values of each possibility k must be the same ( $\approx 3000$ s); this is not visually apparent in Fig. 4 because the inferior threshold is 500 s instead of zero.

7. Related work

We briefly present some ontologies of events expressible in (decidable) fragments of FOL (Section 7.1), and compare them with UFO-B (Section 7.2).

7.1. Event ontologies

The Event Ontology (EO) (Raimond and Abdallah, 2007a) is probably the lightest and most used ontology of events, supporting a classification based on space (using the WGS84 Positioning Ontology (Brickley, 2006)) and time regions (using the OWL-Time Ontology (Hobbs and Pan, 2017) and Timeline Ontology (Raimond and Abdallah, 2007b)). DOLCE+DnS Ultralite (DUL) is a lightweight foundational ontology, which is a combination and simplification of the Descriptive Ontology for Linguistic and Cognitive Engineering (dolce) (Masolo et al., 2003) and the Constructive Descriptions and Situations (c.DnS) pattern for representing aspects of social reality. The Event-Model-F is a formal model of events based on DUL. It can express events and their mereological, causal and correlative relationships, also allowing the modeler to represent different points of view on the same event. The Linking Open Descriptions of Events (LODE) (Shaw et al., 2009) provides interoperability between Cyc, EO, Event-Model-F, ABC CIDOC CRM, EventsML-G2 and DUL by an analysis based on the “factual” aspects of events, the four Ws: What, Where, When and Who. The Simple Event Model (SEM) (van Hage et al., 2011) allows the modeler to avoid making domain-specific assumptions. It also allows the representation of view points in the description of an event. Finally, the Process Specification Language (PSL) (Grüninger, 2009) was designed to facilitate the exchange of process information among manufacturing systems. PSL is formalized in Common Logic (CL), but since there is a formalization in OWL (Katsumi and Grüninger, 2015), we include it in this discussion, basing our analysis on this formalization of PSL in OWL.

7.2. Comparison with UFO-B

In our comparison, we follow a strategy based on Shaw et al. (2009), focusing on the following aspects:

Agentivity: Similarly to LODE, EO, DUL and PSL, UFO-B is agnostic concerning agentivity (or, more generally, to teleology). Differently, SEM allows for the representation of subjective points of view by means of sem:View. Event-Model-F has also an interpretation pattern that defines an F:Interpretant.

Time: UFO-B follows the usual view of events as entities happening over a time interval, which is expressed by means of the relations ufo-b:beginPoint and ufo-b:endPoint to a class ufo-b:TimePoint. Similarly, SEM uses the roles sem:hasBeginTimeStamp and a sem:hasEndTimeStamp with a literal. PSL uses the roles psl:begins and psl:ends to relate psl:Activity_Ocurrences, psl:Objects and psl:TimeIntervals to psl:TimePoints. EO and LODE use TemporalEntity from OWL-TIME, which allows the representation of intervals, instants, and Allen’s relations between intervals. Note that, due to the syntactic constraints of $SROIQ$ (which guarantee decidability), each of our different UFO-B formalizations allows the representation of some, but not all, aspects of Allen’s temporal relations. DUL has an object property dul:hasEventDate with a codomain dul:TimeInterval, this latter being the domain of dul:hasIntervalDate, a datatype property that encodes values from xsd:date. Note that dul:TimeInterval is also used in Event-Model-F to constrain events.

Space: In UFO-B, “all spatial properties of events are defined in terms of the spatial properties of their participants” (Guizzardi et al., 2013, p. 331). Spatial properties are then inherited from UFO-A, which formalizes the notions of ufo-a:Quality, ufo-a:Quale, ufo-a:QualityUniversal, ufo-a:QualityDomain, and ufo-a:QualityDimension. In PSL, both psl:Activities and psl:Activity_Ocurrences (i.e., types and tokens) relate to psl:Locations by means of the roles psl:occurs_at and psl:ocurred_at, respectively. DUL (followed by LODE) makes a distinction between a region with spatial boundaries (like SpatialThing from the W3C Basic Geo Vocabulary)26

²⁶
https://www.w3.org/2003/01/geo/.

and meaningful places for which spatial boundaries are not mandatory. This distinction is represented by dul:hasRegion (and the generic datatype property dul:hasDataValue) for the former case (lode:inSpace for LODE) and dul:hasLocation for the latter case (lode:atPlace for LODE, sem:hasPlace for SEM). All the instances of sem:Place are symbolic places, nevertheless their location can be attached with various datatypes (e.g., W3C Geospatial Vocabulary27

²⁷

https://www.w3.org/2005/Incubator/geo/XGR-geo/.

and W3C Basic Geo Vocabulary).

Participation: UFO-B considers an event an ufo-b:Participation iff it exclusively depends on a single (possibly inanimate) object; this event is an ufo-b:participationOf of the object. In PSL, a psl:Object psl:participates in a psl:Activity_Ocurrence. The relation psl:participates is specialized into psl:performed_in, which holds between psl:Actors and psl:Activity_Ocurrences. A psl:Actor psl:performs a psl:Activity. Concerning SEM, the codomain sem:Actor of the object property sem:hasActor is a class of individuals that are not “necessarily sentient, so potentially objects i.e. a thing, animate or inanimate, physical or non-physical.” So, ufo-b:participationOf seems equivalent to sem:hasActor, lode:involved, dul:hasParticipant, and eo:factor. UFO-B lacks a more specific participation relation between agents and events, such as lode:involvedAgent, dul:involvesAgent, and eo:agent.

Causality: UFO-B captures causality between events by means of ufo-b:directlyCauses and ufo-b:causes (a sort of transitive closure of ufo-b:directlyCauses). Moreover, UFO-B, DUL, Event-Model-F and EO share the view that events and situations are correlated; e.g., for UFO-B, ufo-b:Situations ufo-b:triggers ufo-b:Events, and ufo-b:Events ufo-b:bringsAbout ufo-b:Situations; while for DUL, dul:Event dul:hasPrecondition (dul:hasPostcondition) dul:Situation. EO can represent such a link by means of the object property eo:factor. Neither LODE nor SEM deal with causality. The fragment of PSL formalized in OWL (Katsumi and Grüninger, 2015) also does not capture causality.

Mereology: UFO-B formalizes an Extensional Mereology (EM) (Casati and Varzi, 1999, p. 40) between events (partitioning events between ufo-b:AtomicEvents and ufo-b:ComplexEvents), but the $SROIQ$ translations can only capture some aspects of the ufo-b:hasPart relation. Interestingly, DUL distinguishes between mereological and temporal parthood; dul:hasPart corresponds to ufo-b:during, and dul:hasConstituent to ufo-b:hasPart. SEM and EO consider a simple theory of parthood on events by means of sem:hasSubEvent (assuming no causality) and eo:sub_event. Event-Model-F is more concerned with an event composition relation than event parthood. This theory relates an F:Event that is F:Composite to all its F:Event F:Components by means of a single F:EventCompositionSituation relationship. An F:EventCompositionSituation satisfies an F:CompositionDescription that defines the structure that “glues” the F:Components in an F:Composite F:Event. PSL formalizes parthood (psl:p) and proper parthood (psl:pp), making no restrictions on their (co)domain. LODE does not deal with parthood relations among events.

Manifestation: UFO-B explains the nature of atomic events in the following way: an ufo-b:Situation ufo-b:activates an ufo-b:Disposition (which ufo-b:inheresIn an ufo-b:Object) which is ufo-b:manifestedBy an ufo-b:AtomicEvent. As far as we know, none of the previously discussed theories provides an explanation for the occurrence of an event. The closest relation to ufo-b:manifestedBy would be an inverse of eo:product (“Everything produced by an event”).

Note that UFO-B does not have a concept of datatype properties because it deals with such entities by means of Qualities, Quales, QualityUniversals and QualityStructures.

Table 1 presents the expressivities, the numbers of logical axioms, classes, object properties (OP) and data properties (DP)28

²⁸

As shown by the Protégé tool, available at: https://protege.stanford.edu/. Note that Protégé claims that the unstructured set $T$ is expressible in $SRIQ$ , while, as discussed in Section 4.1, the presentation of $SRIQ$ in Horrocks et al. (2005) does not provide the construct for asymmetry “Asy,” which we use, and that cannot be enforced by means of RIAs (Horrocks et al., 2006, p. 59).

of some foundational event-based ontologies that have been released over the past years.

Table 1

Metrics about some event ontologies

	Ontology	Expressivity	Axioms	Classes	OP	DP
1	CIDOC CRM	$SR I^{D}$	434	81	130	7
2	DUL	$SHI N^{D}$	600	76	107	5
3	EM-F	$ALCHIQ$	115	38	23	0
4	EO	$SROI N^{D}$	300	31	50	30
5	LODE	$ALHF$	31	13	15	0
6	PSL	$SRIQ$	410	27	42	0
7	SEM	$ALH I^{D}$	53	17	17	7
8	UFO-B	$SRIQ$	186	26	34	0

Note that the OWL 2 DL version of UFO-B has 186 axioms, one more than the 185 axioms of the $SROIQ$ version. This is because we had to reify ${hasPart}^{-}$ . This is also the reason why the OWL 2 DL version of UFO-B has 34 object properties, while the $SROIQ$ version has 33 role names.

The Uniform Resource Locator (URLs) of these ontologies are:

http://purl.org/NET/cidoc-crm/core

http://ontologydesignpatterns.org/ont/dul/DUL.owl

http://events.semantic-multimedia.org/ontology/2008/12/15/model.owl

http://motools.sf.net/event/event.n3

http://linkedevents.org/ontology/2010-10-07/rdfxml/

http://stl.mie.utoronto.ca/ontologies/process_specification_language/psl_loc_actors.owl

http://semanticweb.cs.vu.nl/2009/11/sem/sem.rdf

http://www.nemo.inf.ufes.br/ufo-b/

8. Conclusions

The development of suitable foundational theories is an important step towards the definition of precise semantics and sound methodological principles for modeling complex real-world phenomena. From an engineering point of view, there is also a need for decidable representations of these theories that can support automated reasoning. We address the combination of ontological adequacy and decidability by providing OWL 2 DL TBoxes that (partially) represent the axiomatization of UFO-B.

The difficulty in dealing with the trade-off between expressivity and time complexity when writing a theory in $SROIQ$ lies not only in doing tricky combinations with the constructs of $SROIQ$ to write axioms that correspond to the axioms of the original theory – but also in managing an exponential amount of possibilities concerning incompatibilities between axioms. To deal with this issue, we designed a methodology for the translation from a FOL theory to $SROIQ$ . The large number of codification alternatives of a single reference theory in FOL provides us evidence of the difficulty that a modeler faces when using DLs as the single formalism to specify a reference ontology such as UFO-B. Because of that, we defend an approach which clearly separates reference ontology specification (in FOL) from lightweight ontology codification (in $SROIQ$ ), while ensuring the systematic derivation of the lightweight ontology. The approach guarantees that precision is only sacrificed when required for particular computational goals, in our case, those goals for which $SROIQ$ was designed in the first place. Given the number of possible combinations of axioms to be included in the lightweight ontology, maximizing precision while obtaining desirable computational properties would be too hard to perform manually.

As future work, we intend to investigate alternative DL mappings for the UFO theories presented here, dealing with different aspects of the trade-off between expressivity and tractability. We plan to investigate both mappings to more expressive languages (e.g., including the use of Semantic Web Rule Language (SWRL) for modeling aspects such as the temporal relations between events that could not be captured here) as well as to less expressive languages (e.g., OWL 2 EL) that can support efficient reasoning over large event data sets. Another important question is whether the axioms that were not included in the $SROIQ$ translation are really not expressible in $SROIQ$ and, in that case, whether $SROIQ$ can be extended with additional features such as role negation (Schmidt and Tishkovsky, 2007) or nominal schemata (Krötzsch et al., 2011) without affecting decidability of the reasoning services.

Another interesting future work we intend to investigate is the formalization of both the FOL and $SROIQ$ versions of UFO-B in The Distributed Ontology, Model and Specification Language (DOL) (Object Management Group, 2018) to upload them in Ontohub29

²⁹

https://ontohub.org.

and check their alignment, as any theorem of any

SROIQ

version of UFO-B should correspond to a theorem of the FOL version.

The interested reader can find our input files, the SAT solutions, the Haskell source code, our Alloy codification of UFO-B, the generated Alloy models, the OWL 2 DL TBoxes, and the KBs at https://osf.io/kmvna/.

Footnotes

Acknowledgements

We thank Frank Loebe and the anonymous reviewer for their thorough and constructive comments, which greatly contributed to improving the final version of this article. We also thank Carlos Mencía for his help in validating the structural maximality of our UFO-B $SROIQ$ theories.

On funding, this study was financed in part by the Coordenação de Aperfeiçoamento de Pessoal de Nível Superior – Brasil (CAPES) – Finance Code 001. In particular, the first author is currently supported by the postdoctoral grant with process No. 83740910/18 regarding the “edital FAPES/CAPES No. 10/2018 – Bolsa de Fixação de Doutores (PROFIX).” Moreover, the first two authors were respectively supported by the postdoctoral grants with process No. 71024352 and process No. 71047522 regarding the “edital FAPES/CAPES No. 009/2014 – Bolsa de Fixação de Doutores.” The third author was partly supported by the OCEAN Project (Free University of Bozen-Bolzano) and by the CNPq grant #312158/2015-7. The fifth author was partly supported by the CNPq grants #407235/2017-5 and #312123/2017-5, CAPES grant #23038.028816/2016-41 and FAPES grant #69382549.

Regularity constraints

Providing further details in addition to Section 5, the constraints imposed by regularity are:

Note that, from the constraint (1), assuming $I$ (22) entails “ $plays ≺ instantiates$ .” Moreover, from condition (27), assuming $I$ (180) entails “ $instantiates ≺ plays$ .” Similarly, from case (31), assuming $I$ (181) entails “ $instantiates ≺ plays$ .” Therefore, (a22) is incompatible with both (a180) and (a181). These incompatibilities are captured by the meta axiom (m1) in Section 5.2.1.

The combination of Fig. 5(a) with Fig. 5(b) shows a strict partial order of roles satisfying the regularity syntactic constraint for $T ∖ {(a180), (a181)}$ , while Fig. 5(a) together with Fig. 5(c) shows a strict partial order of roles satisfying the regularity syntactic constraint for $T ∖ {(a22)}$ . Therefore, (m1) seems to be the only incompatibility due to regularity.

Simplicity constraints

First step. We capture the (direct and indirect) sources of non-simplicity:

Note that in the five previous formulae, the set of role names that are in the antecedents (i.e., {plays, directlyCauses, hasPart, dependsOn, and participationOf}) is disjoint from the set of role names that appear in the consequents (i.e., {instantiates, causes, mereologicallyOverlaps, exclusivelyDependsOn}). Therefore, if a role in the first set is made non-simple, it must be by reasons (1), or (2), but not due to (3). This allows us to substitute the non-simplicity of such role names in the first set by disjunctions of the antecedents in (1)–(3) that make them non-simple. Note that, since there is no (direct or indirect) source of non-simplicity for participationOf, it is impossible for “ $\bar{S} (participationOf) \land I (143)$ ” to be true, and hence participationOf has no influence on the non-simplicity of exclusivelyDependsOn.

Second step. We show the axioms forbidden by the non-simplicity of roles:

Note that, from the list above, it suffices to consider only the axioms forbidden by the non-simplicity of roles that were mentioned in the previous step, since other roles would have no other reason to be non-simple than (1)–(3). Therefore, we consider only:

Third step. We perform a composition of the constraints generated in the first step with the constraints generated at the second step. This composition generates our meta-axioms (m2)–(m16) in Section 5.2.2 about the incompatibilities due to the simplicity rule.

References

Allen, J.F. (1983). Maintaining knowledge about temporal intervals. Commun. ACM, 26(11), 832–843. doi:10.1145/182.358434.

Armstrong, D.M. (1989). Universals: An Opinionated Introduction. Focus Series. Westview Press. https://books.google.com.br/books?id=MJzmAAAAIAAJ.

Armstrong, D.M. (2004). Truth and Truthmakers. Cambridge University Press.

Azevedo, C.L.B., Iacob, M., Almeida, J.P.A., van Sinderen, M., Pires, L.F. & Guizzardi, G. (2015). Modeling resources and capabilities in enterprise architecture: A well-founded ontology-based proposal for ArchiMate. Inf. Syst., 54, 235–262. doi:10.1016/j.is.2015.04.008.

Batsakis, S., Petrakis, E.G.M., Tachmazidis, I. & Antoniou, G. (2017). Temporal representation and reasoning in OWL 2. Semantic Web, 8(6), 981–1000. doi:10.3233/SW-160248.

Benevides, A.B., Bourguet, J., Guizzardi, G. & Peñaloza, R. (2017). Representing the UFO-B foundational ontology of events in SROIQ. In Proceedings of the Joint Ontology Workshops 2017 Episode 3: The Tyrolean Autumn of Ontology, Bozen-Bolzano, Italy, September 21–23, 2017. http://ceur-ws.org/Vol-2050/FOUST_paper_7.pdf.

Biere, A., Heule, M., van Maaren, H. & Walsh, T. (Eds.) (2009). Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications (Vol. 185). IOS Press.

Bourguet, J., Guizzardi, G., Benevides, A.B. & Zamborlini, V. (2017). Empirically evaluating three proposals for representing changes in OWL2. In Proceedings of the Joint Ontology Workshops 2017 Episode 3: The Tyrolean Autumn of Ontology, Bozen-Bolzano, Italy, September 21–23, 2017. http://ceur-ws.org/Vol-2050/DEW_paper_4.pdf.

Brickley, D. (2006). W3C Semantic Web Interest Group: Basic Geo (WGS84 lat/long) Vocabulary. Online. Last accessed at 1st. July 2019, https://www.w3.org/2003/01/geo/.

10.

Carolo, F. & Burlamaqui, L. (2011). Improving web content management with semantic technologies. In Semantic Technology Conference (SemTech), San Francisco.

11.

Casati, R. & Varzi, A. (2015). Events. In

E.N.

Zalta (Ed.), The Stanford Encyclopedia of Philosophy (Winter 2015 ed.). Metaphysics Research Lab, Stanford University.

12.

Casati, R. & Varzi, A.C. (1999). Parts and Places: The Structures of Spatial Representation. MIT Press.

13.

Codish, M., Lagoon, V. & Stuckey, P.J. (2006). Solving partial order constraints for LPO termination. In

Pfenning (Ed.), Term Rewriting and Applications, 17th International Conference, RTA 2006, Proceedings, Seattle, WA, USA, August 12–14, 2006. Lecture Notes in Computer Science (Vol. 4098, pp. 4–18). Springer. doi:10.1007/11805618_2.

14.

Daly, C. (1994). Tropes. In Proceedings of the Aristotelian Society. New Series (Vol. 94, pp. 253–261). Wiley. JSTOR. https://www-jstor-org.web.bisu.edu.cn/stable/4545197.

15.

de Souza, É.F., de Almeida Falbo, R. & Vijaykumar, N.L. (2017). ROoST: Reference ontology on software testing. Applied Ontology, 12(1), 59–90. doi:10.3233/AO-170177.

16.

Duarte, B.B., Souza, V.E.S., de Castro Leal, A.L., de Almeida Falbo, R., Guizzardi, G. & Guizzardi, R.S.S. (2016). Towards an ontology of requirements at runtime. In

Ferrario and

Kuhn (Eds.), Formal Ontology in Information Systems – Proceedings of the 9th International Conference, FOIS 2016, Annecy, France, July 6–9, 2016, Frontiers in Artificial Intelligence and Applications (Vol. 283, pp. 255–268). IOS Press. doi:10.3233/978-1-61499-660-6-255.

17.

Grüninger, M. (2009). Using the PSL ontology. In

Staab and

Studer (Eds.), Handbook on Ontologies. International Handbooks on Information Systems (pp. 423–443). Springer. doi:10.1007/978-3-540-92673-3_19.

18.

Guizzardi, G. (2005). Ontological foundations for structural conceptual models. PhD Thesis. Enschede, The Netherlands, Enschede.

19.

Guizzardi, G. (2006). On ontology, ontologies, conceptualizations, modeling languages, and (meta) models. In

Vasilecas ,

Eder and

Caplinskas (Eds.), Databases and Information Systems IV – Selected Papers from the Seventh International Baltic Conference, DB&IS, Vilnius, Lithuania, July 3–6, 2006, Frontiers in Artificial Intelligence and Applications (Vol. 155, pp. 18–39). IOS Press. http://www.booksonline.iospress.nl/Content/View.aspx?piid=5421.

20.

Guizzardi, G., de Almeida Falbo, R. & Guizzardi, R.S.S. (2008). Grounding software domain ontologies in the unified foundational ontology (UFO): the case of the ODE software process ontology. In

Lencastre ,

J.F.E.

Cunha and

Valecillo (Eds.), Memorias de la XI Conferencia Iberoamericana de Software Engineering (CIbSE 2008), Recife, Pernambuco, Brasil February 13–17, 2008, (pp. 127–140).

21.

Guizzardi, G. & Wagner, G. (2004). A unified foundational ontology and some applications of it in business modeling. In

Grundspenkis and

Kirikova (Eds.), CAiSE’04 Workshops in Connection with the 16th Conference on Advanced Information Systems Engineering. Riga, Latvia, 7–11 June, 2004, Knowledge and Model Driven Information Systems Engineering for Networked Organisations, Proceedings (Vol. 3, pp. 129–143). Faculty of Computer Science and Information Technology, Riga Technical University. Riga, Latvia.

22.

Guizzardi, G., Wagner, G., de Almeida Falbo, R., Guizzardi, R.S.S. & Almeida, J.P.A. (2013). Towards ontological foundations for the conceptual modeling of events. In

Ng ,

V.C.

Storey and

Trujillo (Eds.), Conceptual Modeling – 32th International Conference, ER 2013, Proceedings, Hong-Kong, China, November 11–13, 2013, Lecture Notes in Computer Science (Vol. 8217, pp. 327–341). Springer. doi:10.1007/978-3-642-41924-9_27.

23.

Guizzardi, R.S.S., Li, F., Borgida, A., Guizzardi, G., Horkoff, J. & Mylopoulos, J. (2014). An ontological interpretation of non-functional requirements. In

Garbacz and

Kutz (Eds.), Formal Ontology in Information Systems – Proceedings of the Eighth International Conference, FOIS 2014, Rio de Janeiro, Brazil, September, 22–25, 2014, Frontiers in Artificial Intelligence and Applications (Vol. 267, pp. 344–357). IOS Press. doi:10.3233/978-1-61499-438-1-344.

24.

Hobbs, J.R. & Pan, F. (2017). Time ontology in OWL. Technical report OGC 16-071r2, W3C/OGC. Last accessed at 1st. July 2019. https://www.w3.org/TR/owl-time/.

25.

Horrocks, I., Kutz, O. & Sattler, U. (2005). The irresistible SRIQ. In

B.C.

Grau ,

Horrocks ,

Parsia and

P.F.

Patel-Schneider (Eds.), Proceedings of the OWLED*05 Workshop on OWL: Experiences and Directions. Galway, Ireland, November 11–12, 2005, CEUR Workshop Proceedings. CEUR-WS.org http://ceur-ws.org/Vol-188/sub20.pdf.

26.

Horrocks, I., Kutz, O. & Sattler, U. (2006). The Even More Irresistible

SROIQ

. In Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2–5, 2006 (pp. 57–67). http://www.aaai.org/Library/KR/2006/kr06-009.php.

27.

Jackson, D. (2012). Software Abstractions: Logic, Language, and Analysis. MIT Press.

28.

Katsumi, M. & Grüninger, M. (2015). Using PSL to extend and evaluate event ontologies. In

Bassiliades ,

Gottlob ,

Sadri ,

Paschke and

Roman (Eds.), Rule Technologies: Foundations, Tools, and Applications – 9th International Symposium, RuleML 2015, Proceedings, Berlin, Germany, August 2–5, 2015, Lecture Notes in Computer Science (Vol. 9202, pp. 225–240). Springer. doi:10.1007/978-3-319-21542-6_15.

29.

Krötzsch, M., Maier, F., Krisnadhi, A. & Hitzler, P. (2011). A better uncle for OWL: Nominal schemas for integrating rules and ontologies. In

Srinivasan ,

Ramamritham ,

Kumar ,

M.P.

Ravindra ,

Bertino and

Kumar (Eds.), Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28–April 1, 2011, (pp. 645–654). ACM. doi:10.1145/1963405.1963496.

30.

Krötzsch, M., Simancik, F. & Horrocks, I. (2012). A description logic primer. CoRR. http://arxiv.org/abs/1201.4089v3.

31.

Liffiton, M.H. & Sakallah, K.A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1), 1–33. doi:10.1007/s10817-007-9084-z.

32.

Loebe, F. (2003). An analysis of roles: Towards ontology-based modelling. Onto-Med Report No. 6, University of Leipzig, Germany. http://www.onto-med.de/publications/2003/loebe-f-2003-a.pdf.

33.

Loebe, F. (2007). Abstract vs. social roles – towards a general theoretical account of roles. Applied Ontology, 2(2), 127–158. http://content.iospress.com/articles/applied-ontology/ao031.

34.

Masolo, C., Borgo, S., Gangemi, A., Guarino, N. & Oltramari, A. (2003). WonderWeb Deliverable D18. Resreport Del 18, ISTC-CNR. Last accessed at 1st. July 2019, http://wonderweb.man.ac.uk/deliverables/documents/D18.pdf.

35.

Nardi, J.C., de Almeida Falbo, R. & Almeida, J.P.A. (2014). An ontological analysis of service modeling at ArchiMate’s business layer. In

Reichert ,

Rinderle-Ma and

Grossmann (Eds.), 18th IEEE International Enterprise Distributed Object Computing Conference, EDOC 2014, Ulm, Germany, September 1–5, 2014 (pp. 92–100). IEEE Computer Society. doi:10.1109/EDOC.2014.22.

36.

Object Management Group (2018). The Distributed Ontology, Modeling, and Specification Language. Technical report formal/18-09-02, OMG Headquarters, 109 Highland Avenue, Needham, MA 02494, USA. Last accessed at 1st. July 2019, https://www.omg.org/spec/DOL/1.0/PDF.

37.

Pena, R.A.P. (2012). Suporte semântico à publicação de conteúdo jornalístico na Web. Mathesis. Programa de Pós-graduação em Informática do Departamento de Informática do Centro Técnico e Científico da PUC-Rio., Rio de Janeiro. doi:10.17771/PUCRio.acad.20235.

38.

Raimond, Y. & Abdallah, S. (2007a). The event ontology. Online. Last accessed at 1st. July 2019, http://motools.sf.net/event/event.html.

39.

Raimond, Y. & Abdallah, S. (2007b). The Timeline Ontology. Online. Last accessed at 1st. July 2019, http://motools.sf.net/timeline/timeline.html.

40.

Santos, P.S.Jr., Almeida, J.P.A. & Guizzardi, G. (2010). An ontology-based semantic foundation for ARIS EPCs. In

S.Y.

Shin ,

Ossowski ,

Schumacher ,

M.J.

Palakal and

Hung (Eds.), Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22–26, 2010 (pp. 124–130). ACM. doi:10.1145/1774088.1774114.

41.

Schmidt, R.A. & Tishkovsky, D. (2007). Deciding ALBO with Tableau. In

Calvanese ,

Franconi ,

Haarslev ,

Lembo ,

Motik ,

Turhan and

Tessaris (Eds.), Proceedings of the 2007 International Workshop on Description Logics (DL2007), Brixen-Bressanone, Near Bozen-Bolzano, Italy, 8–10 June, 2007, CEUR Workshop Proceedings. CEUR-WS.org, Italy. http://ceur-ws.org/Vol-250/paper_75.pdf.

42.

Shaw, R., Troncy, R. & Hardman, L. (2009). LODE: Linking open descriptions of events. In

Gómez-Pérez ,

Yu and

Ding (Eds.), The Semantic Web, Fourth Asian Conference, ASWC 2009, Proceedings, Shanghai, China, December 6–9, 2009, Lecture Notes in Computer Science (Vol. 5926, pp. 153–167). Springer. doi:10.1007/978-3-642-10871-6_11.

43.

van Hage, W.R., Malaisé, V., Segers, R., Hollink, L. & Schreiber, G. (2011). Design and use of the Simple Event Model (SEM). J. Web Semant., 9(2), 128–136. doi:10.1016/j.websem.2011.03.003.

44.

W3C (2012). OWL 2 Web Ontology Language Document Overview (2nd ed.). Last accessed at 1st. July 2019, https://www.w3.org/TR/owl2-overview/.

45.

Werlang, R. (2015). Ontology-based approach for standard formats integration in reservoir modeling. In Mathesis, Universidade Federal do Rio Grande do Sul. Instituto de Informática. Programa de Pós-Graduação em Computação., Porto Alegre. http://hdl.handle.net/10183/115196.

46.

Zamborlini, V. & Guizzardi, G. (2010). On the representation of temporally changing information in OWL. In Workshops Proceedings of the 14th IEEE International Enterprise Distributed Object Computing Conference, EDOCW 2010, 25–29 October, 2010 (pp. 283–292). Vitória, Brazil: IEEE Computer Society. doi:10.1109/EDOCW.2010.50.

Representing a reference foundational ontology of events in SROIQ

Abstract

Keywords

1. Introduction

2. Challenges and methodology

1 A subset of T is maximal w.r.t. obeying regularity and simplicity if and only if (iff) the inclusion of any other axiom generates a subset that is not a SROIQ ontology due to disobeying the regularity or simplicity restrictions.

3 In simple words, an urelement is something that can be an element of a set, but is not a set itself.

4 As noted by Frank Loebe (reviewer), this hasPart relation is neither the parthood relation of UFO-A (which holds between objects) nor a general parthood relation. The (co)domain of hasPart is Event. When unifying UFO-A and UFO-B, hasPart should be renamed to eventHasPart.

3.5. Temporal relations between events: (T1)–(T14′)

3.6. World changes and situations: (S1′)–(S8)

3.7. Processual roles: (R1)–(R2)

7 We avoid here the difficult task of providing an epistemological explanation for ongoing events.

8 Note that by “relationship” we mean a tuple from a relation.

4. The unstructured set of UFO-B SROIQ axioms

4.1. Concepts and roles in SROIQ

10 By “name,” we mean a finite string.

11 We use the symbols “⌜” and “⌝” to denote quasi-quotation. Moreover, note that the role inversion operator “ − ” can only be applied to role names. So, one cannot write “ R − − ” meaning “R.”

Definition 3 (General concept inclusion axiom).

Definition 4 (Role assertion).

12 The construct “Asy” is called “antisymmetry” in Horrocks et al. (2006, p. 59), but we think that the provided semantics of “Asy” is of asymmetry.

14 In Horrocks et al. (2006, p. 58), role composition is denoted by the juxtaposition of roles, e.g., “ fatherOf motherOf .” Here, we use the symbol “∘” for clarity.

Definition 7 (TBox).

4.2. The set T

4.2.1. Formalization of Figs 1 and 2

4.2.2. Universals and individuals: (a121)–(a124)

4.2.3. Event mereology: (a125)–(a133)

15 Since asymmetry entails irreflexivity, and both “Irr” and “Asy” obey the very same SROIQ syntactic constraints (as we will see in Section 5.1, “Irr” and “Asy” only apply to simple roles), then whenever a role is asymmetric, there is no benefit in also asserting its irreflexivity.

4.2.5. On the participation of objects in events: (a140)–(a142)

4.2.6. Temporal relations between events: (a144)–(a174)

4.2.8. Processual roles: (a180)–(a181)

4.2.9. Qualities and quality structures

4.2.10. The creation, termination and change of objects: (a182)–(a185)

5. UFO-B SROIQ theories: The maximally structured subsets of T

5.1. The structural restrictions of SROIQ

Definition 8 (Simplicity).

5.2.1. Incompatibilities due to regularity

5.2.2. Incompatibilities due to simplicity

5.3. Finding the structured subsets of T

19 Solving a SAT problem with 40 proposition symbols is still unfeasible for our computational resources.

5.5. Discussion

20 We thank Frank Loebe (reviewer) for asking for an explanation on the trade-off of guaranteeing structural maximality.

6.1. Individuals in SROIQ

Definition 10 (Individual assertion).

Definition 11 (ABox).

6.2. Validation by means of ABoxes

22 http://owlcs.github.io/owlapi/.

7.1. Event ontologies

7.2. Comparison with UFO-B

26 https://www.w3.org/2003/01/geo/.

Footnotes

Acknowledgements

Regularity constraints

Simplicity constraints

References

¹
A subset of $T$ is maximal w.r.t. obeying regularity and simplicity if and only if (iff) the inclusion of any other axiom generates a subset that is not a $SROIQ$ ontology due to disobeying the regularity or simplicity restrictions.

³
In simple words, an urelement is something that can be an element of a set, but is not a set itself.

⁴
As noted by Frank Loebe (reviewer), this hasPart relation is neither the parthood relation of UFO-A (which holds between objects) nor a general parthood relation. The (co)domain of hasPart is Event. When unifying UFO-A and UFO-B, hasPart should be renamed to eventHasPart.

⁷
We avoid here the difficult task of providing an epistemological explanation for ongoing events.

⁸
Note that by “relationship” we mean a tuple from a relation.

4. The unstructured set of UFO-B $SROIQ$ axioms

4.1. Concepts and roles in $SROIQ$

¹⁰
By “name,” we mean a finite string.

¹¹
We use the symbols “⌜” and “⌝” to denote quasi-quotation. Moreover, note that the role inversion operator “ $^{-}$ ” can only be applied to role names. So, one cannot write “ $R^{- -}$ ” meaning “R.”

¹²
The construct “Asy” is called “antisymmetry” in Horrocks et al. (2006, p. 59), but we think that the provided semantics of “Asy” is of asymmetry.

¹⁴
In Horrocks et al. (2006, p. 58), role composition is denoted by the juxtaposition of roles, e.g., “ $fatherOf motherOf$ .” Here, we use the symbol “∘” for clarity.

4.2. The set $T$

5. UFO-B $SROIQ$ theories: The maximally structured subsets of $T$

5.1. The structural restrictions of $SROIQ$

5.3. Finding the structured subsets of $T$

¹⁹
Solving a SAT problem with 40 proposition symbols is still unfeasible for our computational resources.

²⁰
We thank Frank Loebe (reviewer) for asking for an explanation on the trade-off of guaranteeing structural maximality.

6.1. Individuals in $SROIQ$

²²
http://owlcs.github.io/owlapi/.

²⁶
https://www.w3.org/2003/01/geo/.