Representing the UFO-B Foundational Ontology of Events in SROIQ Alessander BOTTI BENEVIDES a,1 , Jean-Rémi BOURGUET a , Giancarlo GUIZZARDI a,b , Rafael PEÑALOZA b a NEMO, Computer Science Department, Federal University of Espı́rito Santo, Brazil b Faculty of Computer Science, Free University of Bozen-Bolzano, Italy 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 success- fully employed as a reference model for addressing problems from complex media management, enterprise architecture, software engineering, and modeling of events in petroleum exploration. Despite that, 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. Keywords. Knowledge representation, Formal Ontology, Ontology of Events, Description Logics, OWL 1. Introduction 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 a particular philosophically well-founded ontology of events termed Unified Foundational Ontology—Part B (UFO-B) [1]. Dealing with the proper representation of subtle aspects of events is fundamental for a multitude of areas such as bioinformatics, finances, and public safety. In particular, the UFO-B ontology has been extensively tested in practice and successfully employed as a reference model for addressing problems from complex media management, enterprise architecture, software engineering, and the modeling of events in petroleum exploration. 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 1 Corresponding Author: Av. Fernando Ferrari, 514, Goiabeiras, Vitória, BR; E-mail: abbenevides@inf.ufes.br. event relations. 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 [2]) to the Description Logic (DL) SROIQ [3], which is the formal underpinning of the OWL 2 Web Ontology Language (OWL 2 DL) [4]. The remainder of this paper is structured as follows. Section 2 briefly presents the original axioms of UFO-B together with mappings to SROIQ, discussing the challenges in mapping these two formalisms and arguing that representing the totality of UFO-B in SROIQ results in an ill-formed theory. In order to address the latter problem, in Section 3 we propose a number of translations that are maximal w.r.t. the syntactic constraints of SROIQ, i.e., theories such that the inclusion of any other axiom makes them ill-formed. These translations are evaluated by means of codifications in OWL 2 DL terminology boxes (TBoxes), 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). Section 4 presents some final considerations. 2. The Original FOL Formalization of UFO-B and a Translation to SROIQ First, we present some notational conventions: (i) FOL predicates and DL concepts/roles are denoted in Uppercase typewriter type; (ii) we employ restricted quantification à la Frege, i.e., “∀x:T (ϕ)” is a schema for “∀x(T (x) → ϕ),” and “∃x:T (ϕ)” for “∃x(T (x) ∧ ϕ));” and (iii) we homogenized the names of relations defined in [1] by expanding abbreviations and replacing the forms ‘x-y’ or ‘x y’ with ‘xY’. {subsets causes} Individual /directlyCauses {disjoint} /causes * * * * Endurant Event /exclusivelyDependsOn {disjoint} 2..* * * * * 1 1 * Trope 1..* inheresIn 1 Object /participationOf * /Participation hasPart 1 dependsOn * {disjoint,complete} * Situation * activates * Disposition 1 manifestedBy * AtomicEvent ComplexEvent triggers 11 1 triggers * bringsAbout 1..* obtainsIn 0..1 1 J beginPoint Fact 1..* obtainsIn 1 TimePoint 1 JendPoint Figure 1. The union of the five class diagrams shown in [1, Figures. 1–5]. Dotted lines represent our additions. UFO-B extended UFO-A [5] to deal with events (Figure 1), and was formalized by means of FOL formulae in [1] and also by means of an external Alloy codification. Here, we consider only the theory in [1], which is structured as follows: a definition of a parthood relation for events (Section 2.1); an explanation of the nature of events as manifestations of object dispositions (Section 2.2); constraints on how objects participate in events, and how events depend on objects (Section 2.3); an optional linear time structure and a temporal constraint on parthood (Section 2.4); and the view of events as the entities responsible for world changes, a sort of transition between situations (Section 2.5).2 2 In the ontological stance adopted here, the codomain of the relation inheresIn is not restricted to Objects, since Events could also bear Tropes (we thank a reviewer for bringing that to our attention). Moreover, Trope is not the domain of inheresIn, since objectified intrinsic properties in general (e.g., modes [5]) inhere sIn other We formalize the (co)domain and cardinality constraints of relations according to their orientations. Two relation names occur twice in Figure 1: obtainsIn and triggers. We interpret the obtainsIn from Fact to TimePoint as a constraint on the domain of obtainsIn in case the first argument is a Fact (a51). On triggers, (i) as shown in [1, Figure 4], the codomain of triggers is Event (a30); (ii) in case of AtomicEvents, we have that a Situation triggers AtomicEvent if and only if (iff) there is a Dispo- sition that is activated by the Situation and is manifestedBy the AtomicEvent [1, D3]. Finally, TimePoint and Indiviual are disjoint (a40). Subsumptions a4 SituationvEndurant a8 AtomicEvent v Event a5 Trope v Endurant a9 ComplexEventvEvent a1 EndurantvIndividual a6 Disposition v Trope a10 ParticipationvEvent a2 Event v Individual a7 Fact v Situation a11 directlyCausesvcauses a3 Object v Endurant Domain Constraints a18 ∃causes.> v Event a19 ∃directlyCauses.> v Event a12 ∃inheresIn.> v Trope a20 ∃activates.> v Situation a13 ∃hasPart.> v ComplexEvent a21 ∃manifestedBy.> v Disposition a14 ∃dependsOn.> v AtomicEvent a22 ∃beginPoint.> v Event a15 ∃obtainsIn.> v Situation a23 ∃endPoint.> v Event a16 ∃triggers.> v Situation a24 ∃exclusivelyDependsOn.>vParticipation a17 ∃bringsAbout.> v Event a25 ∃participationOf.> v Participation Codomain Constraints a32 > v ∀causes.Event a33 > v ∀directlyCauses.Event a26 > v ∀inheresIn.Object a34 > v ∀activates.Disposition a27 > v ∀hasPart.Event a35 > v ∀manifestedBy.AtomicEvent a28 > v ∀dependsOn.Object a36 > v ∀beginPoint.TimePoint a29 > v ∀obtainsIn.TimePoint a37 > v ∀endPoint.TimePoint a30 > v ∀triggers.Event a38 > v ∀exclusivelyDependsOn.Object a31 > v ∀bringsAbout.Situation a39 > v ∀participationOf.Object Disjointness a42 (Object u Trope) v ⊥ a43 (Object u Situation) v ⊥ a40 (TimePoint u Individual) v ⊥ a44 (Trope u Situation) v ⊥ a41 (Endurant u Event) v ⊥ a45 (AtomicEvent u ComplexEvent) v ⊥ Completeness a46 Event v (AtomicEvent t ComplexEvent) Domain Cardinality Constraints a47 Trope v (=1inheresIn.Object) a48 ComplexEvent v (≥2hasPart.Event) a49 AtomicEvent v (=1dependsOn.Object) Individuals. We ask the reader to interpret inheresIn here as ‘tropeInheresInObject,’ a specialization of the inherence relation. In an extension of this paper, we deal with Events bearing Tropes and qualities. a50 Situation v (≤1obtainsIn.TimePoint) a51 Fact v (=1obtainsIn.TimePoint) a52 Event v (=1bringsAbout.Situation) a53 Event v (=1beginPoint.TimePoint) a54 Event v (=1endPoint.TimePoint) a55 Participation v (=1exclusivelyDependsOn.Object) a56 Participation v (=1participationOf.Object) Codomain Cardinality Constraints a57 Object v (≥1inheresIn− .Trope) a58 TimePoint v (≥1obtainsIn− .Situation) a59 Event v (=1triggers− .Situation) a60 AtomicEvent v (=1manifestedBy− .Disposition) 2.1. Event Mereology: (M1)–(M9) Events may be composite, 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. An event is atomic iff it has no parts (M1), and complex otherwise (M2). (M7) determines when two complex events mereologically overlap. UFO-B uses the same predicate ‘overlaps’ for mereological overlapping and temporal overlapping. Here, we call them mereologi- callyOverlaps and temporallyOverlaps, respectively. UFO-B also commits to weak supplementation [6, 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 [6, p. 39, (P.5)] (M8), which renders a theory in which two entities cannot have all proper parts in common, as shown by the theorem of extensionality [6, p. 40, (3.15)] (our (M9)). M1 ∀e:Event(AtomicEvent(e) ↔ ¬∃e0 :Event(hasPart(e, e0 ))) M2 ∀e:Event(ComplexEvent(e) ↔ ¬AtomicEvent(e)) M3 ∀e:ComplexEvent(¬hasPart(e, e)) M4 ∀e, e0 :ComplexEvent(hasPart(e, e0 ) → ¬hasPart(e0 , e)) M5 ∀e, e0 :ComplexEvent, e00 :Event((hasPart(e, e0 ) ∧ hasPart(e0 , e00 )) → hasPart(e, e00 )) M6 ∀e:ComplexEvent, e0 :Event(hasPart(e, e0 ) → ∃e00 :Event(hasPart(e, e00 ) ∧ ¬mereologicallyOverlaps(e0 , e00 ))) M7 ∀e, e0 :ComplexEvent(Overlaps(e, e0 ) ↔ (hasPart(e, e0 ) ∨ hasPart(e0 , e) ∨ ∃e00 :Event(hasPart(e, e00 ) ∧ hasPart(e0 , e00 )))) M8 ∀e, e0 :ComplexEvent((∀e00 :Event(hasPart(e, e00 ) → hasPart(e0 , e00 ))) → (e = e0 ∨ hasPart(e0 , e))) M9 ∀e, e0 :ComplexEvent(e = e0 ↔ ∀e00 :Event(hasPart(e, e00 ) ↔ hasPart(e0 , e00 ))) [3, p. 67] recognizes the inexpressibility of mereological notions in SROIQ, as its syntactic constraints forbid roles to be asymmetric and transitive. For (M1), we capture the necessary condition (indicated by ‘−’) of AtomicEvent in (a61), and the sufficient condition (indicated by ‘+’) in (a62). An absence of ‘−’ or ‘+’ means equivalence. (M2) is enforced by (a45) and (a46). (M3), (M4) and (M5) are captured by (a63), (a64) and (a65), respectively. (a65) makes hasPart non-simple,3 which forbids its use in (a63) and (a64). 3 Let v+ be the transitive closure of v. A role R is non-simple iff Tra(R) or Sym(R); or there is a role composition τ s.t. τ v+ R; or R− is non-simple. A role is simple iff it is not non-simple. The ‘simplicity’ syntactic rule forbids non-simple roles to be used in (i) concepts of the form ‘∃R.Sel f ’ and ‘SnR.C’, and (ii) role assertions of the form ‘Irr(R),’ ‘Asy(R)’ and ‘Dis(R, S).’ See [3, p. 59]. For (M7), (a66)–(a68) represent the sufficient conditions for mereologicallyOverlaps, where (a68) makes mereologicallyOverlaps non-simple. The necessary condition for this role seems inexpressible, as the right-side of a role inclusion axiom (RIA) [3, p. 58] can only have a role name. The non-simplicity of hasPart by (a65) makes mereo- logicallyOverlaps non-simple by (a66) or (a67). (M6) seems inexpressible even by assuming a definition of mereologicallyOverlaps, e.g., “Ref(hasAtLeastTwoDis- jointParts)” with the ill-formed formula “hasAtLeastTwoDisjointParts ≡ has- Part ◦ notMereologicallyOverlap ◦ hasPart− ” would 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, notMereolog- icallyOverlap is inexpressible, e.g., even by removing the axioms that make mereo- logicallyOverlaps non-simple and asserting “Dis(mereologicallyOverlaps,not- MereologicallyOverlap),” SROIQ could not express that one relation would be the set-complement of the other, i.e., the ill-formed formula “Uv mereologically- Overlaps t notMereologicallyOverlap.” Finally, it seems that (M8) and (M9) are inexpressible, since there is no way to express an equality on “generic individuals.” a61 AtomicEvent v Event u ¬∃hasPart.Event (M1)− a62 Event u ¬∃hasPart.Event v AtomicEvent (M1)+ a63 ComplexEvent v ¬(∃hasPart.Sel f ) (M3) a64 Dis(hasPart, hasPart− ) (M4) a65 Tra(hasPart) (M5) a66 hasPart v mereologicallyOverlaps (M7)+ a67 hasPart− v mereologicallyOverlaps (M7)+ a68 hasPart ◦ hasPart− v mereologicallyOverlaps (M7)+ 2.2. Events as Manifestations of Object Dispositions: (D1)–(D4) Atomic events are manifestations of (the inverse of manifestedBy) unique object dis- positions (D2). Dispositions inheresIn  a unique object (D1). Whenever a disposition inheresIn an object and is manifestedBy an event, the event dependsOn the object (D4). A situation triggers an atomic event iff there is a disposition that is activated by (the inverse of activates) the situation and that is manifestedBy the event (D3). D1 ∀d:Disposition(∃!o:Object(inheresIn(d, o))) D2 ∀e:AtomicEvent(∃!d:Disposition(manifestedBy(d, e))) D3 ∀s:Situation, e:AtomicEvent(triggers(s, e) ↔ ∃d:Disposition(activates(s, d) ∧ manifestedBy(d, e))) D4 ∀d:Disposition, e:AtomicEvent, o:Object((manifestedBy(d, e) ∧ inheresIn(d, o)) → dependsOn(e, o)) (D1) is guaranteed by (a6) and (a47), while (D2) is guaranteed by (a60). As the right-side of a RIA can only have a role name, it seems that only the sufficient condition of (D3) can be formalized as (a69). (D4) is captured by (a70). (a69) and (a70) make triggers and dependsOn non-simple, respectively. a69 activates ◦ manifestedBy v triggers (D3)+ a70 manifestedBy− ◦ inheresIn v dependsOn (D4) 2.3. On the Participation of Objects in Events: (P1)–(P5) Objects participate not only in the atomic events that are manifestations of their disposi- tions, but also in the complex events that have such manifestations as parts; e.g., Caesar participates in both “Caesar’s death” and “the murder of Caesar.” As an atomic event is a manifestation of a unique disposition (D2), which inheresIn a unique object (D1), by (D4) it follows that atomic events dependsOn  unique objects (P1). exclusivelyDe- pendsOn generalizes dependsOn to complex events (P2). By composing the relations hasPart and exclusivelyDependsOn, complex events exclusivelyDependsOn  the objects that its parts exclusivelyDependsOn (P3). A Participation is an event that exclusivelyDependsOn a unique object (P4). A participationOf relation from par- ticipations to objects can be defined by means of exclusivelyDependsOn (P5). P1 ∀e:AtomicEvent ∃!o:Object(dependsOn(e, o)) P2 ∀e:AtomicEvent, o:Object(exclusivelyDependsOn(e, o) ↔ dependsOn(e, o)) P3 ∀e:ComplexEvent, o:Object(exclusivelyDependsOn(e, o) ↔ ∀e0 :Event(hasPart(e, e0 ) → exclusivelyDependsOn(e, o))) P4 ∀e:Event(Participation(e) ↔ ∃!o:Object(exclusivelyDependsOn(e, o))) P5 ∀o:Object, p:Participation(participationOf(p, o) ↔ exclusivelyDependsOn(p, o)) (P1) is guaranteed by (a49). 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 (a71) 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), together, (a10) and (a55) entail the necessary condition for being a par- ticipation, while (a72) entails the sufficient condition. On (P5), since both relations par- ticipationOf and exclusivelyDependsOn have the same domain (Participation, see (a24), (a25)) and the same codomain (Object, see (a38), (a39)), the left-to-right implication can be modeled as “participationOf v exclusivelyDependsOn,” while the right-to-left implication by “exclusivelyDependsOn v participationOf,” i.e., the relations are equivalent. Due to the regularity constraint,4 such role equivalence is inexpressible in SROIQ. However, one can remove one of the relations from the signature of the theory with no loss of expressivity (see [3, Footnote 2]). a71 dependsOn v exclusivelyDependsOn (P2)− a72 Event u (=1exclusivelyDependsOn.Object) v Participation (P4)+ 2.4. Temporal Relations Between Events: (T1)–(T14’) [1, T7–T13] formalizes the temporal Allen relations [7]. Also, the set of time points is totally ordered by the relation precedes [1, T1–T4], and the temporal extent of an event (improperly) includes the temporal extent of all the (proper) parts of the event [1, T14]. [1, T5–T6] constrain the functions begin-point and end-point of an event. As FOL functions are total, they can be applied to TimePoints themselves. We address this issue by turning beginPoint and endPoint into functional relations (T5’), revisiting [1, T5–T14]. T1 ∀t:TimePoint(¬precedes(t,t)) T2 ∀t,t 0 :TimePoint(precedes(t,t 0 ) → ¬precedes(t 0 ,t)) T3 ∀t,t 0 ,t 00 :TimePoint((precedes(t,t 0 ) ∧ precedes(t 0 ,t 00 )) → precedes(t,t 00 )) T4 ∀t,t 0 :TimePoint((t 6= t 0 ) → (precedes(t,t 0 ) ∨ precedes(t 0 ,t))) 4 A strict partial order ≺ on the set of roles is called regular iff for any role name S and role R, then S≺R↔S− ≺R. A RIA ‘wvR’ is ≺-regular iff R is a role name, and (i) w=R◦R; or (ii) w=R− ; or (iii) w=S1 ◦ . . . ◦ Sn and Si ≺ R, for all 1 ≤ i ≤ n; or (iv) w=R ◦ S1 ◦ . . . ◦ Sn and Si ≺ R, for all 1 ≤ i ≤ n; or (v) w=S1 ◦ . . . ◦ Sn ◦ R and Si ≺ R, for all 1 ≤ i ≤ n. A set of RIAs is regular iff there exists a regular order ≺ s.t. each RIA in the set is ≺-regular. The ‘regularity’ syntactic rule ensures that the set of all RIAs in a TBox is regular. See [3, p. 58]. T5’ ∀e:Event∃!t,t 0 :TimePoint(beginPoint(e,t) ∧ endPoint(e,t 0 )) T6’ ∀e:Event,t,t 0 :TimePoint((beginPoint(e,t) ∧ endPoint(e,t 0 )) → precedes(t,t 0 )) T7’ ∀e, e0 :Event(before(e, e0 ) ↔ ∃t,t 0 :TimePoint(endPoint(e,t) ∧ beginPoint(e0 ,t 0 ) ∧ precedes(t,t 0 )) T8’ ∀e, e0 :Event(meets(e, e0 ) ↔ ∃t:TimePoint(endPoint(e,t) ∧ beginPoint(e0 ,t))) T9’ ∀e, e0 :Event(temporallyOverlaps(e, e0 ) ↔ ∃t0 , . . . ,t3 :TimePoint( beginPoint(e,t0 ) ∧ beginPoint(e0 ,t1 ) ∧ endPoint(e,t2 ) ∧ endPoint(e0 ,t3 ) ∧ precedes(t0 ,t1 ) ∧ precedes(t1 ,t2 ) ∧ precedes(t2 ,t3 ))) T10’ ∀e, e0 :Event(starts(e, e0 ) ↔ ∃t,t 0 ,t 00 :TimePoint(beginPoint(e,t) ∧ beginPoint(e0 ,t) ∧ endPoint(e,t 0 ) ∧ endPoint(e0 ,t 00 ) ∧ precedes(t 0 ,t 00 )) T11’ ∀e, e0 :Event(during(e, e0 ) ↔ ∃t0 , . . . ,t3 :TimePoint(beginPoint(e,t0 ) ∧ beginPoint(e0 ,t1 ) ∧ endPoint(e,t2 ) ∧ endPoint(e0 ,t3 ) ∧ precedes(t1 ,t0 ) ∧ precedes(t2 ,t3 ))) T12’ ∀e, e0 :Event(finishes(e, e0 ) ↔ ∃t,t 0 ,t 00 :TimePoint(beginPoint(e,t) ∧ beginPoint(e0 ,t 0 ) ∧ endPoint(e,t 00 ) ∧ endPoint(e0 ,t 00 ) ∧ precedes(t 0 ,t)) T13’ ∀e, e0 :Event(equals(e, e0 ) ↔ ∃t,t 0 :TimePoint(beginPoint(e,t) ∧ beginPoint(e0 ,t) ∧ endPoint(e,t 0 ) ∧ endPoint(e0 ,t 0 ))) T14’ ∀e, e0 :Event(hasPart(e, e0 ) → ((∃t:TimePoint(beginPoint(e,t) ∧ beginPoint(e0 ,t)) ∨ ∃t,t 0 :TimePoint(beginPoint(e,t) ∧ beginPoint(e0 ,t 0 ) ∧ precedes(t,t 0 ))) ∧ (∃t:TimePoint(endPoint(e,t) ∧ endPoint(e0 ,t)) ∨ ∃t,t 0 :TimePoint(endPoint(e,t) ∧ endPoint(e0 ,t 0 ) ∧ precedes(t 0 ,t))))) [8] discusses the impossibility of expressing the Allen’s time interval relations [7] in SROIQ. The best we can do is to provide partial axiomatizations of UFO-B’s temporal relations between events. [1, p. 331] informally defines the (co)domain of these relations as Event (a73)–(a86). On precedes, (T1), (T2) and (T3) are captured by (a87), (a88) and (a89), respectively. (a89) makes precedes non-simple, which forbids its use in (a87) and (a88). Totality (T4) seems inexpressible (we can only think of a solution using variables). (T5’) is guaranteed by (a53) and (a54). (T6’) is guaranteed by (a90), which makes precedes non-simple. As the right-side of a RIA can only have a role name, the necessary conditions of the Allen relations (T7’)–(T13’) seem inexpressible. The sufficient conditions for before (T7’) and meets (T8’) are captured by (a91) and (a92), respectively, and which make them non-simple. The sufficient conditions for temporallyOverlaps (T9’), starts (T10’), during (T11’), finishes (T12’), and equals (T13’), seem inexpressible, since they would require a disjunction of role compositions, see (f1)–(f5), respectively. Finally, (T14’) would break even more syntactic constraints, see (f6). a73 ∃before.>vEvent a77 ∃starts.>vEvent a81 ∃finishes.> v Event a74 >v∀before.Event a78 >v∀starts.Event a82 > v ∀finishes.Event a75 ∃meets.>vEvent a79 ∃during.>vEvent a83 ∃equals.> v Event a76 >v∀meets.Event a80 >v∀during.Event a84 > v ∀equals.Event a85 ∃temporallyOverlaps.> v Event a87 TimePointv¬(∃precedes.Sel f ) (T1) a86 > v ∀temporallyOverlaps.Event a88 Dis(precedes, precedes− ) (T2) a89 Tra(precedes) (T3) a90 beginPoint− ◦ endPoint v precedes (T6’) a91 endPoint ◦ precedes ◦ beginPoint− v before (T7’)+ a92 endPoint ◦ beginPoint− v meets (T8’)+ f1 (beginPoint ◦ precedes ◦ beginPoint− ) u (endPoint ◦ precedes− ◦ beginPoint− ) u (endPoint ◦ precedes ◦ endPoint− ) v temporallyOverlaps (T9’)+ f2 (beginPoint◦beginPoint− )u(endPoint◦precedes◦endPoint− ) v starts (T10’)+ f3 (beginPoint ◦ precedes− ◦ beginPoint− ) u (endPoint ◦ precedes ◦ endPoint− ) v during (T11’)+ f4 (endPoint ◦ endPoint− ) u (beginPoint ◦ precedes− ◦ beginPoint− ) v finishes (T12’)+ f5 (beginPoint ◦ beginPoint− ) u (endPoint ◦ endPoint− ) v equals (T13’)+ f6 hasPartv(((beginPoint◦beginPoint− )t(beginPoint◦precedes◦beginPoint− )) u ((endPoint ◦ endPoint− ) t (endPoint ◦ precedes− ◦ endPoint− ))) (T14’) 2.5. World Changes and Situations: (S1’)–(S7) Any event is triggered by/bringsAbout a unique situation (S3)/(S4). If a situation trig- gers an event, the situation obtainsIn the same TimePoint that is the beginPoint of the event (S1’). 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 e0 “by means of” a situation that was brought about by (the inverse of bringsAbout) e and that triggers e0 (S6). On (S7), causes should be the transitive closure of directlyCauses, what is inexpressible in FOL. S1’ ∀s:Situation, e:Event(triggers(s, e) → ∃t:TimePoint(obtainsIn(s,t) ∧ beginPoint(e,t)) S2’ ∀s:Situation, e:Event(bringsAbout(e, s) → ∃t:TimePoint(obtainsIn(s,t) ∧ endPoint(e,t)) S3 ∀e:Event(∃!s:Situation(triggers(s, e))) S4 ∀e:Event(∃!s:Situation(bringsAbout(e, s))) S5 ∀s:Situation(Fact(s) ↔ ∃t:TimePoint(obtainsIn(s,t))) S6 ∀e, e0 :Event(directlyCauses(e, e0 ) ↔ ∃s:Situation(bringsAbout(e, s) ∧ triggers(s, e0 ))) S7 ∀e, e0 :Event(causes(e, e00 ) ↔ (directlyCauses(e, e00 ) ∨ ∃e0 :Event(causes(e, e0 ) ∧ causes(e0 , e00 )))) (S1’) and (S2’) seem inexpressible in SROIQ, since the right-side of a RIA can only have a role name (see (f7), (f8)). (S3)/(S4) are guaranteed by (a59)/(a52), respectively. On (S5), the necessary condition for being a fact is captured by (a51), while the sufficient condition by (a93). On (S6), it is impossible to define a role as the composition of other roles. So, we capture the sufficient condition for directlyCauses in (a94) (making directlyCauses non-simple), but the necessary condition seems inexpressible. On (S7), only the sufficient conditions for causes seem expressible, as in (a11) and (a95) (making causes non-simple); similarly to (S1’), the necessary condition seem inexpressible. f7 triggersvobtainsIn ◦ beginPoint− f8 bringsAboutvbeginPoint◦obtainsIn− a93 Situation u (≥1obtainsIn.TimePoint) v Fact (S5)+ a94 bringsAbout ◦ triggers v directlyCauses (S6)+ a95 causes ◦ causes v causes (S7)+ 3. Well-formed SROIQ Theories Formalizing UFO-B Figure 2 shows a regular order ≺ on the set of roles and s.t. each RIA in T ={(a1)–(a95)} is ≺-regular, what shows that T is regular. However, T violates simplicity. So, we enu- merate subsets of T that are maximal w.r.t. simplicity, i.e., theories such that the inclusion of any other axiom makes them violate simplicity. In order to track the incompatibilities between axioms that lead to infringing simplicity, we build a simple meta-level theory in propositional logic. Assume the ‘operators’ I and S̄ as “proposition builders” in the sense that a proposition ‘I(i)’ means that the axiom (ai) is included in the TBox, and exclusivelyDependsOn− before before− mereologicallyOverlaps− meets− meets precedes precedes− mereologicallyOverlaps beginPoint beginPoint− endPoint endPoint− hasPart hasPart− causes causes− directlyCauses− directlyCauses exclusivelyDependsOn bringsAbout bringsAbout− triggers− triggers dependsOn dependsOn− activates activates− manifestedBy manifestedBy− inheresIn inheresIn− Figure 2. A strict partial order of roles that satisfy regularity for T = {(a1)–(a95)}. a proposition ‘S̄(r)’ means that the role r is non-simple. Since our set T is finite (95 axioms) and the set of role names is finite (16 role names) then the set of proposition symbols built by means of I and S̄ is also finite (111). By means of this meta-level theory, we define the problem of finding subsets of T that satisfy simplicity as a SAT problem. Firstly, we capture the reasons for non-simplicity: (1) Subsuming a role com- position: I(68)→S̄(mereologicallyOverlaps); I(69)→S̄(triggers); I(70)→S̄(de- pendsOn); I(90)→S̄(precedes); I(92)→S̄(causes). (2) ‘Tra’: I(65)→S̄(hasPart); I(89)→S̄(precedes). (3) Subsuming non-simple roles: (I(65)∧I(66))→S̄(mereolog- icallyOverlaps); (I(65)∧I(67))→S̄(mereologicallyOverlaps); (I(70)∧I(71))→ S̄(exclusivelyDependsOn); (I(11)∧I(94))→S̄(causes). Secondly, the axioms forbidden by the previous non-simple roles: S̄(triggers) → ¬I(59); S̄(dependsOn) → ¬I(49); S̄(hasPart) → (¬I(48) ∧ ¬I(63) ∧ ¬I(64)); S̄(ex- clusivelyDependsOn) → (¬I(55) ∧ ¬I(72)); S̄(precedes) → (¬I(87) ∧ ¬I(88)). Thirdly, the meta-axioms on the incompatibilities due to the simplicity rule: (i) I(65) → (¬I(48) ∧ ¬I(63) ∧ ¬I(64)), (ii) I(69) → ¬I(59), (iii) I(70) → ¬I(49), (iv) (I(70) ∧ I(71)) → (¬I(49) ∧ ¬I(55) ∧ ¬I(72)), (v) (I(89) ∨ I(90)) → (¬I(87) ∧ ¬I(88)). We translated (i)–(v) into 12 clauses in conjunctive normal form (CNF), more specifi- cally, the DIMACS format, and used the SAT solver CryptoMiniSat v5.0.0 in order to find all the models. From the 215 =32 768 possibilities, there are 3 969 models. However, we are only interested in the models that represent maximal TBoxes w.r.t. simplicity. These models are maximal w.r.t. truth, i.e., the change of any truth-value assignment from false to true invalidates the model. Using a script in the language R, we selected from the 3 969 models, the 24 that are maximal, leading to 24 UFO-B theories Ti , which are represented by means of auxiliary sets of indexes T̄i such that Ti = T \ {(a j)| j ∈ T̄i }. T̄0 = {48, 63, 64, 69, 70, 89, 90} T̄12 = {48, 63, 64, 69, 70, 87, 88} T̄1 = {48, 49, 55, 59, 63, 64, 72, 89, 90} T̄13 = {48, 49, 63, 64, 69, 71, 89, 90} T̄2 = {48, 49, 59, 63, 64, 71, 89, 90} T̄14 = {65, 69, 70, 89, 90} T̄3 = {48, 59, 63, 64, 70, 89, 90} T̄15 = {48, 59, 63, 64, 70, 87, 88} T̄4 = {59, 65, 70, 89, 90} T̄16 = {49, 55, 59, 65, 72, 87, 88} T̄5 = {49, 55, 65, 69, 72, 87, 88} T̄17 = {49, 59, 65, 71, 87, 88} T̄6 = {49, 65, 69, 71, 87, 88} T̄18 = {49, 65, 69, 71, 89, 90} T̄7 = {49, 55, 65, 69, 72, 89, 90} T̄19 = {49, 59, 65, 71, 89, 90} T̄8 = {48, 49, 55, 59, 63, 64, 72, 87, 88} T̄20 = {65, 69, 70, 87, 88} T̄9 = {48, 49, 55, 63, 64, 69, 72, 87, 88} T̄21 = {59, 65, 70, 87, 88} T̄10 = {48, 49, 59, 63, 64, 71, 87, 88} T̄22 = {49, 55, 59, 65, 72, 89, 90} T̄11 = {48, 49, 63, 64, 69, 71, 87, 88} T̄23 = {48, 49, 55, 63, 64, 69, 72, 89, 90} In order to empirically evaluate the Ti s, we translated each Ti into a TBoxi in OWL 2 DL. We assessed the consistency of each of these TBoxes by means of models generated by the Alloy Analyzer tool for a new Alloy codification that exactly corresponds to the FOL axioms shown in Section 2. Some of these models are “fully-consistent,” i.e., they have at least one instance for each class or relation. We generated 6 models by the Alloy Analyzer: 3 models enforcing full-consistency, having a minimum scope-size of 9 and a maximum, due to memory constraints, of 28; the other 3 models do not enforce full-consistency, having a model of scope-size 1, and a maximum scope-size of 29, due again to memory constraints. Each model was transformed into an individual assertion box (ABox) and joined to each TBoxi to form an OWL 2 DL knowledge base (KB). In total, this process produced 24×6=144 KBs. We used the DL reasoner Pellet version 2.4.0 to test the consistency of these KBs, all of which are consistent. Finally, the interested reader can find our DIMACS file, the SAT solutions, the R script, our Alloy codification of UFO-B, the generated Alloy models, the OWL 2 DL TBoxes, and the KBs at https://osf.io/jas8m. 4. 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 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. As a future work, we intend to (1) perform an ontological analysis of the 24 theories. (2) complement UFO-B with a fuller presentation and philosophical justification of sub-theories dealing with: (i) the differentiation of roles played by objects w.r.t. an event (the so-called processual roles); (ii) event qualities and quality structures; (iii) events of creation, destruction and modification of objects. (3) investigate alternative DL mappings for the UFO theories presented here dealing with different aspects of the trade-off between expressivity and tractability. Acknowledgments The first two authors were supported by the grants 71024352 and 71047522 of the “edital FAPES/CAPES n. 009/2014.” The third author was supported by the OCEAN Project (FUB) and by the CNPq grant #312158/2015-7. References [1] G. Guizzardi, G. Wagner, R. de Almeida Falbo, R. S. S. Guizzardi, and J. P. A. Almeida, “Towards onto- logical foundations for the conceptual modeling of events,” in Conceptual Modeling - 32th International Conference, ER 2013, Hong-Kong, China, November 11-13, 2013. Proceedings (W. Ng, V. C. Storey, and J. Trujillo, eds.), vol. 8217 of Lecture Notes in Computer Science, pp. 327–341, Springer, 2013. [2] D. Jackson, Software Abstractions: logic, language, and analysis. MIT press, 2012. [3] I. Horrocks, O. Kutz, and U. Sattler, “The even more irresistible SROIQ.,” Kr, vol. 6, pp. 57–67, 2006. [4] W3C, OWL 2 Web Ontology Language Document Overview, second edition ed., Dec. 2012. [5] G. Guizzardi, Ontological foundations for structural conceptual models. phdthesis, University of Twente, Enschede, The Netherlands, Enschede, Oct. 2005. [6] R. Casati and A. C. Varzi, Parts and places: The structures of spatial representation. MIT Press, 1999. [7] J. F. Allen, “Maintaining knowledge about temporal intervals,” Communications of the ACM, vol. 26, no. 11, pp. 832–843, 1983. [8] S. Batsakis, E. Petrakis, I. Tachmazidis, and G. Antoniou, “Temporal representation and reasoning in OWL 2,” Semantic Web, vol. 8, pp. 981–1000, Aug. 2017.