--- 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
Entity; ensure that for attribution the agent's lifetime must
- 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>