Towards a Unified Theory of Endurants and Perdurants: UFO-AB Alessander BOTTI BENEVIDES a,1 , João Paulo A. ALMEIDA a and Giancarlo GUIZZARDI 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. The Unified Foundational Ontology (UFO-A) is a foundational ontol- ogy about endurants that has been built as a foundation for conceptual modeling, and which focuses on static aspects of endurants. In addition to UFO-A, we have the Unified Foundational Ontology–Part B (UFO-B), a formal theory dealing with the interplay between endurants and the dynamic aspects of reality (e.g., events, processes, causation, dispositions, situations). Given the objective of characterizing this interplay between endurants and perdurants, these two ontologies are meant to form an integral whole. However, currently, they diverge in the way they approach modality. While UFO-A uses a general notion of alethic modality without com- mitting to any notion of time, UFO-B is centered around temporal aspects. As an attempt to address this issue, we here define a translation of the axioms of UFO-A to FOL, and revisit an excerpt of UFO-B in order to accommodate a partial order of time points. With the goal of producing a unified theory, we interpret the alethic modalities of necessity and contingency of UFO-A in terms of this temporal struc- ture, paying a special attention to the interplay between the determinism of a causal nexus and the existence of counterfactual situations. The revisited UFO-B is called UFO-B? and the unified theory is called UFO-AB. Keywords. alethic modality, endurant, event, foundational ontology, FOL, QS5 1. Introduction The Unified Foundational Ontology (UFO-A) [8] is an ontology of endurants that was built with the purpose of serving as a foundation for structural conceptual modeling lan- guages. As such, it focuses on static aspects of endurants, including many of their modal aspects. However, this ontology makes no commitment with respect to a particular view of temporal modality. In the Unified Foundational Ontology–Part B (UFO-B) [13,2], in contrast, temporal aspects are fundamental. UFO-B extends UFO-A with a foundational ontology of events, defining a formal theory on the interplay between objects, events, 1 Corresponding Author: Alessander Botti Benevides, NEMO, Computer Science Department, Federal University of Espı́rito Santo, Av. Fernando Ferrari, 514 - Goiabeiras/Vitória, Brazil; E-mail: abbenevides@inf.ufes.br. Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). situations, time points, dispositions, processual roles, and the causal nexus. The focus of UFO-B is to provide ontological foundations for behavioral conceptual modeling, in- cluding for process and project modeling [12,9], situation modeling [1], and discrete event simulation [11]. Regarding their formalizations, UFO-A is expressed in a quantified modal logic (QML) [7] that allows the expression of the alethic modalities of truth (viz., necessity and contingency), and UFO-B is defined in first-order logic (FOL) with the Method of Temporal Arguments (MTA) [26]. In order to enable UFO-A and UFO-B to ground con- ceptual modeling languages that allow the modeling of both endurants and events, i.e., both static and behavioral aspects of a domain, it is necessary to build a unified formal- ism for UFO-A and UFO-B. For this task, one move is to interpret the alethic modalities of necessity and contingency in a temporal structure, as done in [3], where the alethic modalities used in UFO-A were interpreted in a branching-time temporal structure. Differently, [5] interpreted necessity/contingency as immutability/mutability in lin- ear time, which is unable to represent counterfactuals. For instance, while the sentence “John is necessarily a person” can be interpreted in linear time as (i) “John is a person” and (ii) “John was always a person” and (iii) “John will always be a person,” (i)–(iii) do not capture (iv) that “John could not cease to be a person,” i.e., it is not accidental that John is always a person; being a person is an essential property of John. Therefore, just interpreting the alethic modalities used in UFO-A into the linear time structure suggested by the current available full formalization of UFO-B (in FOL) will not work; one has to also revisit the axioms of UFO-B, e.g., by representing the di- chotomy “actual versus counterfactual” in a partial order of time points (a.k.a. branching- time) as done in [3]. However, one has to deal with the determinism of the causal nexus together with counterfactual situations. In this paper, we define a method for rewriting UFO-A in FOL, with no loss of content, and consistently with a revisited UFO-B. This paper is structured as follows. Section 2 briefly reviews the notions of alethic and temporal modalities, and their relevance for conceptual modeling and knowledge representation. In Section 3, we show a set of translation rules for transforming the UFO-A QML axioms to FOL. Section 4 adapts UFO-B for a partial order of time points. In Section 5, we present our final considerations. 2. Alethic and Temporal Modalities Let us first define some notational conventions: (i) free variables are implicitly univer- sally quantified; (ii) unary predicates are noted in upper camel case typewriter type, e.g., “LivingPerson;” (iii) other predicates and constants are noted in lower camel case typewriter type, e.g., “motherOf” and “johnLocke;” (iv) definitions (introduced by “,”) “are to be viewed as extraneous conventions of notational abbreviation” [24, p. 72] and are written following the previous cases, but with an italic style, e.g., “Thing ;” and (v) the symbols “ p ” and “ q ” denote quasi-quotation. The alethic modalities of truth distinguish between necessary and contingent truths. Intuitively, a necessary truth is a truth that could not be otherwise, while a contingent truth could be false; or the negation of a necessary truth is contradictory, while the nega- tion of a possible truth is consistent; or a necessary truth is true in all possible worlds, while a possible truth is true in at least one world [14, Ch. 10]. The original specification of UFO-A in [8] uses QML semantically restricted to uni- versal Kripke frames, e.g., in the definition of rigidity, non-rigidity and anti-rigidity [8, pp. 101–102]. This means that pϕq (i.e., pnecessarily ϕq) is true if and only if (iff) ϕ is true in all worlds, and p♦ϕq (i.e., ppossibly ϕq) is true iff ϕ is true in at least one world. Quantified S5 (QS5) is a modal logic that is sound and strongly complete for the class of universal Kripke frames [4, p. 340, Problem 27.2]. This logic was the choice in later pre- sentations of (excerpts of) UFO-A ([23,10]), where there is also an explicit commitment to the Barcan formula and its converse, embracing possibilistic quantification [7, § 4.9]. Semantically, possibilistic quantification determines a fixed domain of entities for every possible world, which is traditionally associated to the view that the domain includes all the possibilia. In this view, it is possible to make a distinction between existence and presence (at a world). Syntactically, the constants, function applications and variables are terms, things that can be predicated upon and that denote entities from the domain of discourse, the set of existents. Therefore, semantically, the set of existent things is the domain of quantification of the theory. This view agrees with Quine’s dictum that “to be is to be the value of a variable” [25, p. 15]. More specifically, “a theory is committed to those and only those entities to which the bound variables of the theory must be capable of referring in order that the affirmations made in the theory be true” [25, pp. 13–14]. While anything in the domain of quantification of our theory exists, only some en- tities are presentAt a specific world (in other words, are actual at a world). Our unary predicate ppresentAt(x)q is a renaming of what Fitting et al. [7] call pε(x)q, denoting existence in a world. They show how pε(x)q can be used to transform formulae from the varying domain semantics to constant domain semantics [7, p. 106, Definition 4.8.1].2 In a sense, in a possibilistic modal theory, a world w “collects” formulae that are true in w. For us, the terms being predicated upon within these formulae must be presentAt w. The idea is that ppresentAt(t)q being true at w allows t to be mentioned in formulae that are true in w. For this reason, we add to the original axioms of UFO-A the axiom schema (u1), requiring, for each predicate P of arity n in the set P of predicates of the theory, that whenever a P-predication is true, the arguments of the predication are present. ! Pn (xi , . . . , x j ) → presentAt(xk ) , where Pn ∈ P. V u1  k∈{xi ,...,x j } Worlds can be seen as TimePoints, the accessibility relation being temporal prece- dence (e.g., a linear order or a partial order). In this case, necessity can be interpreted as immutability and contingency as possibility within a history.3 For instance, the modal logic KL is sound for the class of finite strict partial orders. Now, let us assume the causal nexus to be deterministic. Then, a causal chain cannot have bifurcations; each causal chain “happens” over a single history, even if we assume a partial order of time points, like in KL. As an example, an analysis of (f1) shows that it requires a TimePoint (world) in which john is a Student, and a TimePoint in which john is not a Student. This is not a problem, since a person can start or cease to be a student in her lifetime (within a single causal chain). Concerning (f2), since BrazilianBorn is an immutable 2 UFO-A also uses pε(x)q in [8, p. 164], but in [23, p. 4], the authors reify times and adopt a temporalized predicate pex(x,t)q for existence in worlds at a specific time. 3 A history/branch is a maximal path, i.e., a maximal chain of TimePoints within the accessibility relation. (f3) and innate (f4) property, john cannot cease to be BrazilianBorn within a history. The only way (f2) can be satisfied is by means of two independent causal chains,4 one in which john is always BrazilianBorn and other in which he never is. f1 ♦(Student(x)) → ♦(¬Student(x)) f2 ♦(BrazilianBorn(x)) → ♦(¬BrazilianBorn(x)) f3 BrazilianBorn(x) → (BrazilianBorn(x)) f4 ¬BrazilianBorn(x) → (¬BrazilianBorn(x)) Types (universals) are reified in both UFO-A and UFO-B. In UFO-A, the predicate “ :: ” represents instantiation (see [8, p. 162], [23, p. 3]), while in UFO-B it is represented by “instantiates” [2]. That said, properties like Student and BrazilianBorn are called anti-rigid and can be captured in QS5 by (u2), where rigidity is defined in QS5 by (u3). In QKL, (u2) and (u3) define immutability and mutability, respectively. u2 AntiRigid(p) , x :: p → ♦(¬(x :: p)) u3 Rigid(p) , x :: p → (presentAt(x) → x :: p) 3. Capturing the Alethic Modality of UFO-A in FOL While in Section 2 we discussed modal notions, our aim is to build a FOL theory. Here, we show a method for translating a QS5 theory (like UFO-A) to FOL. Let T be a QS5 theory with a countably infinite set of variables {x0 , . . . , xλ −1 , xλ , . . .}. In practice, the theory T only uses variables in {x0 , . . . , xλ −1 }, where λ −1 is the biggest index (a natural number) of variables used in axioms. This means that the variable xλ is never used in T . By reifying worlds in the domain of quantification by means of the variable xλ , it is possible to rewrite the axioms of T into a FOL theory T . We define a set of translation rules in A = {(r1), . . . , (r5)}. Predicates can be rewritten with an additional argument, as in (r1). The translation rules (r2)–(r5) define the recursive steps. S5 has the nice property that every well-formed formula (wff) is equivalent to a wff with modal depth ≤ 1, i.e., a wff in which no modal operator falls in the scope of another modal operator (see [4, p. 340, Problem 27.3]). There is an algorithm (that always halts) for finding such a wff, and we denote its application to a wff ϕ as ϕ̊. This allows us to use only one variable, xλ , to quantify over worlds in the translation rule (r5). r1 Pn (xi , . . . , x j ) , Pn+1 (xi , . . . , x j , xλ ), where Pn ∈ P and n is the arity of P. r2 ¬ϕ , ¬ϕ r3 ϕ ∧ α , ϕ ∧ α r4 ∀xi (ϕ) , ∀xi (ϕ) r5 ϕ , ∀xλ (ϕ̊) 4. A Revisited Excerpt of UFO-B Here, we revisit an excerpt of UFO-B (a FOL theory) in order to accommodate a par- tial order of time points. Except for the Allen relations, which require a branching-time counterpart (see [15]), the rest of UFO-B is unaffected by the work presented here. 4 By independent, we mean that the causal chains share no TimePoint. 4.1. Time While UFO-B [13,2] suggests a discrete linear ordering of TimePoints, here we adopt a discrete strict partial order “precedes” over TimePoints (t1). Therefore, precedes is irreflexive (t2), transitive (t3) and asymmetric (a theorem). A TimePoint can be an immediateSucessorOf another TimePoint (t4). (t5) defines when two TimePoints can be seen as an interval, a part of a history.5 (t6) defines when two TimePoints are comparable. (t7) defines when one interval is a subIntervalOf of another interval. (t8) provides a predicate sameLength for comparing the length of two intervals. t1 precedes(x, y) → TimePoint(x) ∧ TimePoint(y) t2 ¬precedes(x, x) t3 precedes(x, y) ∧ precedes(y, z) → precedes(x, z) t4 immediateSucessorOf(x, y) , precedes(y, x) ∧ ¬∃z(precedes(z, x) ∧ precedes(y, z)) t5 interval(x, y) , x = y ∨ precedes(x, y) t6 comparable(x, y) , interval(x, y) ∨ precedes(y, x) t7 subIntervalOf(xb , xe , yb , ye ) , interval(xb , xe ) ∧ interval(yb , ye ) ∧ ((xb = yb ∨ precedes(yb , xb )) ∧ (xe = ye ∨ precedes(xe , ye )) t8 sameLength(xb , xe , yb , ye ) ↔ interval(xb , xe ) ∧ interval(yb , ye ) ∧ ((xb = xe ∧ yb = ye ) ∨ ∃z, z0 (immediateSucessorOf(z, xb ) ∧ immediateSucessorOf(z0 , yb ) ∧ sameLength(z, xe , z0 , ye ))) Moreover, a branching after a TimePoint t must be justified: there must be a differ- ence between the set of things that are presentAt t 0 and the ones presentAt t 00 . More specifically, there must be (i) an event with beginPoint or endPoint in t 0 but not in t 00 , or (ii) a situation that obtainsIn t 0 but not in t 00 (t9). Notice that (i) includes the case of an object being created or terminated (by an event with endPoint) in t 0 but not in t 00 . Finally, only entities other than TimePoints can be presentAt TimePoints (t10), and, for ontological parsimony, there is at least one entity present at a TimePoint (t11). t9 t 0 6= t 00 ∧ immediateSucessorOf(t 0 ,t) ∧ immediateSucessorOf(t 00 ,t) → ∃x((beginPoint(x,t 0 ) ∧ ¬beginPoint(x,t 00 )) ∨ (endPoint(x,t 0 ) ∧ ¬endPoint(x,t 00 )) ∨ (obtainsIn(x,t 0 ) ∧ ¬obtainsIn(x,t 00 ))) t10 presentAt(x, y) → ¬TimePoint(x) ∧ TimePoint(y) t11 TimePoint(x) → ∃y(presentAt(y, x)) 4.2. Endurants Endurants (e.g., a cat, the Moon, Mick Jagger) are in time, in the sense that it is pos- sible to refer to john as a child and john as an adult as the same entity, which under- 5 Although we informally talk about histories, we do not reify them in our theory. We leave as future work investigating whether reifying histories would be of benefit. goes changes over time. For ontological parsimony, each Endurant is presentAt some TimePoint (e1). e1 Endurant(x) → ∃y(presentAt(x, y)) 4.3. Events Fallings cannot fall, deaths cannot die, changes cannot change. Although we do not commit to the notion of Events as changes (which is the main assumption of Lom- bard in [22]), we agree that non-relational changes are events. Events cannot undergo non-relational changes.6 Events happen in time. Since Lombard’s theory and ours share the view that Events have inter-world identity, i.e., an Event can occur over different histories, it is fruitful to compare his theory with ours. While for Lombard [20, p. 354],[17, p. 454] Events could have been different from what they were by having contingent temporal parts, i.e., a single Event could “aggre- gate” different occurrences,7 each of which sharing the same essential parts, but differ- ing in some contingent parts; in our theory, Events have no alethic modal properties. An Event could not have been different from what it was. Nonetheless, it makes sense to allow Events to have temporal branchings, occurring over incomparable TimePoints, but only for the special cases where the reason for the temporal branching is external to the Event, i.e., the Event happens the same way over the different histories. Therefore, Events may have not exactly one, but more than one beginPoints and endPoints (e2), (e3). Moreover, Events are non-instantaneous (e3), which is compatible with Lombard in [20, p. 348]. Events can only happen over different histories because it would not make sense to postulate the existence of two events in cases where it is impossible to distinguish the two occurrences based solely on their non-relational aspects.8 e2 beginPoint(e,t) ∨ endPoint(e,t) → (Event(e) ∧ TimePoint(t)) e3 Event(e) → ∃t,t 0 (beginPoint(e,t) ∧ endPoint(e,t 0 )) For Lombard in [21, p.283], Events cannot recur. We have a stronger position in that Events are nonintermittent, and that is why they cannot recur over a history, having at most one beginPoint in a history (e4). Moreover, Events must end, i.e., in each history in which the Event begins, it must end (e5). Similarly, Events must begin (e6). Finally, whenever an Event occurs over two histories, the two occurrences must have the same length (e7), which also agrees with Lombard’s view [18, p. 9, Footnote 11]. e4 t 6= t 0 ∧ comparable(t,t 0 ) ∧ beginPoint(e,t) → ¬beginPoint(e,t 0 ) e5 beginPoint(e,t) ∧ comparable(t,t 0 ) → ∃t 00 (comparable(t 0 ,t 00 ) ∧ endPoint(e,t 00 )) e6 endPoint(e,t) ∧ comparable(t,t 0 ) → ∃t 00 (comparable(t 0 ,t 00 ) ∧ beginPoint(e,t 00 )) e7 beginPoint(e, xb ) ∧ endPoint(e, xe ) ∧ interval(xb , xe ) ∧ beginPoint(e, yb ) ∧ endPoint(e, ye ) ∧ interval(yb , ye ) → sameLength(xb , xe , yb , ye ) 6 See [16] for (non-)relational changes. 7 Although we informally talk about occurrences of Events, we do not reify them in our theory. 8 Again, “non-relational” as in [16]. Moreover, we think that identity criteria should be based solely on intrinsic properties; e.g., we disagree with the causality-based identity criterion for Events proposed in [6]. 4.4. Situations A Situation is the truthmaker of a synchronic proposition. For instance, the proposition “John is awake now” is made true by a Situation such as thatJohnIsAwakeNow. This view is derived from logical atomism, but Situations differ from Russell’s facts and Wittgenstein’s states of affairs by being synchronic. In our view, reality-at-time-t is partitioned into atomic Situations, and starting from them, one can describe reality-at- time-t in a bottom-up manner by means of atomic synchronic propositions. Since the atomic synchronic propositions describing atomic Situations are the most fine-grained pieces of synchronic information one can get, such propositions should be logically independent. Since we are not reifying propositions, we pose this constraint on Situations: Given two concomitant atomic Situations, knowing the structure of one is insufficient for deriving the structure of the other (f5). f5 s 6= s0 ∧ concomitant(s, s0 ) ∧ instanceOf(s, S) 0 instanceOf(s0 , S0 ) However, capturing syntactic consequence (“`” and “0”) requires a reflection mech- anism, like Gödel functions, where wffs are reified as terms of the theory. Such a require- ment would deviate our attention into the technicalities of a theory of first-order arith- metic. Therefore, we will not formally capture the nature of Situations, but only their interplay with Endurants and Events. Since we are capturing the alethic modality by means of a partial order of time points, possible Situations must obtain (s1) in at least one TimePoint in a history that entertains such a possibility (s2). Moreover, Situa- tions should not re-obtain over a history (s3), they are bound to specific TimePoints.9 s1 obtainsIn(x, y) → (Situation(x) ∧ TimePoint(y)) s2 Situation(x) → ∃y(obtainsIn(x, y)) s3 t 6= t 0 ∧ comparable(t,t 0 ) ∧ obtainsIn(s,t) → ¬obtainsIn(s,t 0 ) Situations are similar to enablers in [19, §V], an obtaining Situation can be a necessary but not a sufficient condition for an Event to occur. Situations have no causal power, only Events do. An Event bringsAbout exactly one Situation (s4), (s5), which holds in all endPoints of the Event (s6). Also, an Event is triggered by exactly one Situation (s7),(s8), which holds in all beginPoints of the Event (s9). Usually, a Situation is considered a Fact (w.r.t. a history) iff the situation obtainsIn a TimePoint (of the history). Since we are not reifying histories, we define a Situation as a Fact w.r.t. a TimePoint t iff there is a t 0 comparable with t—so that t and t 0 are in a path of a history—and such that the Situation obtainsIn t 0 (s10). Finally, except for TimePoints with no preceding TimePoint, if a Situation s obtainsIn t, s must be brought about by an Event with endPoint at t (s11). s4 bringsAbout(e, s) → (Event(e) ∧ Situation(s)) s5 Event(e) → ∃!s(bringsAbout(e, s)) s6 bringsAbout(e, s) ∧ endPoint(e,t) → obtainsIn(s,t) s7 triggers(s, e) → (Situation(s) ∧ Event(e)) s8 Event(e) → ∃!s(triggers(s, e)) s9 triggers(s, e) ∧ obtainsIn(s,t) → beginPoint(e,t) 9 We have no strong objection against removing (s3), leaving such an analysis for future work. s10 Fact(s,t) , ∃t 0 (comparable(t,t 0 ) ∧ obtainsIn(s,t 0 )) s11 ∃t 0 (precedes(t 0 ,t)) ∧ obtainsIn(s,t) → ∃e(bringsAbout(e, s) ∧ endPoint(e,t)) 4.5. Time is a Set of Lines The so called essentiality thesis states that an Event must occur at the same TimePoints in all histories in which it occurs [18]. In [18, pp. 7–13], Lombard shows an argument against the inessentiality thesis, where he presupposes that determinism must be false for the inessentiality to make sense. Here, we show that one must not give up determinism in order to commit to the inessentiality thesis. As an example for the inessentiality thesis, let an event e start in a TimePoint ti in a history h that begins at t0 , and e also starts in a TimePoint ti0 in a history h0 that begins at t00 and s.t. the length of the interval [t0 ,ti ] is different from the length of [t00 ,ti0 ]. Determinism can still hold when h and h0 differ in the Situations that obtainsIn t0 and t00 . Moreover, determinism also holds with the inessentiality thesis when two histories have no beginning. Non-surprisingly, the notion of contingency that is lost due to the view of time as a line in [5] is “regained” by allowing the existence of independent time lines, which are able to entertain counterfactual truths. This means that precedes is not a strict total order because, while it is asymmetric and transitive, it is not semiconnexOver TimePoints (f6). We prove that precedes has a weaker property: transitivity of comparability (f7). f6 semiconnexOver[R, S] , (S(x) ∧ S(y) ∧ x 6= y) → (R(x, y) ∨ R(y, x)) f7 (comparable(x, y) ∧ comparable(y, z)) → comparable(x, z) More specifically, we prove that {(t1), . . . , (t11), (e1), . . . , (e7), (s1), . . . , (s11)} entails a temporal structure that is a set of lines. The proof goes as follows. Assume that there is a bifurcation at TimePoint t, which is immediately succeeded by both t 0 and t 00 . From (t9), there must be (i) an event with beginPoint or endPoint in t 0 but not in t 00 , or (ii) a situation that obtainsIn t 0 but not in t 00 . In case (i), if there is an event e with beginPoint in t 0 but not in t 00 , from {(s8), (s9)}, there is a situation that obtainsIn t 0 and triggers e, but that does not ob- tainsIn t 00 (otherwise, by (s9), e would also have a beginPoint at t 00 ). Then, (a) from (s11), since the situation obtainsIn t 0 , it must be brought about by an event e0 with endPoint in t 0 but not in t 00 (otherwise, by (s6), the situation would also obtain in t 00 ). Then, (b) from (e6), e0 must have a beginPoint in t or earlier. Since e0 started before or in t, it must end in both branches, i.e., not only in t 0 but also in all histories containing t 00 (e5). Moreover, from (e7), all the occurrences of e0 must have the same length. There- fore, e0 must have an endPoint at t 00 , a contradiction. On the other possibility, if there is an event with endPoint in t 0 but not in t 00 , then the proof goes as in (b). In case (ii), the proof goes as in (a). 4.6. Causality The Event john’sFall bringsAbout the Situation thatJohnIsHurt, which triggers the Event john’sCry. So, john’sFall directlyCauses john’sCry, as defined in (c1). The transitive closure of directlyCauses is a useful generalization, encompassing indirect causes. Since transitive closure is inexpressible in FOL, we have causes as a predicate (see (c2)), constraining it to be asymmetric (c3). c1 directlyCauses(e, e0 ) , ∃s(bringsAbout(e, s) ∧ triggers(s, e0 )) c2 causes(e, e00 ) ↔ (directlyCauses(e, e00 )∨∃e0 (causes(e, e0 )∧causes(e0 , e00 ))) c3 causes(e, e0 ) → ¬causes(e0 , e) 4.7. Event Mereology We will not repeat here the axioms of the extensional atomic event mereology of UFO-B (see [13,2]). To that axiomatization, we add the following axioms. A part of an event must occur in all histories in which the whole occurs (m1). The ordering of event parts must be the same in all histories (m2) (literally, (m2) states that the length of the interval from a beginning of the whole to a comparable beginning of the part is constant). m1 hasPart(e, e0 ) ∧ beginPoint(e, xb ) ∧ endPoint(e, xe ) ∧ interval(xb , xe ) → ∃yb , ye (beginPoint(e0 , yb ) ∧ endPoint(e0 , ye ) ∧ subIntervalOf(yb , ye , xb , xe )) m2 hasPart(e, e0 ) ∧ beginPoint(e,t) ∧ beginPoint(e0 ,t 0 ) ∧ comparable(t,t 0 ) ∧ beginPoint(e0 ,t 00 ) ∧ comparable(t,t 00 ) → sameLength(t,t 0 ,t,t 00 ) 4.8. UFO-B? UFO-B? , defined by (a1), is the version of UFO-B (from [2]) where timePoints are partially ordered. UFO-AB, the unification of UFO-A and UFO-B, is defined by (a2). a1 UFO-B? = (UFO-B \ {(T1), . . . , (T14’), (S1’), . . . , (S8)}) ∪ {(t1), . . . , (t11), (e1), . . . , (e7), (s1), . . . , (s11), (c1), . . . , (c3), (m1), (m2)} a2 UFO-AB = UFO-A ∪ {(u1)} ∪ UFO-B? 5. Conclusion The Unified Foundational Ontology (UFO) was built with the goal of providing foun- dations for Conceptual Modeling. In order to do that, it must be able to address both structural and dynamic aspects of reality, i.e., it must be able to characterize ontological aspects of endurants, perdurants, as well as their interplay. These two realms of reality have so far been addressed by two formally independent theories, namely, UFO-A and UFO-B, respectively. In order to produce a theory unifying these two, one must be able to address the different treatment of modality in these two approaches, i.e., one must be able to reconcile the alethic modalities of necessity and contingency in UFO-A with models of time that are essential for talking about events, processes and causation in UFO-B. This paper presents a contribution in this direction. Firstly, we define a (i) translation of the axioms of UFO-A (in [8]) to FOL. We then (ii) revisit an excerpt of UFO-B (in [2]) to accommodate a partial order of time points, thus, producing a theory called UFO-B? . Finally, leveraging on (i) and (ii), we produce a formal unified theory called UFO-AB. Acknowledgments This study was financed in part by the Coordenação de Aperfeiçoamento de Pessoal de Nı́vel Superior – Brazil (CAPES) – Finance Code 001. Alessander is supported by grant 83740910/18 (FAPES/CAPES call 10/2018.) João Paulo is supported by CNPq grants 312123/2017-5 and 407235/2017-5. Giancarlo is supported by FUB (OCEAN Project). References [1] J. P. A. Almeida, P. D. Costa, and G. Guizzardi. Towards an ontology of scenes and situations. In 2018 IEEE Conference on Cognitive and Computational Aspects of Situation Management (CogSIMA), pages 29–35. IEEE, 2018. [2] A. B. Benevides, J.-R. Bourguet, G. Guizzardi, R. Peñaloza, and J. P. A. Almeida. Representing a reference foundational ontology of events in SROIQ. Applied Ontology, 2019. To appear. [3] A. B. Benevides, G. Guizzardi, B. F. B. Braga, and J. P. A. Almeida. Validating modal aspects of On- toUML conceptual models using automatically generated visual world structures. J. UCS, 16(20):2904– 2933, 2010. [4] G. S. Boolos, J. P. Burgess, and R. C. Jeffrey. Computability and Logic. Cambridge University Press, fifth edition, September 2007. [5] B. F. B. Braga, J. P. A. Almeida, G. Guizzardi, and A. B. Benevides. Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method. ISSE, 6(1-2):55–63, 2010. [6] D. Davidson. The individuation of events. In Essays in honor of Carl G. Hempel, pages 216–234. Springer, 1969. [7] M. Fitting and R. L. Mendelsohn. First-order modal logic, volume 277. Springer Science & Business Media, 1998. [8] G. Guizzardi. Ontological foundations for structural conceptual models. PhD Thesis, University of Twente, Enschede, The Netherlands, Enschede, Oct. 2005. [9] G. Guizzardi, R. de Almeida Falbo, and R. S. Guizzardi. Grounding software domain ontologies in the unified foundational ontology (UFO): The case of the ODE software process ontology. In CIbSE, pages 127–140, 2008. [10] G. Guizzardi, C. M. Fonseca, A. B. Benevides, J. P. A. Almeida, D. Porello, and T. P. Sales. Endurant types in ontology-driven conceptual modeling: Towards OntoUML 2.0. In Conceptual Modeling - 37th International Conference, ER 2018, Xi’an, China, October 22-25, 2018, Proceedings, pages 136–150, 2018. [11] G. Guizzardi and G. Wagner. Towards an ontological foundation of discrete event simulation. In Pro- ceedings of the 2010 Winter Simulation Conference, pages 652–664. IEEE, 2010. [12] G. Guizzardi and G. Wagner. Can BPMN be used for making simulation models? In Workshop on Enterprise and Organizational Modeling and Simulation, pages 100–115. Springer, 2011. [13] 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, pages 327–341, 2013. [14] S. Haack. Philosophy of logics. Cambridge University Press, 1978. [15] P. B. Ladkin, F. D. Anger, and R. V. Rodriguez. Temporal reasoning with intervals in branching time. Technical Report TR-90-028, International Computer Science Institute, July 1990. [16] L. B. Lombard. Relational change and relational changes. Philosophical Studies, 34(1):63–79, 1978. [17] L. B. Lombard. Events. Canadian Journal of Philosophy, IX(3):425–460, Sept. 1979. [18] L. B. Lombard. Events and the essentiality of time. Canadian Journal of Philosophy, XII(1):1–17, Mar. 1982. [19] L. B. Lombard. Causes, enablers, and the counterfactual analysis. Philosophical Studies, 59(2):195–211, 1990. [20] L. B. Lombard. Sooner or later. Noûs, 29(3):343–359, 1995. [21] L. B. Lombard. Ontologies of events. In S. Laurence and C. MacDonald, editors, Contemporary Read- ings in the Foundations of Metaphysics, pages 277–294. Oxford: Blackwell Publishing Ltd, 1998. [22] L. B. Lombard. Events: A Metaphysical Study. Routledge Library Editions: Metaphysics. Routledge, Mar. 2019. Originally published in 1986. [23] D. Porello and G. Guizzardi. Towards a first-order modal formalisation of the unified foundational ontology. In Proceedings of the Joint Ontology Workshops 2017 Episode 3: The Tyrolean Autumn of Ontology, Bozen-Bolzano, Italy, September 21-23, 2017., 2017. [24] W. V. O. Quine. New foundations for mathematical logic. The American mathematical monthly, 44(2):70–80, 1937. [25] W. V. O. Quine. From a logical point of view: 9 logico-philosophical essays. Harper & Row, New York, Hagerstown, San Francisco, London, second edition, 1963. [26] L. Vila and H. Reichgelt. The token reification approach to temporal reasoning. Artificial Intelligence, 83(1):59–74, 1996.