author jcheney@inf.ed.ac.uk Sun, 07 Apr 2013 18:48:21 +0100 changeset 6067 ed64eec4d8dc parent 6066 3d236d13a755 child 6068 2de1db892bfc
* revised
 semantics/prov-sem.html
--- a/semantics/prov-sem.html	Fri Apr 05 18:36:16 2013 +0100
+++ b/semantics/prov-sem.html	Sun Apr 07 18:48:21 2013 +0100
@@ -1356,7 +1356,7 @@
<h3>First-Order Formulas</h3>

<p>We also consider the usual connectives and quantifiers of
-first-order logic [[Logic]].</p>
+first-order logic.</p>

\begin{array}{rcl}
\phi &{::=}& atomic\_formula\\
@@ -1897,7 +1897,7 @@
If $ended(end) = (a,e_1,a')$ and $ended(end') = (a,e_2,a')$ then $end=end'$.
</li>
<li id="axiom22">
-    If $started(st) = (a,e)$ then $st \preceq evt$ for all $evt \in + If$started(st) = (a,e,a')$then$st \preceq evt$for all$evt \in
events(a) - Invalidations$. </li> <li id="axiom23"> @@ -1955,6 +1955,10 @@ (ag_1,e_1,a_1)$ and $ended(end) = (ag_2,e_2,a_2)$ then $start \preceq end$.
</li>
+    <li id="axiom36">
+    If $e \in Entity$ and $prov:emptyCollection \in + value(e,prov:type)$ then $e \in Collections$ and there exists no
+    $e'$ such that $(e,e') \in Contains$.
</ol>
</div>

@@ -1980,7 +1984,7 @@

<p>A <em>PROV structure</em> $W$ is a collection of sets, functions, and relations containing all of the above
described components and satisfying all of the associated properties
-and axions.  If we need to talk about the objects or relations of
+and axioms.  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.
@@ -2005,7 +2009,7 @@
is the use of $Things$, which correspond to changing, real-world
things, as opposed to $Entities$, which correspond to limited views or
perspectives on $Things$, with some fixed aspects.  The semantic
-structures of $Things$ and $Entities$ provides a foundation for the
+structures of $Things$ and $Entities$ provide a foundation for the
$alternateOf$ and $specializationOf$ relations.
</p>

@@ -2111,7 +2115,7 @@
<div class="semantics" id="entity-semantics">
<p>$W,\rho \models entity(id,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes an entity $ent = \rho(id) \in Entities$
+<li>[WF] $id$ denotes an entity $ent = \rho(id) \in Entities$.
</li>
<li>the attributes match: $match(W,ent, attrs)$.
</li>
@@ -2150,19 +2154,29 @@
<p>$W,\rho \models activity(id,st,et,attrs)$
holds if and only if:</p>
<ol>
-<li>[WF] The identifier $id$ maps to an activity $act = \rho(id) \in Activities$
+<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:
-$startTime(id) = \rho(st)$
+$startTime(id) = \rho(st)$.
</li>
-<li>$\rho(et)$ is the activity's end time, that is: $endTime(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>There exists $start,e,a$ such that $started(start) = (act,e,a)$,
+and for all such start events $startTime(a) = time(start).</li> +<li>There exists$end,e',a'$such that$ended(end) = (act,e',a')$, and +for all such end events$endTime(a) = time(end)$.</li> <li>The attributes match:$match(W,act,attrs)$. </li> </ol> </div> + +<div class="remark"> + <p>The above definition is complicated for two reasons. First, we + need to ensure that every activity has a start and end event. + Second, when an$activity$formula is asserted, we need to make sure + all of the associated start and end event times match. + </p> + </div> </section> <section> @@ -2174,7 +2188,7 @@ <p>$W,\rho \models agent(id,attrs)$holds if and only if: </p> <ol> - <li>[WF]$id$denotes an agent$ag = \rho(id) \in Agents$+ <li>[WF]$id$denotes an agent$ag = \rho(id) \in Agents$. </li> <li>The attributes match:$match(W,ag,attrs)$. </li> @@ -2317,7 +2331,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) = startTime(act_2) = time(evt)$. +<li>The event happened at time$t$, that is,$\rho(t) = = time(evt)$. </li> <li> The activity$act_1$started$act_2$via entity$ent$: that is,$started(evt) = (act_2,ent,act_1)$.</li> @@ -2402,7 +2416,7 @@ <h5> Delegation </h5> -<p>The$actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$relation is interpreted using the$ActsFor$relation as follows:</p> +<p>The$actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$relation is interpreted as follows:</p> <div class="semantics" id="delegation-semantics"> <p> @@ -2452,7 +2466,7 @@ </li> <li>[WF]$g$denotes a generation event$gen = \rho(g) \in Generations$. </li> -<li>[WF]$u$denotes a use event$\rho(u) \in Usages$. +<li>[WF]$u$denotes a use event$use = \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) =
@@ -2822,58 +2836,60 @@
\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="#axiom7">Axiom 7</a>.</p> - </div> -<div class="inference" number="15" id="influence-inference"><ol><li>$\begin{array}[t]{l}
+  <p>This follows from the semantics of association and delegation, by <a href="#axiom7">Axiom 7</a>.</p> </div>
+<div class="inference" number="15" id="influence-inference">
+  <ol><li><br />$\begin{array}[t]{l} \forall id,e,a,t,attrs.~ \\ \qquad wasGeneratedBy(id,e,a,t,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,e,a,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$
+    </li>
+    <li><br />$\begin{array}[t]{l} \forall id,a,e,t,attrs.~ \\ \qquad used(id,a,e,t,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,a,e,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,a_2,a_1,attrs.~ \\ \qquad wasInformedBy(id,a_2,a_1,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,a_2,a_1,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,a_2,e,a_1,t,attrs.~ \\ \qquad wasStartedBy(id,a_2,e,a_1,t,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,a_2,e,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,a_2,e,a_1,t,attrs.~ \\ \qquad wasEndedBy(id,a_2,e,a_1,t,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,a_2,e,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e,a,t,attrs.~ \\ \qquad wasInvalidatedBy(id,e,a,t,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,e,a,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e_2,e_1,a,g,u,attrs.~ \\ \qquad wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,e_2,e_1,attrs) -\end{array}$</li><li>
+\end{array}$</li><li><br />$\begin{array}[t]{l}
\forall id,e,ag,attrs.~
\\
@@ -2881,7 +2897,7 @@
\\
wasInfluencedBy(id,e,ag,attrs)
-\end{array}$</li><li> +\end{array}$</li><li><br />
$\begin{array}[t]{l} \forall id,a,ag,pl,attrs.~ \\ @@ -2889,7 +2905,7 @@ \\ \quad\Rightarrow wasInfluencedBy(id,a,ag,attrs) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,ag_2,ag_1,a,attrs.~ \\ \qquad actedOnBehalfOf(id,ag_2,ag_1,a,attrs) @@ -3003,14 +3019,14 @@ <h3>Uniqueness constraints</h3> <div class="constraint" number="22" id="key-object"> - <ol><li>$\forall
+  <ol><li><br />$\forall id,attrs_1,attrs_2. entity(id,attrs_1) \wedge entity(id,attrs_2) \Rightarrow entity(id,attrs_1\cup attrs_2)$</li>
-  <li>$\forall + <li><br />$\forall
id,t_1,t_1',t_2,t_2',attrs_1,attrs_2.~ activity(id,t_1,t_2,attrs_1)
\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
+  <li><br />$\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">
@@ -3215,18 +3231,18 @@
end_1 \precedes end_2
\end{array}$</div> <div class="proof"> - <p>This follows from <a href="#axiom22">Axiom 22</a>. + <p>This follows from <a href="#axiom23">Axiom 23</a>. </p> </div> -<div class="constraint" number="33" id="usage-within-activity"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="33" id="usage-within-activity"><ol><li><br />$\begin{array}[t]{l} \forall start,use,a,e_1,e_2,a_1,t_1,t_2,attrs_1,attrs_2.~ \\ \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 \precedes use -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3240,14 +3256,14 @@ </p> </div> -<div class="constraint" number="34" id="generation-within-activity"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="34" id="generation-within-activity"><ol><li><br />$\begin{array}[t]{l} \forall start,gen,e_1,e_2,a,a_1,t_1,t_2,attrs_1,attrs_2.~ \\ \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 \precedes gen -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3270,10 +3286,12 @@ start \precedes end \end{array}$</div>
<div class="proof">
-  <p>This follows from the semantics of $wasInformedBy$ and the
+  <p>This follows from the semantics of $wasInformedBy$, <a
+  href="#axiom24">Axiom 24</a>, and the
previous two constraints, because $wasInformedBy$ implies the
existence of intermediate generation and usage events linking $a_1$
-  and $a_2$.
+  and $a_2$ through an entity $e$.  The generation of $e$ must precede
+  its use.
</p>
</div>

@@ -3287,7 +3305,7 @@
\end{array}$</div> <div class="proof"> - <p>This follows from <a href="#axiom23">Axiom 23</a>. + <p>This follows from <a href="#axiom24">Axiom 24</a>. </p> </div> @@ -3376,14 +3394,14 @@ </p> </div> -<div class="constraint" number="43" id="wasStartedBy-ordering"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="43" id="wasStartedBy-ordering"><ol><li><br />$\begin{array}[t]{l} \forall gen,start,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasStartedBy(start,a,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow gen \precedes start -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3398,14 +3416,14 @@ </p> </div> -<div class="constraint" number="44" id="wasEndedBy-ordering"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="44" id="wasEndedBy-ordering"><ol><li><br />$\begin{array}[t]{l} \forall gen,end,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow gen \precedes end -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3432,7 +3450,7 @@ <div class="proof"> <p> This follows from <a href="#axiom24">Axiom 24</a> and the fact - that if$e_2$specializes$e_1$then all of the events of the$e_2$+ that if$e_2$specializes$e_1$then all of the events of$e_2$are events of$e_1$. Thus, the generation of$e_1$precedes all events of$e_2$. </p> @@ -3449,34 +3467,34 @@ <div class="proof"> <p> This follows from <a href="#axiom25">Axiom 25</a> and the fact - that if$e_2$specializes$e_1$then all of the events of the$e_2$+ that if$e_2$specializes$e_1$then all of the events of$e_2$are events of$e_1$. Thus, the invalidation of$e_1$follows all events of$e_2$. </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}
+<div class="constraint" number="47" id="wasAssociatedWith-ordering"><p>In the following inferences, $pl$ may be a placeholder -.</p><ol><li><br />$\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.~ \\ \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 \precedes inv_2 -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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 \precedes end_2 -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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 \precedes end_2 -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3491,14 +3509,14 @@ </p> </div> -<div class="constraint" number="48" id="wasAttributedTo-ordering"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="48" id="wasAttributedTo-ordering"><ol><li><br />$\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.~ \\ \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 \precedes gen_2 -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3513,14 +3531,14 @@ </p> </div> -<div class="constraint" number="49" id="actedOnBehalfOf-ordering"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="49" id="actedOnBehalfOf-ordering"><ol><li><br />$\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.~ \\ \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 \precedes inv_2 -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\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) @@ -3541,133 +3559,133 @@ <section> <h3>Typing constraints</h3> -<div class="constraint" number="50" id="typing"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="50" id="typing"><ol><li><br />$\begin{array}[t]{l} \forall e,attrs.~ \\ \qquad entity(e,attrs) \\ \quad\Rightarrow typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall ag,attrs.~ \\ \qquad agent(ag,attrs) \\ \quad\Rightarrow typeOf(ag,agent) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall a,t_1,t_2,attrs.~ \\ \qquad activity(a,t_1,t_2,attrs) \\ \quad\Rightarrow typeOf(a,activity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall u,a,e,t,attrs.~ \\ \qquad used(u,a,e,t,attrs) \\ \quad\Rightarrow typeOf(a,activity) \wedge typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall g,a,e,t,attrs.~ \\ \qquad wasGeneratedBy(g,e,a,t,attrs) \\ \quad\Rightarrow typeOf(a,activity) \wedge typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall inf,a_2,a_1,t,attrs.~ \\ \qquad wasInformedBy(inf,a_2,a_1,t,attrs) \\ \quad\Rightarrow typeOf(a_1,activity) \wedge typeOf(a_2,activity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall start,a_2,e,a_1,t,attrs.~ \\ \qquad wasStartedBy(start,a_2,e,a_1,t,attrs) \\ \quad\Rightarrow typeOf(a_1,activity) \wedge typeOf(a_2,activity) \wedge typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall end,a_2,e,a_1,t,attrs.~ \\ \qquad wasEndedBy(end,a_2,e,a_1,t,attrs) \\ \quad\Rightarrow typeOf(a_1,activity) \wedge typeOf(a_2,activity) \wedge typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall inv,a,e,t,attrs.~ \\ \qquad wasInvalidatedBy(inv,e,a,t,attrs) \\ \quad\Rightarrow typeOf(a,activity) \wedge typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e_2,e_1,a,g_2,u_1,attrs.~ \\ \qquad notNull(a) \wedge notNull(g_2) \wedge notNull(u_1) \wedge wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs) \\ \quad\Rightarrow typeOf(e_2,entity) \wedge typeOf(e_1,activity) \wedge typeOf(a,activity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e_2,e_1,attrs.~ \\ \qquad wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \\ \quad\Rightarrow typeOf(e_2,entity) \wedge typeOf(e_1,activity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e,ag,attrs.~ \\ \qquad wasAttributedTo(id,e,ag,attrs) \\ \quad\Rightarrow typeOf(e,entity) \wedge typeOf(ag,agent) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,a,ag,pl,attrs.~ \\ \qquad notNull(pl) \wedge wasAssociatedWith(id,a,ag,pl,attrs) \\ \quad\Rightarrow typeOf(a,activity) \wedge typeOf(ag,agent) \wedge typeOf(pl,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,a,ag,attrs.~ \\ \qquad wasAssociatedWith(id,a,ag,-,attrs) \\ \quad\Rightarrow typeOf(a,activity) \wedge typeOf(ag,agent) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,ag_2,ag_1,a,attrs.~ \\ \qquad actedOnBehalfOf(id,ag_2,ag_1,a,attrs) \\ \quad\Rightarrow typeOf(ag_2,agent) \wedge typeOf(ag_1,agent) \wedge typeOf(a,activity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall e_2,e_1.~ \\ \qquad alternateOf(e_2,e_1) \\ \quad\Rightarrow typeOf(e_2,entity) \wedge typeOf(e_1,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall e_2,e_1.~ \\ \qquad specializationOf(e_2,e_1) \\ \quad\Rightarrow typeOf(e_2,entity) \wedge typeOf(e_1,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall c,e.~ \\ \qquad hadMember(c,e) \\ \quad\Rightarrow typeOf(c,Collection) \wedge typeOf(e,entity) -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall c.~ \\ \qquad entity(c,[prov:type = prov:emptyCollection])) @@ -3678,6 +3696,7 @@ <div class="proof"> <p>Each typing constraint follows immediately from well-formedness criteria marked [WF] in the corresponding semantics for formulas. + The final constraint requires <a href="#axiom36">Axiom 36</a>. </p> </div> </section> @@ -3685,21 +3704,21 @@ <section> <h3>Impossibility constraints</h3> -<div class="constraint" number="51" id="impossible-unspecified-derivation-generation-use"><ol><li>$\begin{array}[t]{l}
+<div class="constraint" number="51" id="impossible-unspecified-derivation-generation-use"><ol><li><br />$\begin{array}[t]{l} \forall id,e_1,e_2,g,attrs.~ \\ \qquad notNull(g) \wedge wasDerivedFrom(id,e_2,e_1,-,g,-,attrs) \\ \quad\Rightarrow False -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e_1,e_2,u,attrs.~ \\ \qquad notNull(u) \wedge wasDerivedFrom(id,e_2,e_1,-,-,u,attrs) \\ \quad\Rightarrow False -\end{array}$</li><li>$\begin{array}[t]{l} +\end{array}$</li><li><br />$\begin{array}[t]{l} \forall id,e_1,e_2,g,u,attrs.~ \\ \qquad notNull(g) \wedge notNull(u) \wedge wasDerivedFrom(id,e_2,e_1,-,g,u,attrs) @@ -3736,10 +3755,16 @@ \end{array}$</div>
<div class="proof">
<p>This follows from the assumption that the different kinds of
-  influences are disjoint sets, characterized by their types.
+  influences are disjoint sets, characterized by their types.  Note
+  that generic influences are allowed to overlap with more specific
+  kinds of influence.
</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} +<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, wasInfluencedBy\}$, the following constraint holds:</p>$\begin{array}[t]{l}
\forall id,a_1,\ldots,a_m,b_1,\ldots,b_n.~
\\
@@ -3804,6 +3829,9 @@
<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>
+<li>If $I$ is an instance and $W \models I$ and $I'$ is obtained from $I$ by applying one
+  of the PROV key or uniqueness constraints, then $W \models I'$.</li>
+
<li>If $I$ is an instance and $W \models I$ then $I$ has a normal
form $I'$ and   $W \models I'$.</li>
<li>If $I$ is a normal form and $W \models I$ then $I$ satisfies all of the ordering,
@@ -3814,16 +3842,17 @@
<div class="proof">
<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
+  part 2, if $W \models I$ then since $W$ satisfies the logical forms
+  of all uniqueness and kety constraints, constraint application cannot
+  fail on $I$ and $W \models I'$.</p>
+  <p> For part 3, proceed by induction on a terminating sequence of inference
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'$, as argued for the key constraints in
-  the previous section.</p>
+  applicable, then use part 2. </p>
<p>
-  For part 3, the arguments are as
+  For part 4, the arguments are as
in the previous section for each constraint. </p>
-  <p>Finally, for part 4,
+  <p>Finally, for part 5,
suppose $W \models I$.  Then $W \models I'$ where $I'$ is the normal
form of $I$ by part 2.  By part 3, $I'$ satisfies all of the
remaining constraints, so $I$ is valid.</p>
@@ -3852,17 +3881,16 @@
<p> The sets of structure $M(I)$ are: </p>
$\begin{eqnarray*} - Entities &=& \{id \mid entity(id,attrs) \in I\}\\ + Entities &=& \{id \mid I \models typeOf(id,entity)\}\\ Plans &=& \{pl \mid wasAssociatedWith(id,ag,act,pl,attrs) \in I, pl \neq -\}\\ - Collections &=& \{e \mid hadMember(e',e) \in I\} \\ - &\cup& \{e \mid - entity(e,attrs) \in I, prov:type=prov:emptyCollection \in attrs\}\\ + Collections &=& \{c \mid I \models typeOf(c,prov:Collection) \text{ + or } I \models typeOf(c,prov:EmptyCollection)\} \\ - Activities &=& \{id \mid activity(id,attrs) \in I\}\\ + Activities &=& \{id \mid I \models typeOf(id, activity)\}\\ &\cup& \{a_{id},a'_{id} \mid id \in Entities\}\\ &\cup& \{a_{id} \mid wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\ - Agents &=& \{id \mid agent(id,attrs) \in I\}\\ + Agents &=& \{id \mid I \models typeOf(id,agent)\}\\ \\ Usages &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\ &\cup& \{u_{id} \mid wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in @@ -3888,14 +3916,24 @@ \\ Influences &=& Events \cup Associations \cup Attributions \cup Communications \cup Delegations\\ - &\cup & \{id \mid wasInfluencedBy(id,q_2,q_1,attrs) \in I\}\\ + &\cup & \{id \mid wasInfluencedBy(id,o_2,o_1,attrs) \in I\}\\ \\ 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
+<p>In the definitions of $Entities$, $Collections$, $Activities$ and
+  $Agents$ we use the notation $I \models typeOf(id,t)$ to indicate
+  that $id$ must have type $t$ in $I$ according to the typing
+  constraints.  For example, for entities, this means that the set
+  $Entities$ contains all identifiers $e,e'$ appearing in the $entity(e,attrs)$,
+  $alternateOf(e,e')$, or $specializationOf(e,e')$ formulas, as well as all tose
+  appearing in the appropriate positions of other formulas, as
+  specified in the typing constraints.
+</p>
+<p>In the definitions of $Activities$, $Generations$, $Invalidations$, and $Usages$ we
+  write $a_{id}$, $g_{id}$, $i_{id}$ and $u_{id}$ respectively to indicate
+  derivations or entities.
</p>
<p> In addition, to define the set of $Things$, we introduce an
equivalence relation on $Entities$ as follows:
@@ -3923,9 +3961,7 @@
<section>
<h4>Functions</h4>

-<p> First, we consider the functions associated with $Entities$.  We
-employ an auxiliary function $events:Entities \to P(Events)$ that collects the set of all
-events in which $e$ participated.</p>
+<p> First, we consider the functions associated with $Entities$.</p>
$\begin{eqnarray*} events'(e) &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\ @@ -3938,19 +3974,19 @@ value'(e,a) &=& \{v \mid entity(e,attrs) \in I, (a=v) \in attrs\} \quad (a \neq uniq)\\ value'(e,uniq) &=&\{ uniq_{e}\}\\ -value(e,a) &=& value'(e) \cup \bigcup_{specializationOf(e',e) \in I} value'(e')\\ +value(e,a) &=& value'(e) \cup \bigcup_{specializationOf(e,e') \in I} value'(e')\\ thingOf(e) &=& [e]_\equiv \end{eqnarray*}$
<p>Above, we introduce a fresh attribute name $uniq$, not already in
use in $I$, along with a fresh value $e$ and for each entity $e$ we
-add an attribute-value pair $uniq=uniq_e$ to $values(e,uniq)$.  This
+add a value $uniq_e$ to $values(e,uniq)$.  This
construction ensures that if an entity is a specialization of another
in $I$ then the specialization relationship will hold in $M(I)$.  We
also define the set of all events involved in $e$ as the set of events
immediately involved in $e$ or any specialization of $e$.  Similarly,
the values of attributes of $e$ are those immediately declared for $e$
-along with those of any specialization.  We also introduce dummy
+along with those of $e'$ that $e$ specializes.  We also introduce dummy
generation and invalidation events for each entity $e$, along with
activities $a_e,a'_e$ to perform them.
</p>
@@ -3964,21 +4000,51 @@
\end{eqnarray*}
\]

-<p> The functions $startTime$ and $endTime$ mapping activities to
-  their start and end times is defined as follows:
+<p> The functions $events$, $startTime$ and $endTime$ mapping activities to
+  their start and end times are defined as follows:
</p>
$\begin{eqnarray*} +events(a) &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\ +&\cup& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\ +&\cup& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\ +&\cup& \{id \mid wasStartedBy(id,a,e,a',t,attrs) \in I\}\\ +&\cup& \{id \mid wasEndedBy(id,a,e,a',t,attrs) \in I\}\\ +&\cup& \{g_e,i_e\}\\ 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\\ \end{eqnarray*}$
-  <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 start and end times are arbitrary (say, some zero value) for activities with no
+  $activity$ formula declaring the times.  The above definitions of $startTime$ and
+  $endTime$ ignore any start times asserted in $wasStartedBy$ or
+  $wasEndedBy$ formulas.  If both $activity$ and
+  $wasStartedBy/wasEndedBy$ statements are present, then they must
+  match, but PROV-CONSTRAINTS does not require that the times of
+  multiple start or end events match for an activity with no
+  $activity$ statement.</p>
+
+<div class="remark">
+  <p>The following valid instance exemplifies the above discussion,
+  when $t_1 \neq t_2$:
+  </p>
+  <pre>
+wasStartedBy(id1;a,e1,a1,t1,[])
+wasStartedBy(id2;a,e2,a2,t2,[])
+</pre>
+<p>This instance becomes invalid if we add an $activity(a,[])$
+  statement, because it expands to $activity(a,T_1,T_2,[])$ where
+  $T_1,T_2$ are existential variables, and uniqueness constraints
+  require that $t_1 = T_1 = t_2$, which leads to uniqueness constraint failure.
+  </p>
+  </div>
+<p> For other $Objects$ besides $Entities$ and $Activities$, the
+associated sets of $Events$ are defined to be empty.  (An $Agent$ that
+happens to be an $Entity$ or $Activity$ will have the set of events
+defined above for the appropriate kind of object.  Note that since
+$Entities$ and $Activities$ are disjoint, this definition is unambiguous.)</p>
+
<p> The function $time$ mapping $Events$ to their $Times$ is defined
as follows:
</p>
@@ -3990,7 +4056,8 @@
time(id) &=& t \text{ where }wasEndedBy(id,a,e,a',t,attrs) \in I\\
\end{eqnarray*}
\]
-
+  <p>This definition is deterministic because the sets of identifiers
+  of different $Events$ are disjoint, and the associated times are unique.</p>

<p>Finally, the functions giving the interpretations of the
different identified influences are as follows:
@@ -4014,8 +4081,10 @@
communicated(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*}
+  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*}
\]
<p>Note that since $I$ is normalized and valid, by the uniqueness
constraints these functions are all well-defined.  In the case for
@@ -4023,6 +4092,30 @@
and usages linking $e_2$ to $e_1$.
</p>

+<p>The definition of the $influenced$ function is more involved, and
+is as follows:</p>
+$\begin{eqnarray*} +influenced(id) &=& used(id) \cup generated(id) \cup invalidated(id)\\ +&\cup& \{(a,e) \mid (a,e,a') \in started(id)\}\\ +&\cup& \{(a,e) \mid (a,e,a') \in ended(id)\}\\ +&\cup & \{(ag,act) \mid (ag,act,pl) \in associatedWith(id)\}\\ + &\cup& attributedTo(id) \\ +&\cup & \{(ag_2,ag_1) \mid (ag_2,ag_1,act) \in actedFor(id)\}\\ +&\cup& communicated(id)\\ +&\cup& \{(e_2,e_1) \mid e_2 \cdot w \cdot e_1 \in + derivationPath(id)\}\\ +&\cup& \{(o_2,o_1) \mid wasInfluencedBy(id,o_2,o_1) \in I\} + \end{eqnarray*} +$
+<p>This definition ensures that by construction $influenced(id)$
+contains all of the other associated relationships.  For any specific
+$id$, however, most of the above sets will be empty, and the final
+line will often  be redundant.  It is not always redundant, because it
+is possible to assert an unspecified influence in $I$.</p>
+
+<p> It is straightforward to verify (by their definitions) that the
+event sets associated with entities and activities satisfy the
+side-conditions in <a href="#events">Component 9</a>.</p>
</section>
<section>
<h4>Relations</h4>
@@ -4031,7 +4124,7 @@
the semantics.</p>
<p>The event ordering relation is defined as follows:</p>
$evt \preceq evt' \iff (evt,evt') \in G_I$
-    <p> Here, we are using a slight abuse of notation: we write $G_I$
+    <p> closed under reflexivity and transitivity.  Here, we are using a slight abuse of notation: we write $G_I$
for the directed graph that is used during validation of $I$ to
test for cycles amond event ordering constraints.  See Sec. 7.1 of PROV-CONSTRAINTS [[PROV-CONSTRAINTS]].</p>

@@ -4099,7 +4192,7 @@
<li> Axioms 28 through 31 follow from Constraint 47.</li>
<li> Axioms 32 and 33 follow from Constraint 48.</li>
<li> Axioms 34 and 35 follow from Constraint 49.</li>
-
+<li>Axiom 36 follows from Constraint 50, part 19, and the semantics of $typeof$.</li>
</ol>
</section>

@@ -4107,19 +4200,17 @@
<h4>Main results</h4>

<p> The main results of this section are that if a valid PROV instance
-    $I$ normalizes to
-    $I'$, then  $M(I') \models I$, and that furthermore $M(I')$
+    $I$ has a model $M \models I$ that
satisfies all of the inferences and constraints.  Thus, a form of
completeness holds: every valid PROV instance has a model.</p>

<div class="theorem" id="weak-completeness-theorem">
-  <p>Suppose $J$ is a valid PROV instance and $I$ is a normal form for
-  $J$.  Then $M(I) \models J$.</p>
+  <p>Suppose $J$ is a valid PROV instance.  Then there exists a PROV structure $M$ such that $M \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)$
+  normalized PROV instance $I$, with no existential variables, 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.
@@ -4127,42 +4218,95 @@

<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 normalizes to $I$, then $M(I) \models J$.  We can prove
+    semantics and the definition of the construction of $M$.  Most
+    cases are straightforward; we consider the cases of $alternateOf$
+    and $specializationOf$ since they are among the most
+    interesting.</p>
+
+    <ul>
+      <li>Suppose $alternateOf(e_1,e_2) \in I$.  We wish to show that
+      $M(I) \models alternateOf(e_1,e_2)$.  Since there are no
+      existential variables in $I$, we know that $e_1,e_2 \in + M(I).Entities$.  Moreover, $e_1 \equiv e_2$ according to the
+      equivalence relation defined above, and so $thingOf(e_1) = + [e_1]_\equiv = [e_2]_\equiv = thingOf(e_2)$, so we can conclude
+      that $M(I) \models alternateOf(e_1,e_2)$.
+</li>
+<li>Suppose $specializationOf(e_1,e_2) \in I$.  We wish to show that
+      $M(I) \models specializationOf(e_1,e_2)$.  Again, clearly
+      $e_1,e_2 \in Entities$, and since $I$ satisfies all inferences,
+      we know that $alternateOf(e_1,e_2)\in I$ so clearly
+      $thingOf(e_2) = thingOf(e_1)$ as argued above.  Next,
+$\begin{eqnarray*} +events(e_1) &=& events'(e_1) \cup \bigcup_{specializationOf(e',e_1) + \in I} events'(e') \\ +&\subseteq& events'(e_2) \cup + \bigcup_{specializationOf(e',e_2) \in I} events'(e_2)\\ +&=& + events(e_2) +\end{eqnarray*} +$
+because $specializationOf(e_1,e_2) \in I$ and all $e'$ that are specializations of $e_1$ are also
+      specializations of $e_2$.
+  Furthermore, for each $attr$,
+$\begin{eqnarray*} +value(e_1,attr) &=& value'(e_1,attr) \cup + \bigcup_{specializationOf(e_1,e') \in I} value'(e',attr)\\ + &\supseteq& value'(e_2,attr) \cup + \bigcup_{specializationOf(e_2,e')\in I}value'(e',attr)\\ +&=& value(e_2,attr) +\end{eqnarray*} +$
+for the same reason.  Finally, by construction $uniq_{e_1} \in + value(e_1,uniq)$ and $uniq_{e_1} \notin value(e_2,uniq)$ so the
+      inclusion is strict for the special attribute $uniq$.  Thus, we
+      have verified all of the conditions necessary to conclude $M(I) + \models specializationOf(e_1,e_2)$.
+</li>
+</ul>
+
+<p> Next, we show how to handle a normalized, valid  $I$ contains
+existential variables $x_1,\ldots,x_n$.  Choose fresh constants $c_1,\ldots,c_n$ of
+appropriate types for the existential variables and define $\rho(x_i) += c_i$. Then $M(\rho(I)) \models \rho(I)$ by the above argument.
+Moreover, $M(\rho(I)),\rho \models I$.  So $M(\rho(I))$ is itself the desired
+model.
+</p>
+
+<p> Finally, to handle the case where $J$ is an arbitrary valid instance, we need to show that if $J$ is not in normal
+    form, and normalizes to some $I$ such that $M \models I$, then $M \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$.
+    in $n$ steps.  By induction, we know that $M \models J'$.  For
+    each possible normalization step, we must show that if $M + \models J'$ then $M \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$
+    is, $J' \supseteq J$.  Hence it is immediate that $M \models J$
since every formula in $J$ is in $J'$, and all formulas of $J'$
-    are satisfied in $M(I)$.
+    are satisfied in $M$.
</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 + S(b_i)$ for each $i \in \{1,\ldots,n\}$.  Since $M \models J'$,
+    we must have $M,\rho \models J'$  for some $\rho$, and therefore
+    we must also have that $M,\rho \models S(J_0)$ and $M,\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_1 \wedge \cdots \wedge S(x_k) = +$M,\rho' \models S(x_1) = x_1 \wedge \cdots \wedge S(x_k) =
x_k$where$dom(S) = \{x_1,\ldots,x_k\}$. Also, -$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
+    $M,\rho' \models J_0$ and $M,\rho' \models r(id,a_1,\ldots,a_n,attrs_1\cup + attrs_2)$.  Moreover, since $S$ is a unifier, we also have $M,\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 damaging its satisfiability, we can
-    conclude that $M(I),\rho' \models r(id,a_1,\ldots,a_n,attrs_1) + conclude that$M,\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 + shown$M \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 \models J\$, as
desired.
</p>
</section>