Representing the UFO-B Foundational Ontology of Events in S ROI Q

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 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 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) S ROIQ [ 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 S ROIQ, discussing the challenges in mapping these two formalisms and arguing that representing the totality of UFO-B in S ROIQ 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 S ROIQ, 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 S ROIQ First, we present some notational conventions: (i) FOL predicates and DL concepts/roles are denoted in Uppercase typewriter type; (ii) we employ restricted quantification a` la Frege, i.e., “8x:T (j )” is a schema for “8x(T (x) ! j ),” and “9x:T (j )” for “9x(T (x) ^ j ));” 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’. f/dsuirbescettlsyCcaauusseessg /causes

* * Event 2..* * * * * hasPart Individual fdisjointg

Situation * activates * Disposition 1

1 1 1 1..* obtainsIn Fact 1..* obtainsIn

Endurant /exclusivelyDependsOn

fdisjointg 1 1 * Trope 1..*inheresIn 1 Object /participationOf * /Participation

1 dependsOn * fdisjoint,completeg * matrnigifgeesrtesdBy * AtomicEvent ComplexEvent triggers *

bringsAbout 0..1 1 JbeginPoint 1 TimePoint 1 JendPoint

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 2In 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 ]) inheresIn 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 Disposition 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 a12 9inheresIn:> v Trope a13 9hasPart:> v ComplexEvent a14 9dependsOn:> v AtomicEvent a15 9obtainsIn:> v Situation a16 9triggers:> v Situation a17 9bringsAbout:> v Event Codomain Constraints a26 > v 8inheresIn:Object a27 > v 8hasPart:Event a28 > v 8dependsOn:Object a29 > v 8obtainsIn:TimePoint a30 > v 8triggers:Event a31 > v 8bringsAbout:Situation a40 (TimePoint u Individual) v ? a41 (Endurant u Event) v ?

Disjointness Completeness

a18 9causes:> v Event a19 9directlyCauses:> v Event a20 9activates:> v Situation a21 9manifestedBy:> v Disposition a22 9beginPoint:> v Event a23 9endPoint:> v Event a24 9exclusivelyDependsOn:>vParticipation a25 9participationOf:> v Participation a32 > v 8causes:Event a33 > v 8directlyCauses:Event a34 > v 8activates:Disposition a35 > v 8manifestedBy:AtomicEvent a36 > v 8beginPoint:TimePoint a37 > v 8endPoint:TimePoint a38 > v 8exclusivelyDependsOn:Object a39 > v 8participationOf:Object a42 (Object u Trope) v ? a43 (Object u Situation) v ? a44 (Trope u Situation) v ? a45 (AtomicEvent u ComplexEvent) v ? 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 mereologicallyOverlaps 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 8e:Event(AtomicEvent(e) $ :9e0:Event(hasPart(e; e0))) M2 8e:Event(ComplexEvent(e) $ :AtomicEvent(e)) M3 8e:ComplexEvent(:hasPart(e; e)) M4 8e; e0:ComplexEvent(hasPart(e; e0) ! :hasPart(e0; e)) M5 8e; e0:ComplexEvent; e00:Event((hasPart(e; e0) ^ hasPart(e0; e00)) ! hasPart(e; e00)) M6 8e:ComplexEvent; e0:Event(hasPart(e; e0) ! 9e00:Event(hasPart(e; e00) ^ :mereologicallyOverlaps(e0; e00))) M7 8e; e0:ComplexEvent(Overlaps(e; e0) $ (hasPart(e; e0) _ hasPart(e0; e) _ 9e00:Event(hasPart(e; e00) ^ hasPart(e0; e00)))) M8 8e; e0:ComplexEvent((8e00:Event(hasPart(e; e00) ! hasPart(e0; e00))) ! (e = e0 _ hasPart(e0; e))) M9 8e; e0:ComplexEvent(e = e0 $ 8e00: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).

3Let 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 t s.t. 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 ‘9R: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 mereologicallyOverlaps non-simple by (a66) or (a67). (M6) seems inexpressible even by assuming a definition of mereologicallyOverlaps, e.g., “Ref(hasAtLeastTwoDisjointParts)” with the ill-formed formula “hasAtLeastTwoDisjointParts hasPart 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, notMereologicallyOverlap is inexpressible, e.g., even by removing the axioms that make mereologicallyOverlaps non-simple and asserting “Dis(mereologicallyOverlaps,notMereologicallyOverlap),” SROIQ could not express that one relation would be the set-complement of the other, i.e., the ill-formed formula “Uv mereologicallyOverlaps 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 :9hasPart:Event a62 Event u :9hasPart:Event v AtomicEvent a63 ComplexEvent v :(9hasPart:Sel f ) a64 Dis(hasPart; hasPart ) a65 Tra(hasPart) a66 hasPart v mereologicallyOverlaps a67 hasPart v mereologicallyOverlaps a68 hasPart hasPart v mereologicallyOverlaps (M1)− (M1)+ (M3) (M4) (M5) (M7)+ (M7)+ (M7)+ (D3)+ (D4) Objects participate not only in the atomic events that are manifestations of their dispositions, but also in the complex events that have such manifestations as parts; e.g., Caesar

2.2. Events as Manifestations of Object Dispositions: (D1)–(D4)

Atomic events are manifestations of (the inverse of manifestedBy) unique object dispositions (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 8d:Disposition(9!o:Object(inheresIn(d; o))) D2 8e:AtomicEvent(9!d:Disposition(manifestedBy(d; e))) D3 8s:Situation; e:AtomicEvent(triggers(s; e) $ 9d:Disposition(activates(s; d) ^ manifestedBy(d; e))) D4 8d: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 a70 manifestedBy inheresIn v dependsOn 2.3. On the Participation of Objects in Events: (P1)–(P5) 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). exclusivelyDependsOn 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 participations to objects can be defined by means of exclusivelyDependsOn (P5).

P1 8e:AtomicEvent 9!o:Object(dependsOn(e; o)) P2 8e:AtomicEvent; o:Object(exclusivelyDependsOn(e; o) $ dependsOn(e; o)) P3 8e:ComplexEvent; o:Object(exclusivelyDependsOn(e; o) $

8e0:Event(hasPart(e; e0) ! exclusivelyDependsOn(e; o))) P4 8e:Event(Participation(e) $ 9!o:Object(exclusivelyDependsOn(e; o))) P5 8o: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 participation, while (a72) entails the sufficient condition. On (P5), since both relations participationOf 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 a72 Event u (=1exclusivelyDependsOn:Object) v Participation (P2)− (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 8t:TimePoint(:precedes(t;t)) T2 8t;t0:TimePoint(precedes(t;t0) ! :precedes(t0;t)) T3 8t;t0;t00:TimePoint((precedes(t;t0) ^ precedes(t0;t00)) ! precedes(t;t00)) T4 8t;t0:TimePoint((t 6= t0) ! (precedes(t;t0) _ precedes(t0;t))) 4A 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’ 8e:Event9!t;t0:TimePoint(beginPoint(e;t) ^ endPoint(e;t0)) T6’ 8e:Event;t;t0:TimePoint((beginPoint(e;t) ^ endPoint(e;t0)) ! precedes(t;t0)) T7’ 8e; e0:Event(before(e; e0) $ 9t;t0:TimePoint(endPoint(e;t) ^ beginPoint(e0;t0) ^ precedes(t;t0)) T8’ 8e; e0:Event(meets(e; e0) $ 9t:TimePoint(endPoint(e;t) ^ beginPoint(e0;t))) T9’ 8e; e0:Event(temporallyOverlaps(e; e0) $ 9t0; : : : ;t3:TimePoint( beginPoint(e;t0) ^ beginPoint(e0;t1) ^ endPoint(e;t2) ^ endPoint(e0;t3) ^ precedes(t0;t1) ^ precedes(t1;t2) ^ precedes(t2;t3))) T10’ 8e; e0:Event(starts(e; e0) $ 9t;t0;t00:TimePoint(beginPoint(e;t) ^

beginPoint(e0;t) ^ endPoint(e;t0) ^ endPoint(e0;t00) ^ precedes(t0;t00)) T11’ 8e; e0:Event(during(e; e0) $ 9t0; : : : ;t3:TimePoint(beginPoint(e;t0) ^ beginPoint(e0;t1) ^ endPoint(e;t2) ^ endPoint(e0;t3) ^ precedes(t1;t0) ^ precedes(t2;t3))) T12’ 8e; e0:Event(finishes(e; e0) $ 9t;t0;t00:TimePoint(beginPoint(e;t) ^ beginPoint(e0;t0) ^ endPoint(e;t00) ^ endPoint(e0;t00) ^ precedes(t0;t)) T13’ 8e; e0:Event(equals(e; e0) $ 9t;t0:TimePoint(beginPoint(e;t) ^ beginPoint(e0;t) ^ endPoint(e;t0) ^ endPoint(e0;t0))) T14’ 8e; e0:Event(hasPart(e; e0) ! ((9t:TimePoint(beginPoint(e;t) ^ beginPoint(e0;t)) _ 9t;t0:TimePoint(beginPoint(e;t) ^ beginPoint(e0;t0) ^ precedes(t;t0))) ^ (9t:TimePoint(endPoint(e;t) ^ endPoint(e0;t)) _ 9t;t0:TimePoint(endPoint(e;t) ^ endPoint(e0;t0) ^ precedes(t0;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 9before:>vEvent a77 9starts:>vEvent a81 9finishes:> v Event a74 >v8before:Event a78 >v8starts:Event a82 > v 8finishes:Event a75 9meets:>vEvent a79 9during:>vEvent a83 9equals:> v Event a76 >v8meets:Event a80 >v8during:Event a84 > v 8equals:Event a85 9temporallyOverlaps:> v Event a87 TimePointv:(9precedes:Sel f ) (T1) a86 > v 8temporallyOverlaps: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 triggers 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’ 8s:Situation; e:Event(triggers(s; e) ! 9t:TimePoint(obtainsIn(s;t) ^ beginPoint(e;t)) S2’ 8s:Situation; e:Event(bringsAbout(e; s) ! 9t:TimePoint(obtainsIn(s;t) ^ endPoint(e;t)) S3 8e:Event(9!s:Situation(triggers(s; e))) S4 8e:Event(9!s:Situation(bringsAbout(e; s))) S5 8s:Situation(Fact(s) $ 9t:TimePoint(obtainsIn(s;t))) S6 8e; e0:Event(directlyCauses(e; e0) $ 9s:Situation(bringsAbout(e; s) ^ triggers(s; e0))) S7 8e; e0:Event(causes(e; e00) $ (directlyCauses(e; e00) _ 9e0: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 =f(a1)–(a95)g is -regular, what shows that T is regular. However, T violates simplicity. So, we enumerate 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 meets meets

before before precedes precedes

mereologicallyOverlaps mereologicallyOverlaps beginPoint beginPoint

causes causes directlyCauses directlyCauses bringsAbout bringsAbout triggers endPoint endPoint hasPart

hasPart triggers exclusivelyDependsOn dependsOn dependsOn activates activates manifestedBy manifestedBy inheresIn inheresIn 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 composition: I(68)!S¯ (mereologicallyOverlaps); I(69)!S¯ (triggers); I(70)!S¯ (dependsOn); 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¯ (mereologicallyOverlaps); (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¯ (exclusivelyDependsOn) ! (: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 specifically, 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 n f(a j)j j 2 T¯ig. T¯0 = f48; 63; 64; 69; 70; 89; 90g T¯1 = f48; 49; 55; 59; 63; 64; 72; 89; 90g T¯2 = f48; 49; 59; 63; 64; 71; 89; 90g T¯3 = f48; 59; 63; 64; 70; 89; 90g T¯4 = f59; 65; 70; 89; 90g T¯5 = f49; 55; 65; 69; 72; 87; 88g T¯6 = f49; 65; 69; 71; 87; 88g T¯7 = f49; 55; 65; 69; 72; 89; 90g T¯8 = f48; 49; 55; 59; 63; 64; 72; 87; 88g T¯9 = f48; 49; 55; 63; 64; 69; 72; 87; 88g ¯ T10 = f48; 49; 59; 63; 64; 71; 87; 88g ¯ T11 = f48; 49; 63; 64; 69; 71; 87; 88g

T¯12 = f48; 63; 64; 69; 70; 87; 88g ¯ T13 = f48; 49; 63; 64; 69; 71; 89; 90g ¯ T14 = f65; 69; 70; 89; 90g ¯ T15 = f48; 59; 63; 64; 70; 87; 88g ¯ T16 = f49; 55; 59; 65; 72; 87; 88g ¯ T17 = f49; 59; 65; 71; 87; 88g ¯ T18 = f49; 65; 69; 71; 89; 90g ¯ T19 = f49; 59; 65; 71; 89; 90g ¯ T20 = f65; 69; 70; 87; 88g ¯ T21 = f59; 65; 70; 87; 88g ¯ T22 = f49; 55; 59; 65; 72; 89; 90g ¯

T23 = f48; 49; 55; 63; 64; 69; 72; 89; 90g

In order to empirically evaluate the Tis, 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 ontological 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 .