author jcheney@inf.ed.ac.uk Thu, 28 Mar 2013 18:14:15 +0000 changeset 6014 7100671defba parent 6013 533399e45425 child 6015 f03fa125a7e1
* resuming work on semantics
 semantics/prov-sem.html
--- a/semantics/prov-sem.html	Thu Mar 28 12:03:32 2013 -0600
+++ b/semantics/prov-sem.html	Thu Mar 28 18:14:15 2013 +0000
@@ -898,7 +898,7 @@
};
var respecConfig = {
// specification status (e.g. WD, LCWD, NOTE, etc.). If in doubt use ED.
-          specStatus:           "WD-NOTE",
+          specStatus:           "ED",

// the specification's short name, as in http://www.w3.org/TR/short-name/
shortName:            "prov-sem",
@@ -910,7 +910,7 @@

// if you wish the publication date to be other than today, set this
-         publishDate:  "2013-03-12",
+         publishDate:  "2013-04-30",

// if the specification's copyright date is a range of years, specify
// the start date here:
@@ -1138,12 +1138,10 @@
<li><a href="#theory">Section 5</a> presents the inferences and
constraints from PROV-CONSTRAINTS as first-order formulas, and gives
brief justifications for their soundness.</li>
-  <li><a href="#soundness">Section 6</a> summarizes the main result: soundness of
-the theory introduced in section 5 with respect to the naive
-  semantics.  Completeness does not hold for the naive semantics.  The
-  theory is, however, sound and complete with respect to a larger
-  class of <em>syntactic models</em>, which implies that a PROV
-  instance is valid if and only if it has a syntactic model.</li>
+  <li><a href="#soundness">Section 6</a> summarizes the main results.
+  We show that Completeness does not hold for the naive semantics,
+  but we establish a weak form of completeness: every valid PROV
+  instance has a naive model.</li>
</ul>
<div class="note">
<p>TODO: We would like to say something stronger here, such as a
@@ -1338,7 +1336,7 @@
other cross-instance assertions, and this semantics should be
generalized in order to provide a rationale for such an
extension and to establish the soundness of constaints associated
-  with $memberOf$. </p>
+  with $mentionOf$. </p>
</div>
</section>

@@ -1385,7 +1383,6 @@

<h3> Things </h3>

-<div class="note">TODO: Add semantic structure for collections and membership.</div>
<p><em>Things</em>  is a set of things in the situation being modeled.  Each thing has a lifetime during which it exists and attributes whose values can change over time.
</p>
<p>To model this, a structure $W$ includes:
@@ -1480,9 +1477,23 @@

<div class="component" id="entities">
<ol><li> a set $Entities \subseteq Objects$ of entities, disjoint from $Activities$ and $Events$ below.
-</li><li> a function $thingOf : Entities \to Things$ that associates each $Entity$ with a $Thing$, such that for each $t \in lifetime(obj)$, and for each attribute $a$ we have $value(obj,a) \subseteq value(thingOf(obj),a,t)$.
-</li><li> $lifetime(e) \subseteq lifetime(t)$.
-</li></ol>
+</li><li> a function $thingOf : Entities \to Things$ that associates
+  each $Entity$ $e$ with a $Thing$, such that for each $t \in + lifetime(e)$, and for each attribute $a$ we have $value(e,a) + \subseteq value(thingOf(e),a,t)$ and $lifetime(e) \subseteq lifetime(thingOf(e))$.
+</li>
+<li>a relation $SpecializationOf \subseteq Entities \times Entities$
+  that is irreflexive and transitive.  Furthermore, if $(e_1,e_2) \in + SpecializationOf$ then
+<ol><li>
+  $thingOf(e_1) = thingOf(e_2)$
+  </li>
+  <li>$lifetime(e_1) \subseteq lifetime(e_2)$</li>
+  <li>For each attribute $attr$ we have $value(e_1,attr) \supseteq + value(e_2,attr)$.</li>
+  </ol></li>
+</ol>
+
</div>

<div class="remark"><p> Although both entities and things can have
@@ -1539,6 +1550,18 @@
</div>
</section>

+<section>
+  <h5>Collections</h5>
+  <p>We identify another specific subset of the entities called
+  <em>collections</em>, with the following associated structure:</p>
+  <div class="component" id="collections">
+    <ul><li>A set $Collections \subseteq Entities$</li>
+    <li>A membership relation $MemberOf\subseteq Entities \times Collections$
+  indicating when an entity is a member of another (collection)
+  entity.</li>
+  </ul>
+    </div>
+  </section>
</section>

<section>
@@ -1629,17 +1652,33 @@
</div>

<p>Associations are used below in the $ActsFor$ and $AssociatedWith$ relations.
-
+</p>

</section>
<section>
<h5>Communications</h5>
-  <div class="note">TODO</div>
+  <p>A <em>Communication</em> is an interaction indicating exchange of
+  information between activities.  To model communications, we introduce:
+</p>
+<div class="component" id="communications">
+  <p>A set $Communications \subseteq Interactions$, such that
+  $type(comm) = communication$ if and only if $comm \in Communications$.
+</p>
+  </div>

+
</section>
<section>
<h5>Delegations</h5>
-  <div class="note">TODO</div>
+<p>A <em>Delegation</em> is an interaction relating  two agents.  To model delegations, we introduce:
+</p>
+<div class="component" id="associations">
+  <p>A set Delegations \subseteq Interactions$, such that +$type(del) = delegation$if and only if$del \in Delegations$. +</p> + </div> + +<p>Associations are used below in the$ActsFor$and$AssociatedWith$relations. </section> <section> @@ -1676,27 +1715,38 @@ <h4> Simple relations </h4> <p>The entities, interactions, and activities in a structure are related in the following ways: </p> -<ol><li> A relation$Used \subseteq Events \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. +<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><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></ol>
+</li>
+<li>A relation $Influence \subseteq Events \times Objects \times +Objects$ indicating when one object influences another.</ol>

<div class="note">
-  TODO: Communication, start, end relations
-  </div>
-
-  <div class="note">
-  TODO: Specialization relation
+  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
-  start before that of the entity.
+  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>

@@ -1739,6 +1789,7 @@
</div>

<div class="note">
+  TODO:
We can make the characterization of DerivationPaths more
precise/concise by introducing sets of Usage and Generation events.
</div>
@@ -2074,11 +2125,11 @@
<li>The event $evt$ has type $start$, i.e. $type(evt) = start$.
</li>
<li>The event happened at the start of $act_2$, that is, $(evt,act_2) - \in EventsActivities$, and $\rho(t) = min(lifetime(act_2)) = time(evt)$.
+  \in EventActivity$, and$\rho(t) = min(lifetime(act_2)) = time(evt)$. </li> -<li>TODO: The entity$e$was generated by$act_1$and started$act_2$. +<li> The activity$act_1$started$act_2$via entity$ent$: that is,$(evt,act_2,ent,act_1) \in Start$.</li> <li>The event happened during$act_1$, that is,$(evt,act_1)
-  \in EventsActivities$. + \in EventActivity$.
</li>
<li>The attributes match: $match(W,evt,attrs)$.
</li></ol></div>
@@ -2100,10 +2151,10 @@
<li>[WF] $a_1$ denotes an activity $act_1 = \rho(a_1)\in Activities$.</li>
<li>The event $evt$ has type $end$, i.e. $type(evt) = end$.</li>
<li>The event happened at the end of $act_2$, that is, $(evt,act_2) - \in EventsActivities$, and $\rho(t) = max(lifetime(act_2)) = time(evt)$.</li>
-  <li>TODO: The entity $e$ was generated by $act_1$ and ended $act_2$.</li>
-
-<li>The event happened during $act_1$, that is, $(evt,act_1) \in EventActivity.</li> + \in EventActivity$, and $\rho(t) = max(lifetime(act_2)) = time(evt)$.</li>
+<li> The activity $act_1$ ended $act_2$ via entity $ent$: that is,
+  $(evt,act_2,ent,act_1) \in End$.</li>
+<li>The event happened during $act_1$, that is, $(evt,act_1) \in EventActivity$.</li>
<li>The attributes match: $match(W,evt,attrs)$.</li>
</ol>
</div>
@@ -2137,8 +2188,25 @@

<section>
<h4>Communication</h4>
-<div class="note">TODO: Communication</div>
-
+<p>A communication formula </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>
+<li>[WF] $a_1,a_2$ denote  activities $act_1 = \rho(a_1) \in +Activities, act_2 = \rho(a_2)\in Activities$.
+</li>
+<li>TODO: There exists some intermediate entity $ent$, generation $gen \in +Events$ and usage $use \in Events$ such that $(gen,ent,act) \in +Generation$ and $(use,act_2,ent) \in Usage$
+</li>
+<li>The attributes match: $match(W,comm,attrs)$.
+</li></ol>
+</div>
</section>

@@ -2172,7 +2240,7 @@
<p>
Derivation formulas can be of one of two forms:</p>
<ul><li>$wasDerivedFrom(id,e_2,e_1,a,g,u,attrs)$, which specifies an
-  activity, generation and usage event.  For convenience we call
+  activity, generation and usage event.  For convenience we call this
a <dfn>precise derivation</dfn>.</li>
<li> and $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$, which does not
specify an activity, generation and usage event.  For convenience we
@@ -2197,7 +2265,8 @@
</li>
<li>[WF] $u$ denotes a use event $\rho(u) \in Events$ and $type(\rho(u)) = use$.
</li>
-<li>The derivation denotes a one-step derivation $derivationPath(deriv) = +<li>The derivation denotes a one-step derivation path linking the +entities via the activity, generation and use:$derivationPath(deriv) =
ent_2 \cdot gen \cdot act \cdot use \cdot ent_1$. </li> <li>The attribute values match:$match(W,deriv,attrs)$.</li> @@ -2227,8 +2296,19 @@ <section> <h3>Influence</h3> - <div class="note">TODO: Define influence semantics.</div> - + <div class="semantics" id="influence-semantics"> + <p>$W,\rho \models wasInfluencedBy(id,o_2,o_1,attrs)$holds if + and only if at least one of the following hold:</p> + <ol> + <li>[WF]$o_1$and$o_2$denote objects$obj_1 = \rho(o_1) \in
+  Objects$and$obj_2= \rho(o_2)
+  \in Objects$.</li> + <li>The objects are inthe Influence relation:$(id,o_2,o_1) \in Influence$.</li> + <li>The attribute values match:$match(W,deriv,attrs)$. +</li> + </ol> + + </section> <section> @@ -2236,35 +2316,37 @@ <p>The$specializationOf(e_1,e_2)$relation indicates when one entity formula presents more specific aspects of another. </p> - <div class="note"> - <p>TODO: The content of this definition may need to be moved into the - semantic structure via an irreflexive/transitive specialization - relation on Entities, since by - itself this definition is not transitive.</p> - </div> + <div class="semantics" id="specialization-semantics"> <p>$W,\rho \models specializationOf(e_1,e_2)$holds if and only if:</p> <ol> <li>[WF] Both$e_1$and$e_2$are entity identifiers, denoting distinct entities$ent_1
-  = \rho(e_1) \in Entities$and$ent_2 = \rho(e_2) \in Entities$, - where$ent_1 \neq ent_2$. + = \rho(e_1) \in Entities$ and $ent_2 = \rho(e_2) \in Entities$.
</li>
-<li>The two Entities refer to the same Thing, that is, $thingOf(ent_1) = thingOf(ent_2)$.
+<li>$(ent_1,ent_2) \in SpecializationOf$.
+</li>
+</ol>
+</div>
+
+<div class="remark">
+  <p>The conditions on the $SpecializationOf$ relation imply that:</p>
+<ol>
+  <li>The two entities are different: $ent_1 \neq ent_2$.
+  <li>The two Entities refer to the same Thing, that is, $thingOf(ent_1) = thingOf(ent_2)$.
</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></ol></div>
-
+</li></ol>
<p>The second criterion says that the two Entities present (possibly different) aspects of
the same Thing. Note that the third criterion allows $ent_1$ and
$ent_2$ to have the same lifetime (or that of $ent_2$ can be larger).
The last criterion allows $ent_1$ to have more defined attributes than
$ent_2$, but they must include the attributes defined by $ent_2$.
</p>
-
+</div>
</section>
<section>

@@ -2299,13 +2381,11 @@
<li>[WF] Both $e_1$ and $e_2$ are entity identifiers, denoting $coll = \rho(c) \in Collections$ and $ent = \rho(e) \in Entities$.
</li>
-<li>TODO
+<li>The entity $ent$ is a member of the collection $coll$: that is,
+$(ent,coll) \in MemberOf$.
</li></ol>
</div>
-<div class="note">
-  <p>Additional constraints needed above to refer to (not yet defined)
-collection   structure of entities/things.</p>
-  </div>
+

</section>
@@ -2336,7 +2416,7 @@
event times are
mapped to a single time line, this amounts to
comparing the event times.  The semantics of strictly precedes ($x - \prec y$ is similar, only $x$ must take place strictly before $y$).</p>
+  \prec y$) is similar, only$x$must take place strictly before$y$.</p> <div class="semantics" id="precedes-semantics"> <ol> <li>$W,\rho \models x \preceq y$holds if and only if @@ -2375,7 +2455,8 @@ </p> </div> - + </section> + <section> <h4>typeOf</h4> @@ -2390,17 +2471,16 @@ <li>$W,\rho\models typeOf(ag,agent)$holds if and only if$\rho(ag) \in Agents$.</li> <li>$W,\rho\models typeOf(c,Collection)$holds if and only if - TODO.</li> +$\rho(c) \in Collections.</li>
<li>$W,\rho\models typeOf(c,EmptyCollection)$ holds if and only if
-      TODO.</li>
+      $\rho(c) \in Collections$ and there is no $e \in Entities$ such
+    that $(e,\rho(c)) \in MemberOf$.</li>
</ol>

