--- a/semantics/prov-sem.html Thu Apr 04 09:08:51 2013 -0400
+++ b/semantics/prov-sem.html Thu Apr 04 15:41:22 2013 +0100
@@ -1286,9 +1286,9 @@
$pl$ in $wasAssociatedWith$ and $a,g,u$ in $wasDerivedFrom$, as shown in the grammar below.
</p>
$$
- \newcommand{\precedes}{~\mathrel{\textrm{precedes}}~}
+\newcommand{\precedes}{~\mathrel{\textrm{precedes}}~}
\newcommand{\strictlyPrecedes}{~\mathrel{\textrm{strictlyPrecedes}}~}
-\begin{array}{rcl}
+ \begin{array}{rcl}
atomic\_formula & {::=}& element\_formula\\
& | & relation\_formula\\
& | & auxiliary\_formula\\
@@ -1314,8 +1314,7 @@
& |& specializationOf(e_1,e_2)\\
& | & hadMember(c,e)\\
auxiliary\_formula
- &{::=}& x = y\\
- & | & x \strictlyPrecedes y\\
+ &{::=}& x \strictlyPrecedes y\\
& | & x \precedes y\\
& | & notNull(x)\\
& | & typeOf(x,ty)\\
@@ -1364,7 +1363,8 @@
\phi &{::=}& atomic\_formula\\
& | & True\\
& | & False\\
-&|& \neg~\phi\\
+&|&x = y\\
+& | & \neg~\phi\\
&|& \phi_1 \wedge \phi_2\\
&|& \phi_1 \vee \phi_2\\
&|& \phi_1 \Rightarrow \phi_2\\
@@ -1395,7 +1395,7 @@
<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
+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>
@@ -1408,18 +1408,18 @@
</p>
<div class="component" id="things"><ol>
<li> a set $Things$ of things</li>
- <li> a function $lifetime : Things \to Intervals$ from things to time intervals</li>
+ <li> a function $lifetime : Things \to Intervals$ from things to intervals</li>
<li>a function $value : Things \times Attributes \times Times \to P(Values)$
</li>
</ol>
</div>
<p>
The range of $value$ is the set $P(Values)$, indicating that $value$
-is essentially a multi-valued that returns a set of values (possibly empty). When $value(x,a,t) =
+is essentially a multi-valued function that returns a set of values (possibly empty). When $value(x,a,t) =
\emptyset$, we say that attribute $a$ is undefined for $x$ at time $t$.</p>
<p>Note that this description does not say what the structure of a
-$Thing$ is, only how it may be described in terms of its time interval
+$Thing$ is, only how it may be described in terms of its lifetime
and attribute values. A thing could be a record of fixed
attribute values; it could be a bear; it could be the Royal Society;
it could be a transcendental number like $\pi$. All that matters from
@@ -1594,6 +1594,8 @@
</p>
<div class="component" id="activities">
<ol><li>A set $Activities \subseteq Objects$ of activities.</li>
+ <li>Functions $startTime : Activities \to Times$ and $endTime
+ :Activities \to Times$ giving the start and end time of each activity.</li>
<li> Activities are disjoint from Entities: $Entities\cap Activities
= \emptyset$.</li>
</ol>
@@ -1641,7 +1643,7 @@
</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
+<li>An associated function $influenced : Influences \to
Objects \times Objects$ giving the source and target of each influence.</li>
</ol>
</div>
@@ -1698,7 +1700,7 @@
</p>
<div class="component" id="attributions">
<p>A set $Attributions \subseteq Influences$ with associated
- function $attributedTo : Attributions \toEntities \times Agents$.
+ function $attributedTo : Attributions \to Entities \times Agents$.
</p>
</div>
@@ -1710,7 +1712,7 @@
</p>
<div class="component" id="communications">
<p>A set $Communications \subseteq Influences$ with associated
- function $communicatedBy : Communications \to Generations \times Usages$.
+ function $communicatedBy : Communications \to Activities \times Activities$.
</p>
</div>
@@ -1723,7 +1725,7 @@
</p>
<div class="component" id="delegations">
<p>A set $Delegations \subseteq Influences$ and associated function
- $actsFor : Delegations \to Agents \times Agents \times Activities$
+ $actedFor : Delegations \to Agents \times Agents \times Activities$
</p>
</div>
@@ -1769,104 +1771,6 @@
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
- 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>
-
-
-<!--
-<section>
-
-<h3> Relations </h3>
-
-<h4> Simple relations </h4>
-<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.
-</li><li> A relation $Invalidated \subseteq Events \times Entities$
-saying when an event invalidated an entity. An event can invalidate
-at most one entity, and if $(evt,e)\in Invalidated$ then
-$max(lifetime(e)) = time(evt)$ and $type(evt) = invalidation$ must
-hold.
-<li>A relation $Start \subseteq Events \times Activities
-\times Entities$ indicating that an activity started another.</li>
-<li>A relation End \subseteq Events \times Activities
-\times Entities$ indicating that an activity ended another.</li>
-
-</li><li> A relation $EventActivity \subseteq Events \times Activities$ associating activities with events, such that $(act,evt) \in EventActivity$ implies $time(evt) \in lifetime(act)$.
-</li><li> A relation $AssociatedWith \subseteq Associations \times Agents \times Activities \times Plans_\bot$ indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan.
-</li><li> A relation $ActsFor \subseteq Delegations \times Agents \times Agents \times Activities$ indicating when one agent acts on behalf of another with respect to a given activity.
-</li>
-<li>A relation $Influence \subseteq Events \times Objects \times
-Objects$ indicating when one object influences another.</ol>
-
-<div class="note">
- TODO: Simplify/regularize event relations; get rid of EventActivity
- relation; add functions defining sets of events associated with
- entity, activity or agent
- </div>
-
- <div class="note">
- TODO: Additional axioms concerning the relations; for example:
- clarify that every Event is associated with an Activity and
- Entity; ensure that for attribution the agent's lifetime must
- start before that of the entity. OR: do not specify these things
- but let them fall out naturally by the requirement that the model
- satisfies all of the FO axioms.
- </div>
-
-
-<section>
-<h4> Derivation paths and DerivedFrom </h4>
-
-<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$$
-
-<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 (Events \cdot Activities \cdot
-Events \cdot Entities)^+$$
-<p>with the constraints that for each derivation path:
-</p>
-<ul>
-<li>for each substring $ent\cdot g \cdot act$ we have $(g,ent) \in Generated$ and $(g,act) \in EventActivity$, and
-</li>
-<li>for each substring $act \cdot u \cdot ent$ we have $(u,ent) \in Used$ and $(u,act) \in EventActivity$.
-</li>
-</ul>
-<p>Each derivation $d \in Derivations$ has an associated derivation path. We link each derivation to an associated derivation path using the
-function $derivationPath : Derivations \to
-DerivationPaths$. </p>
-
-<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 path, identified by different
derivations $d \in Derivations$.
</p>
@@ -1881,12 +1785,125 @@
</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>
+ steps is to reflect that $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ formulas can
+ represent multiple derivation steps. However, there is no way to
+ express a multi-step derivation path in PROV: any valid PROV
+ instance turns out to have a model in which all derivation paths are
+ one-step.</p></div>
</section>
</section>
--->
+</section>
+
+ <section>
+ <h3>Additional axioms</h3>
+
+ <p> Above we have stated some properties of the components. We
+ impose some additional properties that relate several components, as
+ follows:</p>
+
+ <div class="component" id="axioms">
+
+ <ol>
+ <li id="axiom1">
+ If $generated(g) = (e,a_1)$ and $used(u) = (a_2,e)$ then there
+ exists $c \in Communications$ such that $communicatedBy(c) = (a_2,a_1)$.
+ </li>
+ <li id="axiom2">
+ If $started(start) = (a_2,e,a_1)$ then there exists $gen$ such
+ that $generated(gen) = (e,a_1)$.
+ </li>
+ <li id="axiom3">
+ If $ended(end) = (a_2,e,a_1)$ then there exists $gen$ such
+ that $generated(gen) = (e,a_1)$.
+ </li>
+ <li id="axiom4">
+ If $d \in Derivations$ and $prov:Revision \in
+ value(d,prov:type)$ and $derivationPath(deriv) = e_2 \cdot w \cdot
+ e_1$ then $thingOf(e_1) = thingOf(e_2)$.
+ </li>
+ <li id="axiom5">
+ If $attributedTo(att) = (e,ag)$ then there exist $gen$ and $assoc$
+ such that $generated(gen) = (e,a)$ and $associatedWith(assoc) = (a,ag)$.
+ </li>
+ <li id="axiom6">
+ If $actedFor(deleg) = (ag_2,ag_1,act)$ then there exist
+ $assoc_1,assoc_2,pl_1,pl_2$ such that $associatedWith(assoc_1) = (act,ag_1,pl_1)$
+ and $associatedWith(assoc_2) = (act,ag_2,pl_2)$.
+ </li>
+ <li id="axiom7">
+ If $generated(id) = (e,a)$ then $influenced(id) = (e,a)$.
+ </li>
+ <li id="axiom8">
+ If $used(id) = (e,a)$ then $influenced(id) = (e,a)$.
+ </li>
+ <li id="axiom9">
+ If $communicatedBy(id) = (a_2,a_1)$ then $influenced(id) = (a_2,a_1)$.
+ </li>
+ <li id="axiom10">
+ If $started(id) = (a_2,e,a_1)$ then $influenced(id) = (a_2,e)$.
+ </li>
+ <li id="axiom11">
+ If $ended(id) = (a_2,e,a_1)$ then $influenced(id) = (a_2,e)$.
+ </li>
+ <li id="axiom12">
+ If $invalidated(id) = (e,a)$ then $influenced(id) = (e,a)$.
+ </li>
+ <li id="axiom13">
+ If $derivationPath(id) = e_2 \cdot w \cdot e_1$ then
+ $influenced(id) = (e_2,e_1)$.
+ </li>
+ <li id="axiom14">
+ If $attributedTo(id) = (e,ag)$ then $influenced(id) = (e,ag)$.
+ </li>
+ <li id="axiom15">
+ If $associatedWith(id) = (a,ag,pl)$ then $influenced(id) = (a,ag)$.
+ </li>
+ <li id="axiom16">
+ If $actedFor(id) = (ag_2,ag_1)$ then $influenced(id) = (ag_2,ag_1)$.
+ </li>
+ <li id="axiom17">
+ If $generate(gen) = (e,a) = generated(gen')$ then $gen = gen'$.
+ </li>
+ <li id="axiom18">
+ If $invalidated(inv) = (e,a) = invalidated(inv')$ then $inv=inv'$.
+ </li>
+ <li id="axiom19">
+ If $started(st) = (a,e_1,a')$ and $started(st') = (a,e_2,a')$ then $st=st'$.
+ </li>
+ <li id="axiom20">
+ If $ended(end) = (a,e_1,a')$ and $ended(end') = (a,e_2,a')$ then $end=end'$.
+ </li>
+ <li id="axiom21">
+ If $started(st) = (a,e)$ then $st \preceq evt$ for all $evt \in events(a)$.
+ </li>
+ <li id="axiom22">
+ If $ended(end) = (a,e,a') $ then $evt \preceq end$ for all $evt \in events(a)$.
+ </li>
+ <li id="axiom23">
+ If $generated(gen) = (e,a)$ then $gen \preceq evt$ for all $evt \in events(e)$.
+ </li>
+ <li id="axiom24">
+ If $invalidated(inv) = (e,a)$ then $evt\preceq inv$ for all $evt \in events(e)$.
+ </li>
+ <li id="axiom25">
+ For any derivation $deriv$, with path $derivationPath(deriv) = w$,
+ if $e_2 \cdot g \cdot a \cdot u \cdot e_1 $ is a substring of $w$
+ where $e_1,e_2 \in Entities$, $g \in Generations$, $u \in Usages$
+ and $a \in Activities$ then $u \preceq g$.
+ </li>
+ <li id="axiom26">
+ For any derivation $deriv$, with path $derivationPath(deriv) = e_2
+ \cdot w \cdot e_1$, if $generated(gen_1) = (e_1,a_1)$ and
+ $generated(gen_2) = (e_2,a_2)$ then $gen_1 \prec gen_2$.
+ </li>
+ </ol>
+</div>
+
+ <p>These properties are called <em>axioms</em>, and they are
+ needed to ensure that the PROV-CONSTRAINTS inferences and
+ constraints hold in all structures.</p>
+ </section>
<section>
<h3> Putting it all together </h3>
@@ -1898,6 +1915,9 @@
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.
</p>
+
+
+
<div class="note">
TODO: Highlight the distinctive vs obvious/routine features.
</div>
@@ -1914,6 +1934,7 @@
</p>
</section>
+
</section>
<section id="semantics">
<h2> Semantics </h2>
@@ -1944,7 +1965,7 @@
<li>$W,\rho \models \phi \wedge \psi$ holds if and only if $W,\rho \models
\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>
+ or $W,\rho \models \psi$.</li>
<li>$W,\rho \models \phi \Rightarrow \psi$ holds if $W,\rho \models \phi$
implies $W,\rho \models \psi$.</li>
<li>$W,\rho \models \exists x. \phi$ holds if there exists some $obj \in
@@ -2003,6 +2024,8 @@
<ol>
<li>[WF] $id$ denotes an entity $ent = \rho(id) \in Entities$
</li>
+<li>There exists $gen,a$ such that $generated(gen) = (e,a)$.</li>
+<li>There exists $inv,a'$ such that $invalidated(inv) = (e,a)$.</li>
<li>the attributes match: $match(W,ent, attrs)$.
</li>
</ol>
@@ -2042,10 +2065,13 @@
<ol>
<li>[WF] The identifier $id$ maps to an activity $act = \rho(id) \in Activities$
</li>
-<li>$\rho(st) \in Times$ is the activity's start time, that is: $min(lifetime(id)) = \rho(st)$
+<li>$\rho(st) \in Times$ is the activity's start time, that is:
+$startTime(id) = \rho(st)$
</li>
-<li>$\rho(et)$ is the activity's end time, that is: $max(lifetime(id)) = \rho(et)$
+<li>$\rho(et)$ is the activity's end time, that is: $endTime(id) = \rho(et)$
</li>
+<li>There exists $start,e,a$ such that $started(start) = (act,e,a)$.</li>
+<li>There exists $end,e',a'$ such that $ended(end) = (act,e',a')$.</li>
<li>The attributes match: $match(W,act,attrs)$.
</li>
</ol>
@@ -2168,7 +2194,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. $$associatedWith(assoc) = (agent,act,plan)$.
+<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>
@@ -2204,7 +2230,7 @@
</li>
<li>[WF] $a_1$ denotes an activity $act_1 = \rho(a_1) \in Activities$.
</li>
-<li>The event happened at the start of $act_2$, that is, $\rho(t) = min(lifetime(act_2)) = time(evt)$.
+<li>The event happened at the start of $act_2$, that is, $\rho(t) = startTime(act_2) = time(evt)$.
</li>
<li> The activity $act_1$ started $act_2$ via entity $ent$: that is,
$started(evt) = (act_2,ent,act_1)$.</li>
@@ -2226,7 +2252,7 @@
<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 happened at the end of $act_2$, that is, $\rho(t) = max(lifetime(act_2)) = time(evt)$.</li>
+<li>The event happened at the end of $act_2$, that is, $\rho(t) = endTime(act_2) = time(evt)$.</li>
<li> The activity $act_1$ ended $act_2$ via entity $ent$: that is,
$ended(evt) = (act_2,ent,act_1)$.</li>
<li>The attributes match: $match(W,evt,attrs)$.</li>
@@ -2255,7 +2281,7 @@
<li>The entity was attributed to the agent, i.e. $attributedTo(assoc)
= (ent,agent)$.
</li>
-<li>The attributes match: $match(W,evt,attrs)$.
+<li>The attributes match: $match(W,assoc,attrs)$.
</li></ol>
</div>
</section>
@@ -2263,20 +2289,21 @@
<section>
<h4>Communication</h4>
-<p>A communication formula </p>
+<p>A communication formula $wasInformedBy(id,a_2,a_2,attrs)$ is
+interpreted as follows: </p>
<div class="semantics" id="communication-semantics">
<p>
$W,\rho \models wasInformedBy(id,a_2,a_1,attrs)$
holds if and only if:
</p>
<ol>
-<li>[WF] $id$ denotes an communication $comm = \rho(id) \in Communications$.
+<li>[WF] $id$ denotes a communication $comm = \rho(id) \in Communications$.
</li>
<li>[WF] $a_1,a_2$ denote activities $act_1 = \rho(a_1) \in
Activities, act_2 = \rho(a_2)\in Activities$.
</li>
<li>There exist $gen,use,ent$ such that $communicatedBy(comm) =
-(gen,use)$ and $generated(gen) = (ent,act_1)$ and $used(use) = (act_2,ent)$.
+(act_2,act_1)$ and $generated(gen) = (ent,act_1)$ and $used(use) = (act_2,ent)$.
</li>
<li>The attributes match: $match(W,comm,attrs)$.
</li></ol>
@@ -2294,7 +2321,7 @@
<p>
$W,\rho \models actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes an association $deleg=\rho(id) \in Delegations$.
+<li>[WF] $id$ denotes a delegation $deleg=\rho(id) \in Delegations$.
</li>
<li>[WF] $a$ denotes an activity $act=\rho(a) \in Activities$.
</li>
@@ -2303,7 +2330,7 @@
<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>The attributes match: $match(W,deleg,attrs)$.
</li></ol></div>
</section>
@@ -2410,7 +2437,11 @@
</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)$.
+<li>For each attribute $attr$ we have $value(ent_1,attr) \supseteq value(ent_2,attr)$.</li>
+<li>At least one of these inclusions is strict: that is, either
+ $lifetime(ent_1) \subsetneq lifetime(ent_2)$ or for some $attr$ we
+ value(ent_1,attr) \supsetneq value(ent_2,attr)$.
+</li>
</ol>
</div>
@@ -2489,12 +2520,13 @@
<section>
<h4>Precedes and Strictly Precedes</h4>
<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
- \strictlyPrecedes y$) is similar, only $x$ must take place strictly before $y$.</p>
+ place before (or simultaneously with) another. Its meaning is
+ defined in terms of the quasiordering on events specified by
+ $\preceq$. The semantics of strictly precedes ($x
+ \strictlyPrecedes y$) is similar, only $x$ must take place strictly
+ before $y$. It is interpreted as $\prec$, which we recall is
+ defined from $\preceq$ as $x \prec y \iff x \preceq y \text{ and } y
+ \not\preceq x$.</p>
<div class="semantics" id="precedes-semantics">
<ol>
<li>$W,\rho \models x \precedes y$ holds if and only if
@@ -2516,7 +2548,8 @@
</pre>
<p>This instance is valid, and must satisfy precedence constraints
$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.
+ imply anything about the relative orderings of the associated
+ times, or vice versa.
</p>
</div>
@@ -2528,7 +2561,7 @@
be the null value $\bot$. The symbol $-$ always denotes the null
value (i.e. $\rho(-) = \bot$).
<div class="semantics" id="notNull-semantics">
- <p>$W,\rho\models notNull(e)$ holds if and only if $e \neq
+ <p>$W,\rho\models notNull(e)$ holds if and only if $\rho(e) \neq
\bot$.
</p>
</div>
@@ -2561,7 +2594,6 @@
</section>
</section>
</section>
- </section>
<section id="theory">
<h2> Inferences and Constraints </h2>
@@ -2585,14 +2617,21 @@
\quad\Rightarrow
\exists e,gen,t_1,use,t_2.~wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge used(use,a_2,e,t_2,[])
\end{array}$</div>
+
+<div class="proof">
+<p> This follows immediately from the semantics of $wasInformedBy$.</p>
+ </div>
<div class="inference" number="6" id="generation-use-communication-inference">$\begin{array}[t]{l}
-\forall gen,e,a_1,t_1,attrs_1,id_2,a_2,t_2,attrs_2.~
+\forall gen,e,a_1,t_1,attrs_1,use,a_2,t_2,attrs_2.~
\\
-\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(id_2,a_2,e,t_2,attrs_2)
+\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(use,a_2,e,t_2,attrs_2)
\\
\quad\Rightarrow
\exists id.~wasInformedBy(id,a_2,a_1,[])
\end{array}$</div>
+<div class="proof">
+<p> This follows from the semantics of $wasInformedBy$ and <a href="#axiom1">Axiom 1</a>.</p>
+ </div>
<div class="inference" number="7" id="entity-generation-invalidation-inference">$\begin{array}[t]{l}
\forall e,attrs.~
\\
@@ -2601,6 +2640,12 @@
\quad\Rightarrow
\exists gen,a_1,t_1,inv,a_2,t_2.~wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge wasInvalidatedBy(inv,e,a_2,t_2,[])
\end{array}$</div>
+
+<div class="proof">
+ <p> This follows from the semantics of entity formulas, specifically
+ the requirement that generation and invalidation events exist for
+ the entity.</p>
+ </div>
<div class="inference" number="8" id="activity-start-end-inference">$\begin{array}[t]{l}
\forall a,t_1,t_2,attrs.~
\\
@@ -2609,6 +2654,14 @@
\quad\Rightarrow
\exists start,e_1,a_1,end,a_2,e_2.~wasStartedBy(start,a,e_1,a_1,t_1,[]) \wedge wasEndedBy(end,a,e_2,a_2,t_2,[])
\end{array}$</div>
+
+<div class="proof">
+ <p> This follows from the semantics of activity formulas, specifically
+ the requirement that start and end events exist for
+ the activity.</p>
+ </div>
+
+
<div class="inference" number="9" id="wasStartedBy-inference">$\begin{array}[t]{l}
\forall id,a,e_1,a_1,t,attrs.~
\\
@@ -2617,6 +2670,10 @@
\quad\Rightarrow
\exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom2">Axiom 2</a>.</p>
+ </div>
<div class="inference" number="10" id="wasEndedBy-inference">$\begin{array}[t]{l}
\forall id,a,e_1,a_1,t,attrs.~
\\
@@ -2625,6 +2682,10 @@
\quad\Rightarrow
\exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom3">Axiom 3</a>.</p>
+ </div>
<div class="inference" number="11"
id="derivation-generation-use-inference">
$\begin{array}[t]{l}
@@ -2635,6 +2696,11 @@
\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="proof">
+ <p> This follows from the semantics of precise derivation steps.</p>
+ </div>
+
<div class="inference" number="12"
id="revision-is-alternate-inference">
$\begin{array}[t]{l}
@@ -2645,6 +2711,10 @@
\quad\Rightarrow
alternateOf(e_2,e_1)
\end{array}$</div>
+<div class="proof">
+ <p> This follows from the semantics of derivation steps (precise or
+ imprecise) and <a href="#axiom4">Axiom 4</a>.</p>
+ </div>
<div class="inference" number="13" id="attribution-inference">$\begin{array}[t]{l}
\forall att,e,ag,attrs.~
\\
@@ -2653,6 +2723,11 @@
\quad\Rightarrow
\exists a,t,gen,assoc,pl.~wasGeneratedBy(gen,e,a,t,[]) \wedge wasAssociatedWith(assoc,a,ag,pl,[])
\end{array}$</div>
+<div class="proof">
+ <p>This follows from the semantics of generation, association, and
+ attribution, by <a href="#axiom5">Axiom 5</a></p>
+ </div>
+
<div class="inference" number="14" id="delegation-inference">$\begin{array}[t]{l}
\forall id,ag_1,ag_2,a,attrs.~
\\
@@ -2661,6 +2736,9 @@
\quad\Rightarrow
\exists id_1,pl_1,id_2,pl_2.~wasAssociatedWith(id_1,a,ag_1,pl_1,[]) \wedge wasAssociatedWith(id_2,a,ag_2,pl_2,[])
\end{array}$</div>
+<div class="proof">
+ <p>This follows from the semantics of association and delegation, by <a href="#axiom6">Axiom 6</a></p>
+ </div>
<div class="inference" number="15" id="influence-inference"><ol><li>$\begin{array}[t]{l}
\forall id,e,a,t,attrs.~
\\
@@ -2734,6 +2812,10 @@
\quad\Rightarrow
wasInfluencedBy(id,ag_2,ag_1,attrs)
\end{array}$</li></ol></div>
+
+<div class="proof">
+ <p>This follows via <a href="#axiom7">Axioms 7</a> through <a href="#axiom16">16</a>.
+ </div>
<div class="inference" number="16" id="alternate-reflexive">$\begin{array}[t]{l}
\forall e.~
\\
@@ -2743,8 +2825,8 @@
alternateOf(e,e)
\end{array}$</div>
<div class="proof">
- <p> Suppose $ent = \rho(e)$. Clearly $e \in Entities$ and
- $thingOf(e) = thingOf(e)$, so $W,\rho \models alternateOf(e,e)$.</p>
+ <p> Suppose $ent = \rho(e)$. Clearly $ent \in Entities$ and
+ $thingOf(ent) = thingOf(ent)$, so $W,\rho \models alternateOf(e,e)$.</p>
</div>
<div class="inference" number="17" id="alternate-transitive">$\begin{array}[t]{l}
\forall e_1,e_2,e_3.~
@@ -2784,7 +2866,6 @@
\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 =
@@ -2792,11 +2873,12 @@
lifetime(e_3)$. Moreover,
$value(obj_2,attr) \supseteq value(obj_3,attr)$, and similarly
$value(obj_1,attr)\supseteq value(obj_2,attr)$ so $value(obj_1,attr)
- \supseteq value(obj_3,attr)$. (TODO:
- How do we know $e_3 \neq e_1$? Need strict ordering on entities in semantics.)
+ \supseteq value(obj_3,attr)$. Finally, at least one of the
+ inclusions between $obj_1$ and $obj_2$ is strict, so the same is the
+ case for $obj_1$ and $obj_3$.
</p>
</div>
--->
+
<div class="inference" number="20" id="specialization-alternate-inference">$\begin{array}[t]{l}
\forall e_1,e_2.~
@@ -2842,17 +2924,18 @@
\Rightarrow entity(id,attrs_1\cup attrs_2)$</li>
<li>$\forall
id,t_1,t_1',t_2,t_2',attrs_1,attrs_2.~ activity(id,t_1,t_2,attrs_1)
- \wedge activity(idt_1',t_2',attrs_2) \Rightarrow
+ \wedge activity(id,t_1',t_2',attrs_2) \Rightarrow
activity(id,t_1,t_2,attrs_1\cup attrs_2) \wedge t_1=t_1' \wedge t_2=t_2'$</li>
<li>$\forall
id,attrs_1,attrs_2. agent(id,attrs_1) \wedge agent(id,attrs_2)
\Rightarrow agent(id,attrs_1\cup attrs_2)$.</li></ol></div>
<div class="proof">
<p> These properties follow immediately from the definitions of the
- semantics of the respective assertions.</p>
+ semantics of the respective assertions, because functions are used
+ for the underlying data.</p>
</div>
<div class="constraint" number="23" id="key-properties">
- <ol><li>$\begin{array}[t]{l}
+ <ol><li><br />$\begin{array}[t]{l}
\forall
id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\
wasGeneratedBy(id,e,a,t,attrs)
@@ -2860,69 +2943,61 @@
\quad \Rightarrow
wasGeneratedBy(id,e,a,t,attrs_1 \cup attrs_2) \wedge e=e' \wedge
a=a' \wedge t = t'\end{array}$</li>
- <li> $\begin{array}[t]{l}\forall
+ <li><br /> $\begin{array}[t]{l}\forall
id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\used(id,a,e,t,attrs)
\wedge used(id,a',e',t',attrs_2)\\ \quad \Rightarrow
used(id,a,e',t,attrs_1 \cup attrs_2) \wedge e=e' \wedge
a=a' \wedge t = t'
\end{array}$</li>
- <li> $\begin{array}[t]{l}\forall
+ <li><br /> $\begin{array}[t]{l}\forall
id,a_1,a_2,a_1',a_2',attrs_1,attrs_2.~ \\wasInformedBy(id,a_1,a_2,attrs)
\wedge wasInformedBy(id,a_1',a_2',attrs_2)\\ \Rightarrow
wasInformedBy(id,a_1,a_2,attrs_1 \cup attrs_2) \wedge a_1=a_1'
\wedge a_2=a_2'
\end{array}$</li>
- <li> $\begin{array}[t]{l}\forall
+ <li><br /> $\begin{array}[t]{l}\forall
id,e,e'a_1,a_2,a_1',a_2',t,t',attrs_1,attrs_2.~ \\wasStartedBy(id,a_2,e,a_1,t,attrs_1)
\wedge wasStartedBy(id,a_2',e',a_1',t',attrs_2)\\ \Rightarrow
wasStartedBy(id,a_2,e,a_1,t,attrs_1 \cup attrs_2) \wedge a_1=a_1'
\wedge e=e' \wedge
a_2=a_2' \wedge t = t'
\end{array}$</li>
- <li>$\begin{array}[t]{l}\forall
+ <li><br />$\begin{array}[t]{l}\forall
id,e,e'a_1,a_2,a_1',a_2',t,t',attrs_1,attrs_2.~ \\wasEndedBy(id,a_2,e,a_1,t,attrs_1)
\wedge wasEndedBy(id,a_2',e',a_1',t',attrs_2)\\ \Rightarrow
wasEndedBy(id,a_2,e,a_1,t,attrs_1 \cup attrs_2) \wedge a_1=a_1'
\wedge e=e' \wedge
a_2=a_2' \wedge t = t'
\end{array}$</li>
- <li>$\begin{array}[t]{l}\forall
+ <li><br />$\begin{array}[t]{l}\forall
id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\wasInvalidatedBy(id,e,a,t,attrs_1)
\wedge wasInvalidatedBy(id,e',a',t',attrs_2)\\ \Rightarrow
wasInvalidatedBy(id,e,a,t,attrs_1 \cup attrs_2) \wedge e=e' \wedge
a=a' \wedge t = t'
\end{array}$</li>
- <li>The identifier field $id$ is a <span
- class="conditional">KEY</span> for the
- $wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)$ statement. $\begin{array}[t]{l}\forall
+ <li><br />$\begin{array}[t]{l}\forall
id,e_1,e_1',e_2,e_2',a,a',g,g',u,u',attrs_1,attrs_2.~ \\wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs_1)
\wedge wasDerivedFrom(id,e_2',e_1',a',g_2',u_1',attrs_2)\\ \Rightarrow
wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs_1 \cup attrs_2) \wedge e_1=e_1'\wedge e_2=e_2'\wedge a=a'\wedge g=g'\wedge u=u'
\end{array}$</li>
- <li>The identifier field $id$ is a <span
- class="conditional">KEY</span> for the
- $wasAttributedTo(id,e,ag,attrs)$ statement. $\begin{array}[t]{l}\forall
+ <li><br /> $\begin{array}[t]{l}\forall
id,e,e',ag,ag',attrs_1,attrs_2.~ \\wasAttributedTo(id,e,ag,attrs_1)
\wedge wasAttributedTo(id,e',ag',attrs_2)\\ \Rightarrow
wasAttributedTo(id,e,ag,attrs_1 \cup attrs_2) \wedge e=e' \wedge ag = ag'
\end{array}$</li>
- <li>The identifier field $id$ is a <span
- class="conditional">KEY</span> for the
- $wasAssociatedWith(id,a,ag,pl,attrs)$ statement. $\begin{array}[t]{l}\forall
+ <li> <br />$\begin{array}[t]{l}\forall
id,a,a',ag,ag',pl,pl',attrs_1,attrs_2.~ \\wasAssociatedWith(id,a,ag,pl,attrs_1)
\wedge wasAssociatedWith(id,a',ag',pl',attrs_2)\\ \Rightarrow
wasAssociatedWith(id,a,ag,pl,attrs_1 \cup attrs_2) \wedge a=a'
\wedge ag=ag' \wedge pl=pl'
\end{array}$</li>
- <li>The identifier field $id$ is a <span
- class="conditional">KEY</span> for the
- $actedOnBehalfOf(id,ag_2,ag_1,a,attrs)$ statement. $\begin{array}[t]{l}\forall
+ <li><br />$\begin{array}[t]{l}\forall
id,ag_1,ag_1',ag_2,ag_2',a,a',attrs_1,attrs_2.~ \\actedOnBehalfOf(id,ag_2,ag_1,a,attrs_1)
\wedge actedOnBehalfOf(id,ag_2',ag_1',a',attrs_2)\\ \Rightarrow
actedOnBehalfOf(id,ag_2,ag_1,a,attrs_1 \cup attrs_2) \wedge
ag_1=ag_1' \wedge ag_2 = ag_2' \wedge a = a'
\end{array}$</li>
- <li>$\begin{array}[t]{l}\forall
+ <li><br />$\begin{array}[t]{l}\forall
id,o_1,o_2,o_1',o_2',attrs_1,attrs_2.~ \\wasInfluencedBy(id,o_2',o_1',attrs_1)
\wedge wasInfluencedBy(id,o_2',o_1',attrs_2)\\ \Rightarrow
wasInfluencedBy(id,o_2,o_1,attrs_1 \cup attrs_2) \wedge o_1=o_1'
@@ -2931,7 +3006,8 @@
</div>
<div class="proof">
<p> These properties follow immediately from the definitions of the
- semantics of the respective assertions.</p>
+ semantics of the respective assertions, again because functions are
+ used for the underlying data.</p>
</div>
<div class="constraint" number="24" id="unique-generation">$\begin{array}[t]{l}
\forall gen_1,gen_2,e,a,t_1,t_2,attrs_1,attrs_2.~
@@ -2941,6 +3017,11 @@
\quad\Rightarrow
gen_1 = gen_2
\end{array}$</div>
+<div class="proof">
+ <p>
+ This follows from <a href="#axiom17">Axiom 17</a>.
+ </p>
+ </div>
<div class="constraint" number="25" id="unique-invalidation">$\begin{array}[t]{l}
\forall inv_1,inv_2,e,a,t_1,t_2,attrs_1,attrs_2.~
\\
@@ -2949,6 +3030,11 @@
\quad\Rightarrow
inv_1 = inv_2
\end{array}$</div>
+<div class="proof">
+ <p>
+ This follows from <a href="#axiom17">Axiom 18</a>.
+ </p>
+ </div>
<div class="constraint" number="26" id="unique-wasStartedBy">$\begin{array}[t]{l}
\forall start_1,start_2,a,e_1,e_2,a_0,t_1,t_2,attrs_1,attrs_2.~
\\
@@ -2957,6 +3043,12 @@
\quad\Rightarrow
start_1 = start_2
\end{array}$</div>
+<div class="proof">
+ <p>
+ This follows from <a href="#axiom17">Axiom 19</a>.
+ </p>
+ </div>
+
<div class="constraint" number="27" id="unique-wasEndedBy">$\begin{array}[t]{l}
\forall end_1,end_2,a,e_1,e_2,a_0,t_1,t_2,attrs_1,attrs_2.~
\\
@@ -2965,6 +3057,11 @@
\quad\Rightarrow
end_1 = end_2
\end{array}$</div>
+<div class="proof">
+ <p>
+ This follows from <a href="#axiom17">Axiom 20</a>.
+ </p>
+ </div>
<div class="constraint" number="28" id="unique-startTime">$\begin{array}[t]{l}
\forall start,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1.~
\\
@@ -2973,6 +3070,12 @@
\quad\Rightarrow
t_1 = t
\end{array}$</div>
+<div class="proof">
+ <p>
+ This follows from the semantics of $wasStartedBy$, since the start times
+ must both match that of the activity.
+ </p>
+ </div>
<div class="constraint" number="29" id="unique-endTime">$\begin{array}[t]{l}
\forall end,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1.~
\\
@@ -2981,6 +3084,12 @@
\quad\Rightarrow
t_2 = t
\end{array}$</div>
+<div class="proof">
+ <p>
+ This follows from the semantics of $wasEndedBy$, since the end times
+ must both match that of the activity.
+ </p>
+ </div>
</section>
<section>
@@ -2995,6 +3104,11 @@
\quad\Rightarrow
start \precedes end
\end{array}$</div>
+<div class="proof">
+ <p>This follows from <a href="#axiom21">Axiom 21</a>.
+ </p>
+ </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.~
\\
@@ -3003,6 +3117,11 @@
\quad\Rightarrow
start_1 \precedes start_2
\end{array}$</div>
+<div class="proof">
+ <p>This follows from <a href="#axiom21">Axiom 21</a>.
+ </p>
+ </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.~
\\
@@ -3011,6 +3130,11 @@
\quad\Rightarrow
end_1 \precedes end_2
\end{array}$</div>
+<div class="proof">
+ <p>This follows from <a href="#axiom22">Axiom 22</a>.
+ </p>
+ </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.~
\\
@@ -3026,6 +3150,12 @@
\quad\Rightarrow
use \precedes end
\end{array}$</li></ol></div>
+<div class="proof">
+ <p>Part 1 follows from <a href="#axiom21">Axiom 21</a> and part 2
+ follows from <a href="#axiom22">Axiom 22</a>.
+ </p>
+ </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.~
\\
@@ -3041,6 +3171,12 @@
\quad\Rightarrow
gen \precedes end
\end{array}$</li></ol></div>
+<div class="proof">
+ <p>Part 1 follows from <a href="#axiom21">Axiom 21</a> and part 2
+ follows from <a href="#axiom22">Axiom 22</a>.
+ </p>
+ </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.~
\\
@@ -3049,6 +3185,14 @@
\quad\Rightarrow
start \precedes end
\end{array}$</div>
+<div class="proof">
+ <p>This follows from the semantics of $wasInformedBy$ and the
+ previous two constraints, because $wasInformedBy$ implies the
+ existence of intermediate generation and usage events linking $a_1$
+ and $a_2$.
+ </p>
+ </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.~
\\
@@ -3057,7 +3201,13 @@
\quad\Rightarrow
gen \precedes inv
\end{array}$</div>
-<div class="constraint" number="37" id="generation-precedes-usage">$\begin{array}[t]{l}
+
+<div class="proof">
+ <p>This follows from <a href="#axiom22">Axiom 22</a>.
+ </p>
+ </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.~
\\
\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(use,a_2,e,t_2,attrs_2)
@@ -3065,6 +3215,12 @@
\quad\Rightarrow
gen \precedes use
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom 23">Axiom 23</a>.
+ </p>
+ </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.~
\\
@@ -3073,6 +3229,12 @@
\quad\Rightarrow
use \precedes inv
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom24">Axiom 24</a>.
+ </p>
+ </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.~
\\
@@ -3081,6 +3243,12 @@
\quad\Rightarrow
gen_1 \precedes gen_2
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom23">Axiom 23</a>.
+ </p>
+ </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.~
\\
@@ -3089,8 +3257,14 @@
\quad\Rightarrow
inv_1 \precedes inv_2
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom24">Axiom 24</a>.
+ </p>
+ </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}
+ id="derivation-usage-generation-ordering">$\begin{array}[t]{l}
\forall d,e_1,e_2,a,gen_2,use_1,attrs.~
\\
\qquad notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(d,e_2,e_1,a,gen_2,use_1,attrs)
@@ -3098,7 +3272,13 @@
\quad\Rightarrow
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}
+
+<div class="proof">
+ <p>This follows from <a href="#axiom25">Axiom 25</a>.
+ </p>
+ </div>
+
+<div class="constraint" number="42" id="derivation-generation-generation-ordering">$\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.~
\\
\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)
@@ -3106,6 +3286,12 @@
\quad\Rightarrow
gen_1 \strictlyPrecedes gen_2
\end{array}$</div>
+
+<div class="proof">
+ <p>This follows from <a href="#axiom25">Axiom 26</a>.
+ </p>
+ </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.~
\\
@@ -3121,6 +3307,13 @@
\quad\Rightarrow
start \precedes inv
\end{array}$</li></ol></div>
+
+<div class="proof">
+ <p>Part 1 follows from <a href="#axiom23">Axiom 23</a>. Part 2
+ follows from <a href="#axiom24">Axiom 24</a>.
+ </p>
+ </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.~
\\
@@ -3136,6 +3329,13 @@
\quad\Rightarrow
end \precedes inv
\end{array}$</li></ol></div>
+
+<div class="proof">
+ <p>Part 1 follows from <a href="#axiom23">Axiom 23</a>. Part 2
+ follows from <a href="#axiom24">Axiom 24</a>.
+ </p>
+ </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.~
\\
@@ -3144,7 +3344,14 @@
\quad\Rightarrow
gen_1 \precedes gen_2
\end{array}$</div>
-<div class="constraint" number="46" id="specialization-invalidation-ordering">$\begin{array}[t]{l}
+
+
+<div class="proof">
+ <p> ???
+ </p>
+ </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.~
\\
\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)
@@ -3152,6 +3359,12 @@
\quad\Rightarrow
inv_1 \precedes inv_2
\end{array}$</div>
+
+<div class="proof">
+ <p> ???
+ </p>
+ </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.~
\\
@@ -3181,6 +3394,12 @@
\quad\Rightarrow
start_1 \precedes end_2
\end{array}$</li></ol></div>
+
+<div class="proof">
+ <p>TODO - arbitrary axioms.
+ </p>
+ </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.~
\\
@@ -3196,6 +3415,12 @@
\quad\Rightarrow
start_1 \precedes gen_2
\end{array}$</li></ol></div>
+
+<div class="proof">
+ <p>TODO - arbitrary axioms.
+ </p>
+ </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.~
\\
@@ -3212,6 +3437,12 @@
start_1 \precedes end_2
\end{array}$</li></ol></div>
+<div class="proof">
+ <p>TODO - arbitrary axioms.
+ </p>
+ </div>
+
+
</section>
<section>
@@ -3461,16 +3692,21 @@
<section id="soundness-completeness">
<h2>Soundness and Completeness</h2>
-<section id="soundness">
- <h3>Soundness</h3>
-
-<p>Above we have presented arguments for the soundness of the
+
+ <p>Above we have presented arguments for the soundness of the
constraints and inferences with respect to the naive semantics.
Here, we relate the notions of <dfn>validity</dfn> and <dfn>normal
form</dfn> defined in PROV-CONSTRAINTS to the semantics.
-Our main observation is:</p>
+</p>
+
+<section id="soundness">
+ <h3>Soundness</h3>
+
+<p>Our main soundness result is:</p>
<div class="theorem" id="soundness-theorem">
+ <p> Let $W$ be a PROV model, that is, a structure satisfying all of
+ the axioms</p>.
<ol>
<li>If $I$ is an instance and $W \models I$ and $I'$ is obtained from $I$ by applying one
of the PROV inferences, then $W \models I'$.</li>
@@ -3485,7 +3721,7 @@
<p>For part 1, the arguments are as in the previous section. </p>
<p>For
part 2, proceed by induction on a terminating sequence of inference
- or uniqueness constraint steps: if $I$ is in normal form them we are
+ or uniqueness constraint steps: if $I$ is in normal form then we are
done. If $I$ is not in normal form then if an inference is applicable, then use part 1; if a uniqueness constraint is
applicable, then from $W \models I$ the uniqueness constraint cannot
fail on $I$ and $W \models I'$.</p>
@@ -3519,17 +3755,18 @@
\begin{eqnarray*}
Entities &=& \{id \mid entity(id,attrs) \in I\}\\
Plans &=& \{pl \mid wasAssociatedWith(id,ag,act,pl,attrs) \in I, pl
- \neq \bot\}\\
+ \neq -\}\\
Collections &=& \{e \mid memberOf(e',e) \in I\} \\
&\cup& \{e \mid
entity(e,attrs) \in I, prov:type=prov:emptyCollection \in attrs\}\\
Activities &=& \{id \mid activity(id,attrs) \in I\}\\
+ &\cup& \{a_{id} \mid wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\
Agents &=& \{id \mid agent(id,attrs) \in I\}\\
\\
Usages &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\
- Generations &=& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\
- Invalidations &=& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\
+ &\cup& \{u_{id} \mid wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\ Generations &=& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\
+ &\cup& \{g_{id} \mid wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\ Invalidations &=& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\
Starts &=& \{id \mid wasStartedBy(id,a,e,a',t,attrs) \in I\}\\
Ends &=& \{id \mid wasEndedBy(id,a,e,a',t,attrs) \in I\}\\
Events &=& Usages \cup Generations \cup Invalidations \cup Starts
@@ -3549,6 +3786,10 @@
Objects &=& Entities \cup Activities \cup Agents \cup Influences\\
\end{eqnarray*}
\]
+<p>In the definitions of $Activities$, $Generations$, and $Usages$ we
+ write $a_{id}$, $g_{id}$ and $u_{id}$ respectively to indicate
+ additional activities, generations and usages added for imprecise derivations.
+</p>
<p> In addition, to define the set of $Things$, we introduce an
equivalence relation on $Entities$ as follows:
</p>
@@ -3556,14 +3797,13 @@
<p>The fact that this is an equivalence relation follows from the
fact that $I$ is in normal form, since the constraints on
$alternateOf$ ensure that it is an equivalence relation. Recall
- that givne an equivalence relation $\equiv$ on some set $X$, the
+ that given an equivalence relation $\equiv$ on some set $X$, the
<em>equivalence class</em> of $x \in X$ is the set $[x]_\equiv = \{y
\in X \mid x
\equiv y\}$. The <em>quotient</em> of $X$ by an equivalence
relation on $X$ is the set of equivalence classes, $X_\equiv =
\{[x]_\equiv \mid x \in X\}$. Now we
- define the set of $Things$ as equivalence classes of $Entities$
- modulo $\equiv$.</p>
+ define the set of $Things$ as the quotient of $\equiv$-equivalence classes of $Entities$.</p>
\[Things = Entities /_{\equiv} = \{[e]_\equiv \mid e \in Entities\}\]
@@ -3607,6 +3847,20 @@
some of the times are symbolic?</p>
</div>
+<p> The functions $startTime$ and $endTime$ mapping activities to
+ their start and end times is defined as follows:
+ </p>
+ \[\begin{eqnarray*}
+ startTime(id) &=& t_1 \text{ where } activity(a,t_1,t_2,attrs) \in
+ I\\
+ & \text{ or } wasStartedBy(start,a,e,a',t_1,attrs) \in I\\
+ endTime(id) &=& t_2 \text{ where } activity(a,t_1,t_2,attrs) \in
+ I\\
+ & \text{ or } wasEndedBy(end,a,e,a',t_2,attrs) \in I\\
+\]
+ <p>Note that the above definition is deterministic because the start
+ and end times in $activity$ and $wasStartedBy/wasEndedBy$ statements
+ must be equal</p>.
<p> The function $time$ mapping $Events$ to their $Times$ is defined
as follows:
</p>
@@ -3634,9 +3888,8 @@
I\\
attributedTo(id) &=& (e,ag) \text{ where } wasAttributedTo(id,e,ag,attrs) \in I\\
actedFor (id) &=& (ag_2,ag_1,act) \text{ where } actedOnBehalfOf(id,ag_2,ag_1,act,attrs) \in I\\
- communicatedBy(id) &=& (u,g) \text{ where }
- \{wasInformedBy(id,a_2,a_1,attrs),
- wasGeneratedBy(g,e,a_1,t_1,attrs_1), used(u,a_2,e,t_2,attrs_2)\} \subseteq I\\
+ communicatedBy(id) &=& (a_2,a_1) \text{ where }
+ wasInformedBy(id,a_2,a_1,attrs)\in I\\
derivationPath(id) &=& e_2\cdot g \cdot a \cdot u \cdot e_1 \text{ where } wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \in I\\
derivationPath(id) &=& e_2\cdot g_{id} \cdot a_{id} \cdot u_{id} \cdot e_1 \text{ where } wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\\
\end{eqnarray*}
@@ -3646,15 +3899,12 @@
imprecise derivations, we generate additional activities, generations
and usages linking $e_2$ to $e_1$.
</p>
- <div class="note">
- <p>TODO: Communication is slightly weird, as the generation and use
- might not be unique.</p>
- <p> TODO: Derivation is also slightly weird, since there is no
- guarantee that a multi-step derivation exists in the imprecise case
- (and no way to force this). So in the case for imprecise we simply
- generate a new one-step activity/generation/use path. We need to
- add these to $Activities$, $Generations$ and $Usages$ along with
- appropriate function values for $used$ and $generated$.</p>
+ <div class="remark">
+
+ <p> We explicitly add activities, generations, and usages to
+ ensure that we can form derivation paths for imprecise derivation
+ formulas.
+ </p>
</div>
</section>
<section>
@@ -3673,6 +3923,16 @@
\[(e,c) \in MemberOf \iff memberOf(e,c) \in I\]
</section>
+ <section>
+ <h4>Axioms</h4>
+
+ <p>To verify that the construction of $M(I)$ yields a PROV
+ structure, we must ensure that all of the axioms and
+ side-conditions in the components are satisfied. As noted above,
+ the disjointness constraints are satisfied by construction. </p>
+
+ </section>
+
<section>
<h4>Main results</h4>
@@ -3683,9 +3943,58 @@
completeness holds: every valid PROV instance has a model.</p>
<div class="theorem">
- <p>Suppose $I$ is a valid, normalized PROV instance, and let $M(I)$
- be the corresponding structure. Then $M(I)$ satisfies all of the
- inferences and constraints.</p>
+ <p>Suppose $J$ is a valid PROV instance and $I$ is a normal form for
+ $J$. Then $M(I) \models J$</p>
+ </div>
+ <div class="proof">
+ <p>
+ First, we consider the case where $J$ itself is a valid,
+ normalized PROV instance $I$, and let $M(I)$
+ be the corresponding structure. Then $M(I)$ is a PROV structure,
+ satisfying all of the axioms (and hence all of the inferences and
+ constraints) stated above.
+ </p>
+
+ <p>Moreover, $M(I) \models I$, as can be verified on a
+ case-by-case basis for each type of formula by considering its
+ semantics and the definition of the construction of $M$. </p>
+
+ <p> To conclude, we need to show that if $J$ is not in normal
+ form, and norma,izes to $I$, then $M(I) \models J$. WE can prove
+ this by induction on the length of the sequence of normalization
+ steps. The base case, when $J = I$, is established already.
+ Suppose $J$ normalizes in $n+1$ steps and we can perform one
+ normalization step on it to obtain $J'$, which normalizes to $I$
+ in $n$ steps. By induction, we know that $M(I) \models J'$. For
+ each possible normalization step, we must show that if $M(I)
+ \models J'$ then $M(I) \models J$.
+ </p>
+ <p>First consider inference steps. These add information, that
+ is, $J' \supseteq J$. Hence it is immediate that $M(I) \models J$
+ since every formula in $J$ is in $J'$, and all formulas of $J'$
+ are satisfied in $M(I)$.
+ </p>
+ <p>Next consider uniqueness constraint steps, which may involve
+ merging formulas. That is, $J = J_0 \cup
+ \{r(id,a_1,\ldots,a_n,attrs_1), r(id,b_1,\ldots,b_n,attrs_2)\}$
+ and $J' = S(J_0) \cup \{r(id,S(a_1),\ldots,S(a_n),attrs_1\cup
+ attrs_2)\}$, where $S$ is a unifying substitution making $S(a_i) =
+ S(b_i)$ for each $i \in \{1,\ldots,n\}$. Since $M(I) \models J'$,
+ we must have $M(I),\rho \models J'$ for some $\rho$, and therefore
+ we must also have that $M(I),\rho \models S(J_0)$ and $M(I)\rho \models r(id,S(a_1),\ldots,S(a_n),attrs_1\cup
+ attrs_2)$. We can extend $\rho$ to a valuation $\rho'$ such that
+ $M(I),\rho' \models S(x_1) = x_i \wedge \cdots \wedge S(x_k) =
+ x_k$ where $dom(S) = \{x_1,\ldots,x_k\}$.
+ $M(I),\rho' \models J_0$ and $M(I),\rho' \models r(id,a_1,\ldots,a_n,attrs_1\cup
+ attrs_2)$. Moreover, since $S$ is a unifier, we also have $M(I),\rho' \models r(id,b_1,\ldots,b_n,attrs_1\cup
+ attrs_2)$. Finally, since we can always remove attributes from an
+ atomic formula without danaging its satisfiability, we can
+ conclude that $M(I),\rho' \models r(id,a_1,\ldots,a_n,attrs_1)
+ \wedge r(id,b_1,\ldots,b_n, attrs_2)$. To conclude, we have
+ shown $M(I) \models J_0 \cup \{ r(id,a_1,\ldots,a_n,attrs_1)
+ r(id,b_1,\ldots,b_n, attrs_2)\}$, that is, $M(I) \models J$, as
+ desired.
+</p>
</section>
</section>