--- a/semantics/prov-sem.html Tue Apr 02 15:54:29 2013 +0100
+++ b/semantics/prov-sem.html Tue Apr 02 18:45:04 2013 +0100
@@ -1110,13 +1110,14 @@
alternative approaches to validity checking.</p>
<p>This document mostly considers the semantics of PROV statements and
- instances. PROV documents can consist of multiple instances, and
- the semantics does not (as yet) cover PROV documents, but the
+ instances. PROV documents can consist of multiple instances, such
+ as named bundles. The semantics does not (as yet) cover general PROV documents, but the
semantics can be used on each instance in a document separately,
just as PROV-CONSTRAINTS specifies that each instance in a document
is to be validated separately.
- So, in the rest of this document, we do not discuss PROV documents.
- The semantics of other features of PROV, such as dictionaries
+ So, in the rest of this document, we discuss only PROV instances and
+ not PROV documents.
+ The semantics of extensions of PROV, such as dictionaries
[[PROV-DICTIONARY]] and linking across bundles [[PROV-LINKS]], are
beyond the scope of this document. </p>
@@ -1138,10 +1139,10 @@
<li><a href="#theory">Section 5</a> presents the inferences and
constraints from PROV-CONSTRAINTS as first-order formulas, and gives
brief justifications for their soundness.</li>
- <li><a href="#soundness">Section 6</a> summarizes the main results.
- We show that Completeness does not hold for the naive semantics,
- but we establish a weak form of completeness: every valid PROV
- instance has a naive model.</li>
+ <li><a href="#soundness-completeness">Section 6</a> summarizes the
+ main results relating PROV-CONSTRAINTS validation to the semantics,
+ including soundness and a weak form of completeness: a PROV
+ instance is valid if and only if it has a naive model.</li>
</ul>
<div class="note">
<p>TODO: We would like to say something stronger here, such as a
@@ -1164,7 +1165,7 @@
<p>This document may be useful to users of PROV who have a formal
background and are interested in the rationale for some of the
- constructs of PROV; for resaerchers investigating extensions of PROV
+ constructs of PROV; for researchers investigating extensions of PROV
or alternative approaches to reasoning about PROV; or for future
efforts on provenance standardization. </p>
@@ -1226,20 +1227,21 @@
<p>A lowercase symbol $x,y,...$ on its own denotes an identifier.
Identifiers may or may not be URIs. Identifiers are viewed as
-variables from the point of view of logic: they denote objects, but
-just because we have two different identifiers $x$ and $y$ doesn't
-tell us that they denote different objects, since we could discover
-that they are actually the same later. We write $Identifiers$ for the
+variables from the point of view of logic. Identifiers denote objects, and
+two different identifiers $x$ and $y$ may denote equal or different objects. We write $Identifiers$ for the
set of identifiers of interest in a given situation (typically, the
set of identifiers present in the PROV instance of interest).
</p>
</section>
+<!--
<section>
<h3> Times and Intervals </h3>
-<p>We assume a linearly ordered set $(Times,\leq)$ of time instants. For convenience we assume the order is total or linear order, corresponding to a linear timeline; however, PROV does not assume that time is linear and events could be partially ordered and not necessarily reconciled to a single global clock.
+<p>We assume an ordered set $(Times,\leq)$ of time instants, where
+$Times \subseteq Val$ and $\leq$ is a linear order.
</p>
+
<div class="remark">
<p>Restricting attention to linearly-ordered times, and imposing this
order on events, is a simplifying assumption; it is more restrictive than required to model the
@@ -1249,11 +1251,20 @@
models such that every valid instance has a model.
</p>
</div>
-
-<p>We also consider a set $Intervals$ of closed intervals of the form $\{t \mid t_1 \leq t \leq t_2\}$.
+
+<p>We also consider a set $Intervals$ of subsets of $Times$ of the
+ form $[t_1,t_2] = \{t \mid t_1 \leq t \leq t_2\}$. Every interval has a minimum
+ and maximum time, written $min([t_1,t_2]) = t_1$ and $max([t_1,t_2])
+ = t_2$ respectively.
</p>
+
+
</section>
-
+ -->
+
+
+
+
<section>
<h3> Attributes and Values </h3>
@@ -1274,6 +1285,8 @@
$pl$ in $wasAssociatedWith$ and $a,g,u$ in $wasDerivedFrom$, as shown in the grammar below.
</p>
$$
+ \newcommand{\precedes}{~\mathrel{\textrm{precedes}}~}
+\newcommand{\strictlyPrecedes}{~\mathrel{\textrm{strictlyPrecedes}}~}
\begin{array}{rcl}
atomic\_formula & {::=}& element\_formula\\
& | & relation\_formula\\
@@ -1301,8 +1314,8 @@
& | & hadMember(c,e)\\
auxiliary\_formula
&{::=}& x = y\\
- & | & x \prec y\\
- & | & x \preceq y\\
+ & | & x \strictlyPrecedes y\\
+ & | & x \precedes y\\
& | & notNull(x)\\
& | & typeOf(x,ty)\\
attrs &::=& [attr_1 = v_1, \ldots,attr_n = v_n]\\
@@ -1318,7 +1331,7 @@
<p>We include the standard PROV collection types ($Collection$ and
$EmptyCollection$) and the membership relation $hadMember$; however,
we do not model dictionaries or the insertion or deletion relations
- in the PROV-DICTIONARY [[PROV-DICTIONARY]], since these are not part
+ in PROV-DICTIONARY [[PROV-DICTIONARY]], since these are not part
of the PROV recommendations. If these features are incorporated
into future standards, their semantics (and the soundness of the
associated constraints) should be modeled.
@@ -1332,8 +1345,8 @@
the standard features of PROV can be defined without talking about
multiple instances; however, the $mentionOf$ relation in
PROV-LINKS [[PROV-LINKS]] is intended to support linking across
- bundles. Future editions of PROV may incoporate $mentionOf$ or
- other cross-instance assertions, and this semantics should be
+ bundles. Future editions of PROV may incorporate $mentionOf$ or
+ other cross-instance assertions, and if so this semantics should be
generalized in order to provide a rationale for such an
extension and to establish the soundness of constaints associated
with $mentionOf$. </p>
@@ -1379,6 +1392,11 @@
<section id="structures">
<h2> Structures and Interpretations </h2>
+<p> In this section we define mathematical structures $W$ that can be used to
+interpret PROV formulas and instances. A structure consists of a
+collection of sets, functions and relations. THe components of a
+structure $W$ are given in the rest of the section in
+<em>components</em>, highlighted in boxes.
<section>
<h3> Things </h3>
@@ -1429,9 +1447,10 @@
that have discrete, fixed features, and relationships among these
objects. Some objects, called $Entities$, are associated with
$Things$, and their fixed attributes need to match those of the
- associated $Thing$ during their common lifetime.</p>
-
-<p>In this section, we detail the different subsets $Objects$, and
+ associated $Thing$ during their common lifetime. Others correspond
+ to agents, activities, or identifiable interactions among them.</p>
+
+<p>In this section, we detail the different subsets of $Objects$, and
give disjointness constraints and associated functions. Generally, these constraints are necessary to validate
disjointness constraints from PROV-CONSTRAINTS [[PROV-CONSTRAINTS]].
</p>
@@ -1473,7 +1492,8 @@
<section>
<h4> Entities </h4>
-<p>An <em>entity</em> is a kind of object that describes a time-slice of a thing, during which some of the thing's attributes are fixed. We assume:</p>
+<p>An <em>entity</em> is a kind of object that fixes some aspects of a
+ thing. We assume:</p>
<div class="component" id="entities">
<ol><li> a set $Entities \subseteq Objects$ of entities, disjoint from $Activities$ and $Events$ below.
@@ -1482,7 +1502,7 @@
lifetime(e)$, and for each attribute $a$ we have $value(e,a)
\subseteq value(thingOf(e),a,t)$ and $lifetime(e) \subseteq lifetime(thingOf(e))$.
</li>
-<li>a relation $SpecializationOf \subseteq Entities \times Entities$
+<!--<li>a relation $SpecializationOf \subseteq Entities \times Entities$
that is irreflexive and transitive. Furthermore, if $(e_1,e_2) \in
SpecializationOf$ then
<ol><li>
@@ -1492,6 +1512,7 @@
<li>For each attribute $attr$ we have $value(e_1,attr) \supseteq
value(e_2,attr)$.</li>
</ol></li>
+ -->
</ol>
</div>
@@ -1501,7 +1522,7 @@
different: for a thing, $value(x,a,t) = \emptyset$ means that the
attribute $a$ has no value at time $t$, whereas for an entity,
$value(x,a) = \emptyset$ only means that the thing associated to
- entity $x$ does not have a
+ entity $x$ need not have a
fixed value for $a$ during the lifetime of $x$. This does not imply
that $value(thingOf(e),a,t) = \emptyset$ when $t \in lifetime(e)$.
</p>
@@ -1528,10 +1549,10 @@
inconsistency in saying that an entity has two different values for
some attribute. In some
situations, further uniqueness constraints or range constraints
- could be imposed on attributes, for example by extending the PROV-O
- ontology.
+ could be imposed on attributes.
</p>
- <p>Only $Entities$ are associated with $Things$, and this is
+ <p>Only $Entities$ are associated with $Things$, and this
+ association is
necessary to provide an interpretation for the $alternateOf$ and
$specializationOf$ relations. It might also make sense
to associate $Agents$, $Activities$, and $Interactions$ with
@@ -1568,7 +1589,7 @@
<h4> Activities </h4>
-<p>An <em>activity</em> is an object that encompasses a set of events. We introduce
+<p>An <em>activity</em> is an object that encompasses a set of events. We introduce:
</p>
<div class="component" id="activities">
<ol><li>A set $Activities \subseteq Objects$ of activities.</li>
@@ -1598,71 +1619,97 @@
<section>
-<h4> Interactions </h4>
-
-<p>We consider a set $Interactions \subseteq Objects$ which are split into
+<h4> Influences </h4>
+
+<p>We consider a set $Influences \subseteq Objects$ which has disjoint
+ subsets
<em>Events</em> connecting entities and activities,
<em>Associations</em> between agents and activities,
+ <em>Attributions</em> between entities and agents,
<em>Communications</em> between pairs of activities,
<em>Delegations</em> between pairs of agents, and
<em>Derivations</em> that describe chains of generation and usage
- steps. These kinds of interactions are discussed further below. Interactions are disjoint from entities, activities and agents.
+ steps. These kinds of influences are discussed further below. Influences are disjoint from entities, activities and agents.
</p>
-<div class="component" id="interactions">
- <ol><li> A set $Interactions = Events \cup Associations \cup
+<div class="component" id="influences">
+ <ol><li> A set $Influences = Events \cup Associations \cup
Communications \cup Delegations \cup Derivations \subseteq Objects$
</li>
-<li> A function $type: Interactions \to
- \{start,end,usage,generation,invalidation,derivation,revision,quotation,primarySource,attribution,delegation\}$.
-</li>
<li> The sets $Events$, $Associations$, $Communications$, $Delegations$
- and $Derivations$ are all disjoint.
-</li><li> Interactions are disjoint from entities, agents and
-activities: $Interactions \cap (Entities \cup Activities \cup Agents) = \emptyset$
-</li></ol>
+ and $Derivations$ are all pairwise disjoint.
+</li><li> Influences are disjoint from entities, agents and
+activities: $Influences \cap (Entities \cup Activities \cup Agents) = \emptyset$
+</li>
+<li>An associated function $influenced : Influences \times
+ Objects \times Objects$ giving the source and target of each influence.</li>
+</ol>
</div>
<section>
<h5> Events </h5>
-<p>An <em>Event</em> is an interaction whose lifetime is a single time
+<p>An <em>Event</em> is an influence whose lifetime is a single time
instant, and relates an activity to an entity (which could be an
agent). Events have types including usage, generation, invalidation, starting and ending. Events are instantaneous. We introduce:
</p>
<div class="component" id="events">
-<ol><li> A set $Events \subseteq Interactions$ of events, such that
- $type(evt) \in \{start,end,generation,usage,invalidation\}$ if and
- only if $evt \in Events$.
-</li><li> A function $time : Events \to Times$ giving the time of each event; i.e. $lifetime(evt) = \{time(evt)\}$.
-</li><li> The derived ordering on events given by $evt_1 \leq evt_2 \iff time(evt_1) \leq time(evt_2)$
-</li></ol>
+<ol><li> A set $Events \subseteq Influences$ of events, partitioned
+ into disjoint subsets $Starts, Ends, Generations, Usages,
+ Invalidations$.
+</li><li> A function $time : Events \to Times$ giving the time of each
+event, such that $lifetime(evt) = \{time(evt)\}$.
+</li>
+<li> A quasi-ordering on events $\preceq \subset Events \times
+Events$. We write $e \prec e'$ when $e \preceq e'$ and $e'
+\not\preceq e$ hold.
+</li>
+<li>A function $started : Starts \to Activities \times Entities \times Activities$.
+</li>
+<li>A function $ended : Ends \to Activities \times Entities \times Activities$.
+</li>
+<li>A function $used : Usages \to Activities \times Entities$.
+</li>
+<li>A function $generated : Generations \to Entities \times Activities$.
+</li>
+<li>A function $invalidated : Invalidations \to Entities \times Activities$.
+</li>
+</ol>
</div>
</section>
<section>
<h5> Associations </h5>
-<p>An <em>Association</em> is an interaction relating an agent to an activity. To model associations, we introduce:
+<p>An <em>Association</em> is an influence relating an agent to an activity. To model associations, we introduce:
</p>
<div class="component" id="associations">
- <p>A set $Associations \subseteq Interactions$, such that
- $type(assoc) = association$ if and only if $assoc \in Associations$.
+ <p>A set $Associations \subseteq Influences$ with associated
+ function $associatedWith : Associations \to Agents \times Activities \times Plans_\bot$.
</p>
</div>
-<p>Associations are used below in the $ActsFor$ and $AssociatedWith$ relations.
+<section>
+
+<h5> Attributions </h5>
+
+<p>An <em>Attribution</em> is an influence relating an entity to an agent. To model associations, we introduce:
</p>
-
+<div class="component" id="attributions">
+ <p>A set $Attributions \subseteq Influences$ with associated
+ function $attributedTo : Attributions \toEntities \times Agents$.
+</p>
+ </div>
+
</section>
<section>
<h5>Communications</h5>
- <p>A <em>Communication</em> is an interaction indicating exchange of
+ <p>A <em>Communication</em> is an influence indicating exchange of
information between activities. To model communications, we introduce:
</p>
<div class="component" id="communications">
- <p>A set $Communications \subseteq Interactions$, such that
- $type(comm) = communication$ if and only if $comm \in Communications$.
+ <p>A set $Communications \subseteq Influences$ with associated
+ function $communicatedBy : Communications \to Generations \times Usages$.
</p>
</div>
@@ -1670,31 +1717,61 @@
</section>
<section>
<h5>Delegations</h5>
-<p>A <em>Delegation</em> is an interaction relating two agents. To model delegations, we introduce:
+<p>A <em>Delegation</em> is an influence relating two agents. To
+ model delegations, we introduce:
</p>
-<div class="component" id="associations">
- <p>A set Delegations \subseteq Interactions$, such that
- $type(del) = delegation$ if and only if $del \in Delegations$.
+<div class="component" id="delegations">
+ <p>A set $Delegations \subseteq Influences$ and associated function
+ $actsFor : Delegations \to Agents \times Agents \times Activities$
</p>
</div>
-<p>Associations are used below in the $ActsFor$ and $AssociatedWith$ relations.
</section>
<section>
<h5> Derivations </h5>
-<p>A <em>Derivation</em> is an interaction chaining one or more generation and use steps.
+<p>A <em>Derivation</em> is an influence chaining one or more
+ generation and use steps. To model derivations, we introduce an
+ auxiliary notion of <em>derivation path</em>. These paths are of the form </p>
+
+$$ent_n\cdot g_n\cdot act_n\cdot u_n\cdot ent_{n-1}\cdot ...\cdot
+ent_1\cdot g_1\cdot act_1\cdot u_1\cdot ent_0$$
+
+<p>where the $ent_i$ are entities, $act_i$ are activities, $g_i$ are generations, and $u_i$ are usages.
</p>
+<p>Formally, we consider the (regular) language:
+</p>
+$$DerivationPaths = Entities \cdot (Generations \cdot Activities \cdot
+Usages \cdot Entities)^+$$
+<p>with the constraints that for each derivation path:
+</p>
+<ul>
+<li>for each substring $ent\cdot g \cdot act$ we have $generated(g) = (ent,act)$, and
+</li>
+<li>for each substring $act \cdot u \cdot ent$ we have $used(u) = (act,ent)$.
+</li>
+</ul>
+
+
<div class="component" id="derivations">
-<p> A set $Derivations \subseteq Interactions$, such that
- $type(deriv) \in \{derivation, revision, primarySource,quotation\}$
- if and only if $deriv \in Derivations$.
-</p></div>
-<p>See below for the associated derivation path and DerivedFrom relation.
+<p> A set $Derivations \subseteq Influences$ with an associated
+ function $derivationPath : Derivations \to
+DerivationPaths$ linking each derivation to a derivation path. </p>
</p>
+</div>
<div class="remark">
+ <p>
+ The $derivationPath$ function links each $ d \in Derivations$ to a
+ derivation path. A derivation has exactly one associated derivation
+ path. However, if the PROV-N statement <span
+ class="name">wasDerivedFrom(e_2,e_1,-,-,-)</span> is asserted in an
+ instance, there may be multiple derivation paths linking $e_2$ to
+ $e_1$, each corresponding to a different, identified by different
+ derivations $d \in Derivations$.
+ </p>
+
<p>A derivation path implies the existence of at least one chained generation
and use step. However, not all such potential derivation paths are associated
with derivations; there can (and in general will) be many such paths
@@ -1703,17 +1780,23 @@
the existence of a derivation from the existence of an
alternating generation/use chain.
</p>
-</div>
+<p>
+ The reason why we need paths and not just individual derivation
+ steps is that $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ formulas can
+ represent multiple derivation steps.</p></div>
</section>
</section>
</section>
+
+
+<!--
<section>
<h3> Relations </h3>
<h4> Simple relations </h4>
-<p>The entities, interactions, and activities in a structure are related in the following ways:
+<p>The entities, influences, and activities in a structure are related in the following ways:
</p>
<ol><li> A relation $Used \subseteq Usage \times Entities$ saying when an event used an entity. An event can use at most one entity, and if $(evt,e)\in Used$ then $time(evt) \in lifetime(e)$ and $type(evt) = usage$ must hold.
</li><li> A relation $Generated \subseteq Events \times Entities$ saying when an event generated an entity. An event can generate at most one entity, and if $(evt,e)\in Generated$ then $min(lifetime(e)) = time(evt)$ and $type(evt) = generation$ must hold.
@@ -1753,7 +1836,7 @@
<section>
<h4> Derivation paths and DerivedFrom </h4>
-<p>Recall that above we introduced a subset of interactions called <em>Derivations</em>. These identify <em>paths</em> of the form </p>
+<p>Recall that above we introduced a subset of influences called <em>Derivations</em>. These identify <em>paths</em> of the form </p>
$$ent_n\cdot g_n\cdot act_n\cdot u_n\cdot ent_{n-1}\cdot ...\cdot
ent_1\cdot g_1\cdot act_1\cdot u_1\cdot ent_0$$
@@ -1783,26 +1866,32 @@
path. However, if the PROV-N statement <span
class="name">wasDerivedFrom(e_2,e_1,-,-,-)</span> is asserted in an
instance, there may be multiple derivation paths linking $e_2$ to
- $e_1$, each corresponding to a different, identified by different
+ $e_1$, each corresponding to a different path, identified by different
derivations $d \in Derivations$.
</p>
- </div>
-
-<div class="note">
- TODO:
- We can make the characterization of DerivationPaths more
- precise/concise by introducing sets of Usage and Generation events.
-</div>
-
-<div class="remark">The reason why we need paths and not just individual derivation steps is that $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ formulas can represent multiple derivation steps.</div>
+
+ <p>A derivation path implies the existence of at least one chained generation
+ and use step. However, not all such potential derivation paths are associated
+ with derivations; there can (and in general will) be many such paths
+ that are not associated with derivation steps. In other words, because we require derivations to be
+ explicitly assocated with derivation paths, it is not sound to infer
+ the existence of a derivation from the existence of an
+ alternating generation/use chain.
+ </p>
+<p>
+ The reason why we need paths and not just individual derivation
+ steps is that $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ formulas can
+ represent multiple derivation steps.</p></div>
+
</section>
</section>
+-->
<section>
<h3> Putting it all together </h3>
-<p>A <em>structure</em> $W$ is a structure containing all of the above
-described data. If we need to talk about the objects or relations of
+<p>A <em>structure</em> $W$ is a collection of sets, functions, and relations containing all of the above
+described components. If we need to talk about the objects or relations of
more than one structure then we may write $W_1.Objects$, $W_1.Things$,
etc.; otherwise, to
decrease notational clutter, when we consider a fixed structure then the names of the sets, relations and functions above refer to the components of that model.
@@ -1817,9 +1906,10 @@
<h3> Interpretations </h3>
<p>We need to link identifiers to the objects they denote. We do this using a function which we shall call an <em>interpretation</em>.
- Thus, we consider interpretations as follows:
-An interpretation is a function $\rho : Identifiers \to Objects$ describing
-which object is the target of each identifier. The mapping from identifiers to objects may <b>not</b> change over time.
+ An interpretation is a function $\rho : Identifiers \to Objects$ describing
+which object is the target of each identifier. The mapping from
+ identifiers to objects may <b>not</b> change over time; only
+ $Objects$ can be denoted by $Identifiers$.
</p>
</section>
@@ -1827,7 +1917,7 @@
<section id="semantics">
<h2> Semantics </h2>
-<p>In what follows, let $W$ be a fixed structure with the associated sets and relations discussed in the previous section, and let $I$ be an interpretation of identifiers as objects in $W$.
+<p>In what follows, let $W$ be a fixed structure with the associated sets and relations discussed in the previous section, and let $\rho$ be an interpretation of identifiers as objects in $W$.
The annotations [WF] refer to well-formedness constraints that correspond to typing constraints.
</p>
@@ -1835,7 +1925,7 @@
<h3> Satisfaction </h3>
<p>Consider a formula $\phi$, a structure $W$ and an interpretation
- $I$.
+ $\rho$.
We define notation $W,\rho \models \phi$ which means that $\phi$ is
satisfied in $W,\rho$. For atomic formulas, the definition of the
satisfaction relation is given in the next few subsections. We give
@@ -1846,10 +1936,12 @@
<ol>
<li>$W,\rho \models True$ always holds.</li>
<li>$W,\rho \models False$ never holds.</li>
+ <li>$W,\rho \models x = y$ holds if and only if $\rho(x) =
+ \rho(y)$.</li>
<li>$W,\rho \models \neg \phi$ holds if and only if $W,\rho \models
\phi$ does not hold.</li>
<li>$W,\rho \models \phi \wedge \psi$ holds if and only if $W,\rho \models
- \phi$ and $W,i\models \psi$.</li>
+ \phi$ and $W,\rho \models \psi$.</li>
<li>$W,\rho \models \phi \vee \psi$ holds if either $W,\rho \models \phi$
or $W,\rho \models \psi$ holds.</li>
<li>$W,\rho \models \phi \Rightarrow \psi$ holds if $W,\rho \models \phi$
@@ -1863,8 +1955,8 @@
<div class="remark">
<p>In the semantics above, note that the domain of quantification is
the set of $Objects$; that is, quantifiers range over entities,
- activities, agents, or interactions (which are in turn further
- subdivided into types of interactions). $Things$ and relations
+ activities, agents, or influences (which are in turn further
+ subdivided into types of influences). $Things$ and relations
cannot be referenced directly by identifiers.
</p>
</div>
@@ -1993,19 +2085,15 @@
<p>$W,\rho \models
wasGeneratedBy(id,e,a,t,attrs)$ holds if and only if:</a>
<ol>
-<li>[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$.
+<li>[WF] The identifier $id$ denotes a generation event $evt = \rho(id) \in Generations$.
</li>
<li>[WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$.
</li>
<li>[WF] The identifier $a$ denotes an activity $act = \rho(a) \in Activities$.
</li>
-<li>The event $evt$ is involved in $act$, that is, $(evt,act) \in EventActivity$.
-</li>
-<li>The type of $evt$ is $generation$, i.e. $type(evt) = generation$.
-</li>
<li>The event $evt$ occurred at time $\rho(t) \in Times$, i.e. $time(evt) = \rho(t)$.
</li>
-<li>The event $evt$ generated $ent$, i.e. $(evt,ent) \in Generated$.
+<li>The activity $act$ generated $ent$ via $evt$, i.e. $generated(evt) = (ent,act)$.
</li>
<li>The attribute values match: $match(W,evt,attrs)$.
</li>
@@ -2024,20 +2112,16 @@
<p>$W,\rho \models used(id,a,e,t,attrs)$ holds if and only if:</p>
<ol>
</li>
-<li>[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$.
+<li>[WF] The identifier $id$ denotes a usage event $evt = \rho(id) \in Usages$.
</li>
<li>[WF] The identifier $a$ denotes an activity $act = \rho(id) \in Activities$.
</li>
<li>[WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$.
</li>
-<li>The event $evt$ is part of $act$, i.e. $(evt,act) \in EventActivity$.
-</li>
-<li>The type of $evt$ is $use$, i.e., $type(evt) = use$.
-</li>
<li>The event $evt$ occurred at time $\rho(t) \in Times$,
i.e. $time(evt) = \rho(t)$.
</li>
-<li>The event $evt$ used $obj$, i.e. $(evt,ent) \in Used$.
+<li>The activity $act$ used $obj$ via $evt$, i.e. $used(evt) = (act,ent)$.
</li>
<li>The attribute values match: $match(W,evt,attrs)$.
</li></ol></div>
@@ -2051,20 +2135,16 @@
<div class="semantics" id="invalidation-semantics"> <p>An invalidation formula $W,\rho \models
wasInvalidatedBy(id,e,a,t,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$.
+<li>[WF] The identifier $id$ denotes an invalidation event $evt = \rho(id) \in Invalidations$.
</li>
<li>[WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$.
</li>
<li>[WF] The identifier $a$ denotes an activity $act = \rho(a) \in Activities$.
</li>
-<li>The event $evt$ is involved in $act$, that is, $(evt,act) \in EventActivity$.
-</li>
-<li>The type of $evt$ is $invalidation$, i.e. $type(evt) = invalidation$.
-</li>
<li>The event $evt$ occurred at time $\rho(t) \in Times$,
i.e. $time(evt) = \rho(t)$.
</li>
-<li>The event $evt$ invalidated $ent$, i.e. $(evt,ent) \in Invalidated$.
+<li>The activity $act$ invalidated $ent$ via $evt$, i.e. $invalidated(evt) = (ent,act)$.
</li>
<li>The attribute values match: $match(W,evt,attrs)$.
</li></ol></div>
@@ -2087,7 +2167,7 @@
</li>
<li>[WF] $pl$ denotes a plan $plan=\rho(pl) \in Plans$.
</li>
-<li>The association associates the agent with the activity and plan, i.e. $(assoc,agent,act,plan) \in AssociatedWith$.
+<li>The association associates the agent with the activity and plan, i.e. $$associatedWith(assoc) = (agent,act,plan)$.
</li>
<li>The attributes match: $match(W,assoc,attrs)$.
</li></ol></div>
@@ -2101,20 +2181,21 @@
</li>
<li>[WF] $ag$ denotes an agent $agent = \rho(ag) \in Agents$.
</li>
-<li>The association associates the agent with the activity and plan, i.e. $(assoc,agent,act,\bot) \in AssociatedWith$.
+<li>The association associates the agent with the activity and no
+ plan, i.e. $associatedWith(assoc) = (agent,act,\bot)$.
</li>
<li>The attributes match: $match(W,assoc,attrs)$.
</li></ol></div>
</section>
<section>
-<h5> Start Formulas </h5>
+<h5> Start </h5>
<p>A start formula $wasStartedBy(id,a_2,e,a_1,t,attrs)$ is interpreted as follows:</p>
<div class="semantics" id="start-semantics">
<p>$W,\rho \models wasStartedBy(id,a_2,e,a_1,t,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes an event $evt = \rho(id) \in Events$.
+<li>[WF] $id$ denotes a start event $evt = \rho(id) \in Starts$.
</li>
<li>[WF] $a_2$ denotes an activity $act_2 = \rho(a_2) \in Activities$.
</li>
@@ -2122,15 +2203,10 @@
</li>
<li>[WF] $a_1$ denotes an activity $act_1 = \rho(a_1) \in Activities$.
</li>
-<li>The event $evt$ has type $start$, i.e. $type(evt) = start$.
+<li>The event happened at the start of $act_2$, that is, $\rho(t) = min(lifetime(act_2)) = time(evt)$.
</li>
-<li>The event happened at the start of $act_2$, that is, $(evt,act_2)
- \in EventActivity$, and $\rho(t) = min(lifetime(act_2)) = time(evt)$.
-</li>
-<li> The activity $act_1$ started $act_2$ via entity $ent$: that is, $(evt,act_2,ent,act_1) \in Start$.</li>
-<li>The event happened during $act_1$, that is, $(evt,act_1)
- \in EventActivity$.
-</li>
+<li> The activity $act_1$ started $act_2$ via entity $ent$: that is,
+ $started(evt) = (act_2,ent,act_1)$.</li>
<li>The attributes match: $match(W,evt,attrs)$.
</li></ol></div>
</section>
@@ -2145,16 +2221,13 @@
if:</p>
<ol>
- <li>[WF] $id$ denotes an event $evt = \rho(id) \in Events$.</li>
+ <li>[WF] $id$ denotes an end event $evt = \rho(id) \in Ends$.</li>
<li> [WF] $a_2$ denotes an activity $act_2 = \rho(a_2)\in Activities$.</li>
<li> [WF] $e$ denotes an entity $ent = \rho(e)\in Entities$.</li>
<li>[WF] $a_1$ denotes an activity $act_1 = \rho(a_1)\in Activities$.</li>
-<li>The event $evt$ has type $end$, i.e. $type(evt) = end$.</li>
-<li>The event happened at the end of $act_2$, that is, $(evt,act_2)
- \in EventActivity$, and $\rho(t) = max(lifetime(act_2)) = time(evt)$.</li>
+<li>The event happened at the end of $act_2$, that is, $\rho(t) = max(lifetime(act_2)) = time(evt)$.</li>
<li> The activity $act_1$ ended $act_2$ via entity $ent$: that is,
- $(evt,act_2,ent,act_1) \in End$.</li>
-<li>The event happened during $act_1$, that is, $(evt,act_1) \in EventActivity$.</li>
+ $ended(evt) = (act_2,ent,act_1)$.</li>
<li>The attributes match: $match(W,evt,attrs)$.</li>
</ol>
</div>
@@ -2178,7 +2251,8 @@
</li>
<li>[WF] $ag$ denotes an agent $agent = \rho(ag) \in Agents$.
</li>
-<li>The entity was attributed to the agent, i.e. $(assoc,ent,agent) \in AttributedTo$.
+<li>The entity was attributed to the agent, i.e. $attributedTo(assoc)
+= (ent,agent)$.
</li>
<li>The attributes match: $match(W,evt,attrs)$.
</li></ol>
@@ -2200,9 +2274,8 @@
<li>[WF] $a_1,a_2$ denote activities $act_1 = \rho(a_1) \in
Activities, act_2 = \rho(a_2)\in Activities$.
</li>
-<li>TODO: There exists some intermediate entity $ent$, generation $gen \in
-Events$ and usage $use \in Events$ such that $(gen,ent,act) \in
-Generation$ and $(use,act_2,ent) \in Usage$
+<li>There exist $gen,use,ent$ such that $communicatedBy(comm) =
+(gen,use)$ and $generated(gen) = (ent,act_1)$ and $used(use) = (act_2,ent)$.
</li>
<li>The attributes match: $match(W,comm,attrs)$.
</li></ol>
@@ -2226,7 +2299,8 @@
</li>
<li>[WF] $ag_1,ag_2$ denote agents $agent_1=\rho(ag_1), agent_2=\rho(ag_2) \in Agents$.
</li>
-<li>The agent $agent_2$ acts for the agent $agent_1$ with respect to the activity $act$, i.e. $(deleg,agent_2,agent_1,act) \in ActsFor$.
+<li>The agent $agent_2$ acted for the agent $agent_1$ with respect to
+ the activity $act$, i.e. $actedFor(deleg) = (agent_2,agent_1,act)$.
</li>
<li>The attributes match: $match(W,assoc,attrs)$.
</li></ol></div>
@@ -2261,9 +2335,9 @@
</li>
<li>[WF] $a$ denotes an activity $act = \rho(a) \in Activities$.
</li>
-<li>[WF] $g$ denotes a generation event $gen = \rho(g) \in Events$ and $type(\rho(g)) = generation$.
+<li>[WF] $g$ denotes a generation event $gen = \rho(g) \in Generations$.
</li>
-<li>[WF] $u$ denotes a use event $\rho(u) \in Events$ and $type(\rho(u)) = use$.
+<li>[WF] $u$ denotes a use event $\rho(u) \in Usages$.
</li>
<li>The derivation denotes a one-step derivation path linking the
entities via the activity, generation and use: $derivationPath(deriv) =
@@ -2282,11 +2356,11 @@
<div class="semantics" id="derivation-imprecise-semantics">
<p>$W,\rho \models wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes a derivation $deriv = \rho(id) \in Derivations$
+<li>[WF] $id$ denotes a derivation $deriv = \rho(id) \in Derivations$.
</li>
-<li>[WF] $e_1,e_2$ denote entities $ent_1 = \rho(e_1), ent_2=\rho(e_2) \in Entities$
+<li>[WF] $e_1,e_2$ denote entities $ent_1 = \rho(e_1), ent_2=\rho(e_2) \in Entities$ .
</li>
-<li>$derivationPath(deriv)= ent_2 \cdot w \cdot ent_1$ for some $w$
+<li>$derivationPath(deriv)= ent_2 \cdot w \cdot ent_1$ for some $w$.
</li>
<li>The attribute values match: $match(W,deriv,attrs)$.
</li></ol></div>
@@ -2300,10 +2374,13 @@
<p>$W,\rho \models wasInfluencedBy(id,o_2,o_1,attrs)$ holds if
and only if at least one of the following hold:</p>
<ol>
+ <li>[WF] $id$ denotes an influence $inf = \rho(id) \in Influences$.
<li>[WF] $o_1$ and $o_2$ denote objects $obj_1 = \rho(o_1) \in
Objects$ and $obj_2= \rho(o_2)
\in Objects$.</li>
- <li>The objects are inthe Influence relation: $(id,o_2,o_1) \in Influence$.</li>
+ <li>The influence $inf$ links $o_2$ with $o_1$; that is,
+ $influenced(inf) = (o_2,o_1)$.
+ </li>
<li>The attribute values match: $match(W,deriv,attrs)$.
</li>
</ol>
@@ -2325,13 +2402,19 @@
distinct entities $ent_1
= \rho(e_1) \in Entities$ and $ent_2 = \rho(e_2) \in Entities$.
</li>
-<li>$(ent_1,ent_2) \in SpecializationOf$.
+<!--<li>$(ent_1,ent_2) \in SpecializationOf$.-->
+<ol>
+ <li>The two entities are different: $ent_1 \neq ent_2$.
+ <li>The two entities present aspects of the same thing, that is, $thingOf(ent_1) = thingOf(ent_2)$.
</li>
+<li>The lifetime of $ent_1$ is contained in that of $ent_2$, i.e. $lifetime(ent_1) \subseteq lifetime(ent_2)$.
+</li>
+<li>For each attribute $attr$ we have $value(ent_1,attr) \supseteq value(ent_2,attr)$.
</ol>
</div>
<div class="remark">
- <p>The conditions on the $SpecializationOf$ relation imply that:</p>
+ <!--<p>The conditions on the $SpecializationOf$ relation imply that:</p>
<ol>
<li>The two entities are different: $ent_1 \neq ent_2$.
<li>The two Entities refer to the same Thing, that is, $thingOf(ent_1) = thingOf(ent_2)$.
@@ -2340,11 +2423,14 @@
</li>
<li>For each attribute $attr$ we have $value(ent_1,attr) \supseteq value(ent_2,attr)$.
</li></ol>
+-->
<p>The second criterion says that the two Entities present (possibly different) aspects of
the same Thing. Note that the third criterion allows $ent_1$ and
$ent_2$ to have the same lifetime (or that of $ent_2$ can be larger).
The last criterion allows $ent_1$ to have more defined attributes than
-$ent_2$, but they must include the attributes defined by $ent_2$.
+$ent_2$, but they must include the attributes defined by $ent_2$. Two
+ different entities that have the same attributes can also be related
+ by specialization.
</p>
</div>
</section>
@@ -2393,43 +2479,33 @@
</section>
<section>
- <h3>Auxiliary formulas</h3>
+ <h3>Semantics of Auxiliary Formulas</h3>
<p>In this section, we define the semantics of additional formulas
concerning ordering, null values, and typing. These are used in the
logical versions of constraints.</p>
<section>
- <h4>Equals</h4>
- <p>As usual, an equality formula means that two expressions denote
- the same value. Identifiers always denote $Objects$.</p>
- <div class="semantics" id="equals-semantics">
- <p>$W,\rho \models x = y$ holds if and only if $\rho(x) =
- \rho(y)$.</p>
- </div>
- </section>
- <section>
<h4>Precedes and Strictly Precedes</h4>
- <p>The precedes relation $x \preceq y$ holds between two events, one taking
+ <p>The precedes relation $x \precedes y$ holds between two events, one taking
place before (or simultaneously with) another. Since the
naive semantics assumes that times are linearly ordered and
event times are
mapped to a single time line, this amounts to
comparing the event times. The semantics of strictly precedes ($x
- \prec y$) is similar, only $x$ must take place strictly before $y$.</p>
+ \strictlyPrecedes y$) is similar, only $x$ must take place strictly before $y$.</p>
<div class="semantics" id="precedes-semantics">
<ol>
- <li>$W,\rho \models x \preceq y$ holds if and only if
- $\rho(x),\rho(y) \in Events$ and $time(\rho(x)) \leq time(\rho(y))$.</li>
- <li>$W,\rho \models x \prec y$ holds if and only if
- $\rho(x),\rho(y) \in Events$ and $time(\rho(x)) < time(\rho(y))$.</li>
+ <li>$W,\rho \models x \precedes y$ holds if and only if
+ $\rho(x),\rho(y) \in Events$ and $\rho(x) \preceq\rho(y)$.</li>
+ <li>$W,\rho \models x \strictlyPrecedes y$ holds if and only if
+ $\rho(x),\rho(y) \in Events$ and $\rho(x) \prec \rho(y)$.</li>
</ol>
</div>
<div class="remark">
- <p> Because we use a linearly ordered time to define event
- precedence, there are valid PROV instances that are not satisfied
- in any naive model. For example:</p>
+ <p> Although times are linearly ordered, the time ordering is
+ unrelated to the event ordering. For example:</p>
<pre>
entity(e)
activity(a1)
@@ -2438,7 +2514,8 @@
wasGeneratedBy(gen2; e, a2, 2012-11-16T16:05:00) //different date
</pre>
<p>This instance is valid, and must satisfy precedence constraints
- $gen_1 \preceq gen_2$ and $gen_2 \preceq gen_1$, but $time(gen_1)=
+ $gen_1 \precedes gen_2$ and $gen_2 \precedes gen_1$, but this does not
+ imply anything about the relative orderings of the associated times.
</p>
</div>
@@ -2471,7 +2548,7 @@
<li>$W,\rho\models typeOf(ag,agent)$ holds if and only if
$\rho(ag) \in Agents$.</li>
<li>$W,\rho\models typeOf(c,Collection)$ holds if and only if
- $\rho(c) \in Collections.</li>
+ $\rho(c) \in Collections$.</li>
<li>$W,\rho\models typeOf(c,EmptyCollection)$ holds if and only if
$\rho(c) \in Collections$ and there is no $e \in Entities$ such
that $(e,\rho(c)) \in MemberOf$.</li>
@@ -2483,6 +2560,7 @@
</section>
</section>
</section>
+ </section>
<section id="theory">
<h2> Inferences and Constraints </h2>
@@ -2546,7 +2624,9 @@
\quad\Rightarrow
\exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])
\end{array}$</div>
-<div class="inference" number="11" id="derivation-generation-use-inference"><p>In this inference, none of $a$,$gen_2$, or $use_1$ can be placeholders -.</p>$\begin{array}[t]{l}
+<div class="inference" number="11"
+ id="derivation-generation-use-inference">
+ $\begin{array}[t]{l}
\forall id,e_2,e_1,a,gen_2,use_1,attrs.~
\\
\qquad notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(id,e_2,e_1,a,gen_2,use_1,attrs)
@@ -2554,7 +2634,9 @@
\quad\Rightarrow
\exists t_1,t_2.~used(use_1,a,e_1,t_1,[]) \wedge wasGeneratedBy(gen_2,e_2,a,t_2,[])
\end{array}$</div>
-<div class="inference" number="12" id="revision-is-alternate-inference"><p>In this inference, any of $a$,$gen_2$, or $use_1$ can be placeholders -.</p>$\begin{array}[t]{l}
+<div class="inference" number="12"
+ id="revision-is-alternate-inference">
+ $\begin{array}[t]{l}
\forall id,e_1,e_2,a,g,u.~
\\
\qquad wasDerivedFrom(id,e_2,e_1,a,g,u,[prov:type = prov:Revision]))
@@ -2627,14 +2709,16 @@
\\
\quad\Rightarrow
wasInfluencedBy(id,e_2,e_1,attrs)
-\end{array}$</li><li><p>In this rule, $a$,$g$, or $u$ may be placeholders -.</p>$\begin{array}[t]{l}
+\end{array}$</li><li>
+$\begin{array}[t]{l}
\forall id,e,ag,attrs.~
\\
\qquad wasAttributedTo(id,e,ag,attrs)
\\
\quad\Rightarrow
wasInfluencedBy(id,e,ag,attrs)
-\end{array}$</li><li><p>In this rule, $pl$ may be a placeholder -.</p>$\begin{array}[t]{l}
+\end{array}$</li><li>
+$\begin{array}[t]{l}
\forall id,a,ag,pl,attrs.~
\\
\qquad wasAssociatedWith(id,a,ag,pl,attrs)
@@ -2699,6 +2783,7 @@
\quad\Rightarrow
specializationOf(e_1,e_3)
\end{array}$</div>
+<!--
<div class="proof">
<p> Suppose the conditions for specialization hold of $ent_1$ and
$ent_2$ and for $ent_2$ and $ent_3$, where $ent_1 = \rho(e_1)$ and $ent_2 = \rho(e_2)$ and $ent_3 =
@@ -2710,6 +2795,7 @@
How do we know $e_3 \neq e_1$? Need strict ordering on entities in semantics.)
</p>
</div>
+-->
<div class="inference" number="20" id="specialization-alternate-inference">$\begin{array}[t]{l}
\forall e_1,e_2.~
@@ -2906,7 +2992,7 @@
\qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start \preceq end
+start \precedes end
\end{array}$</div>
<div class="constraint" number="31" id="start-start-ordering">$\begin{array}[t]{l}
\forall start_1,start_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -2914,7 +3000,7 @@
\qquad wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasStartedBy(start_2,a,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start_1 \preceq start_2
+start_1 \precedes start_2
\end{array}$</div>
<div class="constraint" number="32" id="end-end-ordering">$\begin{array}[t]{l}
\forall end_1,end_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -2922,7 +3008,7 @@
\qquad wasEndedBy(end_1,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-end_1 \preceq end_2
+end_1 \precedes end_2
\end{array}$</div>
<div class="constraint" number="33" id="usage-within-activity"><ol><li>$\begin{array}[t]{l}
\forall start,use,a,e_1,e_2,a_1,t_1,t_2,attrs_1,attrs_2.~
@@ -2930,14 +3016,14 @@
\qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge used(use,a,e_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start \preceq use
+start \precedes use
\end{array}$</li><li>$\begin{array}[t]{l}
\forall use,end,a,e_1,e_2,a_2,t_1,t_2,attrs_1,attrs_2.~
\\
\qquad used(use,a,e_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-use \preceq end
+use \precedes end
\end{array}$</li></ol></div>
<div class="constraint" number="34" id="generation-within-activity"><ol><li>$\begin{array}[t]{l}
\forall start,gen,e_1,e_2,a,a_1,t_1,t_2,attrs_1,attrs_2.~
@@ -2945,14 +3031,14 @@
\qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen,e_2,a,t_2,attrs_2)
\\
\quad\Rightarrow
-start \preceq gen
+start \precedes gen
\end{array}$</li><li>$\begin{array}[t]{l}
\forall gen,end,e,e_1,a,a_1,t,t_1,attrs,attrs_1.~
\\
\qquad wasGeneratedBy(gen,e,a,t,attrs) \wedge wasEndedBy(end,a,e_1,a_1,t_1,attrs_1)
\\
\quad\Rightarrow
-gen \preceq end
+gen \precedes end
\end{array}$</li></ol></div>
<div class="constraint" number="35" id="wasInformedBy-ordering">$\begin{array}[t]{l}
\forall id,start,end,a_1,a_1',a_2,a_2',e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2.~
@@ -2960,7 +3046,7 @@
\qquad wasInformedBy(id,a_2,a_1,attrs) \wedge wasStartedBy(start,a_1,e_1,a_1',t_1,attrs_1) \wedge wasEndedBy(end,a_2,e_2,a_2',t_2,attrs_2)
\\
\quad\Rightarrow
-start \preceq end
+start \precedes end
\end{array}$</div>
<div class="constraint" number="36" id="generation-precedes-invalidation">$\begin{array}[t]{l}
\forall gen,inv,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -2968,7 +3054,7 @@
\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen \preceq inv
+gen \precedes inv
\end{array}$</div>
<div class="constraint" number="37" id="generation-precedes-usage">$\begin{array}[t]{l}
\forall gen,use,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -2976,7 +3062,7 @@
\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(use,a_2,e,t_2,attrs_2)
\\
\quad\Rightarrow
-gen \preceq use
+gen \precedes use
\end{array}$</div>
<div class="constraint" number="38" id="usage-precedes-invalidation">$\begin{array}[t]{l}
\forall use,inv,a_1,a_2,e,t_1,t_2,attrs_1,attrs_2.~
@@ -2984,7 +3070,7 @@
\qquad used(use,a_1,e,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-use \preceq inv
+use \precedes inv
\end{array}$</div>
<div class="constraint" number="39" id="generation-generation-ordering">$\begin{array}[t]{l}
\forall gen_1,gen_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -2992,7 +3078,7 @@
\qquad wasGeneratedBy(gen_1,e,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen_1 \preceq gen_2
+gen_1 \precedes gen_2
\end{array}$</div>
<div class="constraint" number="40" id="invalidation-invalidation-ordering">$\begin{array}[t]{l}
\forall inv_1,inv_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -3000,7 +3086,7 @@
\qquad wasInvalidatedBy(inv_1,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-inv_1 \preceq inv_2
+inv_1 \precedes inv_2
\end{array}$</div>
<div class="constraint" number="41"
id="derivation-usage-generation-ordering"><p>In this constraint, $a$,$gen_2$, or $use_1$ must not be placeholders -.</p>$\begin{array}[t]{l}
@@ -3009,7 +3095,7 @@
\qquad notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(d,e_2,e_1,a,gen_2,use_1,attrs)
\\
\quad\Rightarrow
-use_1 \preceq gen_2
+use_1 \precedes gen_2
\end{array}$</div>
<div class="constraint" number="42" id="derivation-generation-generation-ordering"><p>In this constraint, any of $a$,$g$, or $u$ may be placeholders -.</p>$\begin{array}[t]{l}
\forall d,gen_1,gen_2,e_1,e_2,a,a_1,a_2,g,u,t_1,t_2,attrs,attrs_1,attrs_2.~
@@ -3017,7 +3103,7 @@
\qquad wasDerivedFrom(d,e_2,e_1,a,g,u,attrs) \wedge wasGeneratedBy(gen_1,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen_1 \prec gen_2
+gen_1 \strictlyPrecedes gen_2
\end{array}$</div>
<div class="constraint" number="43" id="wasStartedBy-ordering"><ol><li>$\begin{array}[t]{l}
\forall gen,start,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -3025,14 +3111,14 @@
\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasStartedBy(start,a,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen \preceq start
+gen \precedes start
\end{array}$</li><li>$\begin{array}[t]{l}
\forall start,inv,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
\\
\qquad wasStartedBy(start,a,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start \preceq inv
+start \precedes inv
\end{array}$</li></ol></div>
<div class="constraint" number="44" id="wasEndedBy-ordering"><ol><li>$\begin{array}[t]{l}
\forall gen,end,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -3040,14 +3126,14 @@
\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen \preceq end
+gen \precedes end
\end{array}$</li><li>$\begin{array}[t]{l}
\forall end,inv,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
\\
\qquad wasEndedBy(end,a,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-end \preceq inv
+end \precedes inv
\end{array}$</li></ol></div>
<div class="constraint" number="45" id="specialization-generation-ordering">$\begin{array}[t]{l}
\forall gen_1,gen_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -3055,7 +3141,7 @@
\qquad specializationOf(e_2,e_1) \wedge wasGeneratedBy(gen_1,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen_1 \preceq gen_2
+gen_1 \precedes gen_2
\end{array}$</div>
<div class="constraint" number="46" id="specialization-invalidation-ordering">$\begin{array}[t]{l}
\forall inv_1,inv_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -3063,7 +3149,7 @@
\qquad specializationOf(e_1,e_2) \wedge wasInvalidatedBy(inv_1,e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-inv_1 \preceq inv_2
+inv_1 \precedes inv_2
\end{array}$</div>
<div class="constraint" number="47" id="wasAssociatedWith-ordering"><p>In the following inferences, $pl$ may be a placeholder -.</p><ol><li>$\begin{array}[t]{l}
\forall assoc,start_1,inv_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
@@ -3071,28 +3157,28 @@
\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,ag,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start_1 \preceq inv_2
+start_1 \precedes inv_2
\end{array}$</li><li>$\begin{array}[t]{l}
\forall assoc,gen_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
\\
\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasGeneratedBy(gen_1,ag,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen_1 \preceq end_2
+gen_1 \precedes end_2
\end{array}$</li><li>$\begin{array}[t]{l}
\forall assoc,start_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
\\
\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,ag,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start_1 \preceq end_2
+start_1 \precedes end_2
\end{array}$</li><li>$\begin{array}[t]{l}
\forall assoc,start_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
\\
\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasStartedBy(start_1,ag,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start_1 \preceq end_2
+start_1 \precedes end_2
\end{array}$</li></ol></div>
<div class="constraint" number="48" id="wasAttributedTo-ordering"><ol><li>$\begin{array}[t]{l}
\forall att,gen_1,gen_2,e,a_1,a_2,t_1,t_2,ag,attrs,attrs_1,attrs_2.~
@@ -3100,14 +3186,14 @@
\qquad wasAttributedTo(att,e,ag,attrs) \wedge wasGeneratedBy(gen_1,ag,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen_1 \preceq gen_2
+gen_1 \precedes gen_2
\end{array}$</li><li>$\begin{array}[t]{l}
\forall att,start_1,gen_2,e,e_1,a_1,a_2,ag,t_1,t_2,attrs,attrs_1,attrs_2.~
\\
\qquad wasAttributedTo(att,e,ag,attrs) \wedge wasStartedBy(start_1,ag,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start_1 \preceq gen_2
+start_1 \precedes gen_2
\end{array}$</li></ol></div>
<div class="constraint" number="49" id="actedOnBehalfOf-ordering"><ol><li>$\begin{array}[t]{l}
\forall del,gen_1,inv_2,ag_1,ag_2,a,a_1,a_2,t_1,t_2,attrs,attrs_1,attrs_2.~
@@ -3115,14 +3201,14 @@
\qquad actedOnBehalfOf(del,ag_2,ag_1,a,attrs) \wedge wasGeneratedBy(gen_1,ag_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,ag_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-gen_1 \preceq inv_2
+gen_1 \precedes inv_2
\end{array}$</li><li>$\begin{array}[t]{l}
\forall del,start_1,end_2,ag_1,ag_2,a,a_1,a_2,e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2.~
\\
\qquad actedOnBehalfOf(del,ag_2,ag_1,a,attrs) \wedge wasStartedBy(start_1,ag_1,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,ag_2,e_2,a_2,t_2,attrs_2)
\\
\quad\Rightarrow
-start_1 \preceq end_2
+start_1 \precedes end_2
\end{array}$</li></ol></div>
</section>
@@ -3325,7 +3411,7 @@
\end{array}$</div>
<div class="proof">
<p>This follows from the assumption that the different classes of
- interactions are disjoint sets, characterized by their types.
+ influences are disjoint sets, characterized by their types.
</p>
</div>
<div class="constraint" number="54" id="impossible-object-property-overlap"><p>For each $p \in \{entity,activity,agent\}$ and each $r \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$, the following constraint holds:</p>$\begin{array}[t]{l}
@@ -3337,7 +3423,7 @@
False
\end{array}$</div>
<div class="proof">
- <p>This follows from the assumption that interactions are distinct
+ <p>This follows from the assumption that influences are distinct
from other objects (entities, activities or agents).
</p>
</div>
@@ -3372,8 +3458,10 @@
</section>
+<section id="soundness-completeness">
+ <h2>Soundness and Completeness</h2>
<section id="soundness">
-<h2>Soundness</h2>
+ <h3>Soundness</h3>
<p>Above we have presented arguments for the soundness of the
constraints and inferences with respect to the naive semantics.
@@ -3409,6 +3497,7 @@
remaining constraints, so $I$ is valid.</p>
</div>
+ </section>
<section id="completeness">
<h3>Weak Completeness</h3>