</div>

-    <div class="note">TODO Collections</div>

</section>
-
</section>
</section>

@@ -2670,48 +2750,102 @@
<h3>Uniqueness constraints</h3>

<div class="constraint" number="22" id="key-object">
-  <ol><li>The
-  identifier field $id$ is a <span class="conditional">KEY</span> for
-  the $entity(id,attrs)$ statement.</li>
-  <li>The identifier field $id$
-  is a <span class="conditional">KEY</span> for the
-  $activity(id,t_1,t_2,attrs)$ statement.</li>
-  <li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $agent(id,attrs)$ statement.</li></ol></div>
+  <ol><li>$\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 + 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 + 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>
+    </div>
<div class="constraint" number="23" id="key-properties">
-  <ol><li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the
-    $wasGeneratedBy(id,e,a,t,attrs)$ statement.</li>
-    <li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the $used(id,a,e,t,attrs)$
-    statement.</li>
-    <li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the
-    $wasInformedBy(id,a_2,a_1,attrs)$ statement.</li>
+  <ol><li>$\begin{array}[t]{l} + \forall + id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\ + wasGeneratedBy(id,e,a,t,attrs) + \wedge wasGeneratedBy(id,e',a',t',attrs_2) \\ + \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 + 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 + 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 + 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 + 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 + 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
-    $wasStartedBy(id,a_2,e,a_1,t,attrs)$ statement.</li>
-    <li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the
-    $wasEndedBy(id,a_2,e,a_1,t,attrs)$ statement.</li>
-    <li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the
-    $wasInvalidatedBy(id,e,a,t,attrs)$ statement.</li>
+    $wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)$ statement. $\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
-    $wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)$ statement.</li>
-    <li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the
-    $wasAttributedTo(id,e,ag,attrs)$ statement.</li>
+    $wasAttributedTo(id,e,ag,attrs)$ statement. $\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.</li>
+    $wasAssociatedWith(id,a,ag,pl,attrs)$ statement. $\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.</li>
-    <li>The identifier field $id$ is a <span
-    class="conditional">KEY</span> for the
-    $wasInfluencedBy(id,o2,o1,attrs)$ statement.</li></ol>
+    $actedOnBehalfOf(id,ag_2,ag_1,a,attrs)$ statement. $\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 + 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' + \wedge o_2=o_2' + \end{array}$</li></ol>
</div>
+    <div class="proof">
+<p>  These properties follow immediately from the definitions of the
+  semantics of the respective assertions.</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.~ \\ @@ -3227,7 +3361,12 @@ \quad\Rightarrow False \end{array}$</div>
-
+<div class="proof">
+  <p>This follows from the definition of the semantics of
+  $typeOf(c,EmptyCollection)$, which requires that there are no
+  members of the collection denoted by $c$.
+  </p>
+  </div>
</section>
</section>
</section>
@@ -3270,18 +3409,13 @@
remaining constraints, so $I$ is valid.</p>
</div>

-<section id="syntactic">
-  <h3>Syntactic Models and Completeness</h3>
-
-  <p>In this section we relate PROV instances and validation as
-  specified in PROV-CONSTRAINTS to certain models, which we call
-  <dfn>syntactic models</dfn>.  We will show that valid PROV instances
-  correspond to syntactic models of the first-order theory of
-  PROV.</p>
+<section id="completeness">
+  <h3>Weak Completeness</h3>
+

<div class="note">
-    Explain how to translate PROV formulas to purely relational
-    formulas.
+    TODO: Translate valid instances (via normal forms) to models, to
+    obtain a weak form of completeness.
</div>
</section>