--- 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 @@
\\
\quad\Rightarrow
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.~
\\
\qquad p(id,a_1,\ldots,a_m) \wedge r(id,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
- additional activities, generations and usages added for imprecise derivations.
+<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
+ additional activities, generations and usages added for imprecise
+ 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>