--- a/model/prov-constraints.html Mon Aug 06 18:35:01 2012 +0100
+++ b/model/prov-constraints.html Mon Aug 06 20:04:37 2012 +0100
@@ -526,9 +526,9 @@
that applications MAY employ, including <em>definitions</em> of some
provenance statements in terms of others, and also defines a class of
<a>valid</a> PROV instances by specifying <em>constraints</em> that
-<a>valid</a> PROV instances must satisfy. There are three kinds of
+<a>valid</a> PROV instances must satisfy. There are four kinds of
constraints: <em>uniqueness constraints</em>, <em>event ordering
-constraints</em>, and <em>impossibility constraints</em>.
+constraints</em>, <em>impossibility constraints</em>, and <em>type constraints</em>.
Applications SHOULD produce valid
provenance and MAY reject provenance that is not <a>valid</a>. Applications
SHOULD also use definitions, inferences and constraints to normalize
@@ -538,7 +538,7 @@
<p>To summarize: compliant applications use definitions,
inferences, and uniqueness constraints to normalize PROV instances,
-and then check event ordering and impossibility constraints. If these
+and then check event ordering, impossibility, and type constraints. If these
checks succeed, the instance is
<a>valid</a>, and the normal form is considered <a>equivalent</a> to
the original instance. Also, any two PROV instances that yield the
@@ -564,14 +564,15 @@
new facts representing implicit knowledge about the structure of
provenance. </p>
-<p><a href="#constraints">Section 5</a> presents three kinds of constraints,
+<p><a href="#constraints">Section 5</a> presents four kinds of constraints,
<em>uniqueness</em> constraints that prescribe that certain statements
must be unique within PROV <a>instances</a>,
<em>event ordering</em> constraints that require that the records in a
PROV <a>instance</a> are consistent with a sensible ordering of events
-relating the activities, entities and agents involved, and
+relating the activities, entities and agents involved,
<em>impossibility</em> constraints that forbid certain patterns of
-statements in valid PROV instances.
+statements in valid PROV instances, and <em>type</em> constraints that
+classify the types of identifiers in valid PROV instances.
</p>
<p><a href="#normalization-validity-equivalence">Section 6</a> defines the notions
@@ -750,7 +751,7 @@
<section>
<h4>Summary of constraints and inferences</h4>
-<p><a href="">Table 5</a> summarizes the definitions, inferences, and
+<p><a href="">Table 1</a> summarizes the definitions, inferences, and
constraints of this document.
</p>
@@ -758,7 +759,7 @@
<div id="prov-constraints-fig" style="text-align: left;">
<table class="thinborder" style="margin-left: auto; margin-right: auto; border-color: #0;">
-<caption id="prov-constraints">Table 5: Summary of definitions, constraints, and inferences for PROV Types and Relations</caption>
+<caption id="prov-constraints">Table 1: Summary of definitions, constraints, and inferences for PROV Types and Relations</caption>
<tr><td><a><b>Type or Relation Name</b></a></td><td><b>
Inferences and Constraints</b></td><td><b>Component</b></td></tr>
<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
@@ -1097,7 +1098,8 @@
[[PROV-N]] statements, or explicit <span class="name">-</span>
markers, are placeholders for existentially quantified variables;
that is, they denote unknown values. There are a few exceptions to
- this general rule, which are explained below.</p>
+ this general rule, which are specified in <a class="rule-ref"
+ href="#optional-placeholders"><span>TBD</span></a></p>
<p> Definitions have the following general form:</p>
@@ -1175,10 +1177,10 @@
<ol> <li>
<span class="name">r(a<sub>1</sub>,...,a<sub>n</sub>) </span> holds <span class="conditional">IF AND ONLY IF</span>
there exists <span class="name">id</span> such that <span
- class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
- <li> <span class="name">r(-;a<sub>1</sub>,...,a<sub>n</sub>) </span> holds <span class="conditional">IF AND ONLY IF</span>
+ class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
+ <li> <span class="name">r(-; a<sub>1</sub>,...,a<sub>n</sub>) </span> holds <span class="conditional">IF AND ONLY IF</span>
there exists <span class="name">id</span> such that <span
- class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
+ class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
</ol>
</div>
@@ -1188,13 +1190,13 @@
<div class="definition" id="optional-attributes">
<ol>
<li>
- For each <span class="name">r</span> in {<span
+ For each <span class="name">p</span> in {<span
class="name">entity</span>, <span class="name">activity</span>,
<span class="name">agent</span>}, if <span class="name">a<sub>n</sub></span> is not an attribute
list parameter then the following definitional rule holds:
- <p><span class="name">r(a<sub>1</sub>,...,a<sub>n</sub>)</span>
+ <p><span class="name">p(a<sub>1</sub>,...,a<sub>n</sub>)</span>
holds <span class="conditional">IF AND ONLY IF</span> <span
- class="name">r(a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.
+ class="name">p(a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.
</li>
<li>
For each <span class="name">r</span> in {
@@ -1211,9 +1213,9 @@
<span class="name">actedOnBehalfOf</span>}, if <span class="name">a<sub>n</sub></span> is not an
attribute list parameter then the following definition holds:
- <p> <span class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds
+ <p> <span class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>)</span> holds
<span class="conditional">IF AND ONLY IF</span> <span
- class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li></ol>
+ class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li></ol>
</div>
<p> Finally, many PROV
@@ -1227,21 +1229,21 @@
<ol>
<li> <span class="name">activity(id,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">activity(id,-,-,attrs)</span>.
</li>
- <li><span class="name">wasGeneratedBy(id;e,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasGeneratedBy(id;e,-,-,attrs)</span>.
+ <li><span class="name">wasGeneratedBy(id; e,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasGeneratedBy(id; e,-,-,attrs)</span>.
</li>
- <li><span class="name">used(id;a,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">used(id;a,-,-,attrs)</span>.
- </li>
- <li><span class="name">wasStartedBy(id;a,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasStartedBy(id;a,-,-,-,attrs)</span>.
+ <li><span class="name">used(id; a,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">used(id; a,-,-,attrs)</span>.
</li>
- <li><span class="name">wasEndedBy(id;a,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasEndedBy(id;a,-,-,-,attrs)</span>.
- </li>
- <li><span class="name">wasInvalidatedBy(id;e,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasInvalidatedBy(id;e,-,-,attrs)</span>.
+ <li><span class="name">wasStartedBy(id; a,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasStartedBy(id; a,-,-,-,attrs)</span>.
</li>
- <li><span class="name">wasDerivedFrom(id;e2,e1,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasDerivedFrom(id;e2,e1,-,-,-,attrs)</span>.
+ <li><span class="name">wasEndedBy(id; a,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasEndedBy(id; a,-,-,-,attrs)</span>.
</li>
- <li><span class="name">wasAssociatedWith(id;e,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasAssociatedWith(id;e,-,-,attrs)</span>.
+ <li><span class="name">wasInvalidatedBy(id; e,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasInvalidatedBy(id; e,-,-,attrs)</span>.
</li>
- <li><span class="name">actedOnBehalfOf(id;a2,a1,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">actedOnBehalfOf(id;a2,a1,-,attrs)</span>.
+ <li><span class="name">wasDerivedFrom(id; e2,e1,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasDerivedFrom(id; e2,e1,-,-,-,attrs)</span>.
+ </li>
+ <li><span class="name">wasAssociatedWith(id; e,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">wasAssociatedWith(id; e,-,-,attrs)</span>.
+ </li>
+ <li><span class="name">actedOnBehalfOf(id; a2,a1,attrs)</span> <span class="conditional">IF AND ONLY IF</span> <span class="name">actedOnBehalfOf(id; a2,a1,-,attrs)</span>.
</li>
</ol>
</div>
@@ -1249,11 +1251,11 @@
<div class="remark">
<!--<p>
Note that there is no expansion rule for <span class="name">wasDerivedFrom</span>. In a derivation of the form
- <span class="name">wasDerivedFrom(id;e1,e2,attr)</span>, the
+ <span class="name">wasDerivedFrom(id; e1,e2,attr)</span>, the
absence of the optional activity, generation and use identifiers
means that the derivation relationship may encompass multiple activities,
generations, and uses. Thus, it is not equivalent to <span
- class="name">wasDerivedFrom(id;e1,e2,a,g,u,attr)</span> where some
+ class="name">wasDerivedFrom(id; e1,e2,a,g,u,attr)</span> where some
activity, generation and use are given explicitly.
The short
form is not defined in terms of the long form in this case.</p>-->
@@ -1270,20 +1272,31 @@
class="name">-</span>) are, for the purpose of this document,
considered to be distinct, fresh existential variables. Thus,
before proceeding to apply other definitions or inferences, most
- occurrences of <span class="name">-</span> MUST be replaced
+ occurrences of <span class="name">-</span> are to be replaced
by fresh existential variables, distinct from any others occurring in
the instance.
- The only exceptions, where <span class="name">-</span> MUST be left
+ The only exceptions to this general rule, where <span
+ class="name">-</span> are to be left
in place, are the <a href="http://www.w3.org/TR/prov-dm/#derivation.activity">activity</a>, <a href="http://www.w3.org/TR/prov-dm/#derivation.generation">generation</a>, and <a href="http://www.w3.org/TR/prov-dm/#derivation.usage">usage</a> parameters in <span class="name">wasDerivedFrom</span> and
- the <a href="http://www.w3.org/TR/prov-dm/#association.plan">plan</a> parameter in <span class="name">wasAssociatedWith</span>.
+ the <a
+ href="http://www.w3.org/TR/prov-dm/#association.plan">plan</a>
+ parameter in <span class="name">wasAssociatedWith</span>.
</p>
- <p>The following table characterizes the <dfn>expandable
- parameter</dfn>s of the properties of PROV, needed in the
- following definition. For emphasis, the two optional parameters
+ <p>The treatment of optional parameters is specified formally using
+ the auxiliary concept of <dfn>expandable parameter</dfn>. An
+ expandable parameter is one that can be omitted using the
+ placeholder <span class="name">-</span>, and if so, it is
+ to be replaced by a fresh existential identifier.
+ <a href="#expandable-parameters-fig">Table 2</a> defines the <a>expandable
+ parameter</a>s of the properties of PROV, needed in <a class="rule-ref"
+href="#optional-placeholders"><span>TBD</span></a>. For emphasis, the four optional parameters
that are not <a title="expandable parameter">expandable</a> are
also listed.</p>
- <table class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
+ <div id="expandable-parameters-fig">
+ <table id="expandable-parameters" border="1" class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
+<caption id="expandable-parameters">Table 2: Expandable and
+ Non-Expandable Parameters</caption>
<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
<tr>
<th>Relation</th>
@@ -1291,66 +1304,67 @@
<th>Non-expandable</th>
</tr>
<tr >
- <td class="name">wasGeneratedBy(id;e,a,t,attrs)</td>
+ <td class="name">wasGeneratedBy(id; e,a,t,attrs)</td>
<td class="name">id,a,t</td>
<td></td>
</tr>
<tr>
- <td class="name">used(id;a,e,t,attrs)</td>
+ <td class="name">used(id; a,e,t,attrs)</td>
<td class="name">id,e,t</td>
<td></td>
</tr>
<tr>
- <td class="name">wasInformedBy(id;a2,a1,attrs)</td>
+ <td class="name">wasInformedBy(id; a2,a1,attrs)</td>
<td class="name">id</td>
<td></td>
</tr>
<tr>
- <td class="name">wasStartedBy(id;a2,e,a1,t,attrs)</td>
+ <td class="name">wasStartedBy(id; a2,e,a1,t,attrs)</td>
<td class="name">id,e,a1,t</td>
<td></td>
</tr>
<tr>
- <td class="name">wasEndedBy(id;a2,e,a1,t,attrs)</td>
+ <td class="name">wasEndedBy(id; a2,e,a1,t,attrs)</td>
<td class="name">id,e,a1,t</td>
<td></td>
</tr>
<tr>
- <td class="name">wasInvalidatedBy(id;e,a,t,attrs)</td>
+ <td class="name">wasInvalidatedBy(id; e,a,t,attrs)</td>
<td class="name">id,a,t</td>
<td></td>
</tr>
<tr>
- <td class="name">wasDerivedFrom(id;e2,e1,a,g2,u1,attrs)</td>
+ <td class="name">wasDerivedFrom(id; e2,e1,a,g2,u1,attrs)</td>
<td class="name">id</td>
<td class="name">a,g2,u1</td>
</tr>
<tr>
- <td class="name">wasDerivedFrom(id;e2,e1,attrs)</td>
- <td class="name">id</td>
- <td></td>
- </tr>
- <tr>
- <td class="name">wasAttributedTo(id;e,ag,attr)</td>
+ <td class="name">wasDerivedFrom(id; e2,e1,attrs)</td>
<td class="name">id</td>
<td></td>
</tr>
<tr>
- <td class="name">wasAssociatedWith(id;a,ag,pl,attrs)</td>
+ <td class="name">wasAttributedTo(id; e,ag,attr)</td>
+ <td class="name">id</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasAssociatedWith(id; a,ag,pl,attrs)</td>
<td class="name">id,ag</td>
<td class="name">pl</td>
</tr>
<tr>
- <td class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</td>
+ <td class="name">actedOnBehalfOf(id; ag2,ag1,a,attrs)</td>
<td class="name">id,a</td>
<td></td>
</tr>
<tr>
- <td class="name">wasInfluencedBy(id;e2,e1,attrs)</td>
+ <td class="name">wasInfluencedBy(id; e2,e1,attrs)</td>
<td class="name">id</td>
<td></td>
</tr>
</table>
+ </div>
<div class="definition" id="optional-placeholders">
<ol><li>
@@ -1391,15 +1405,15 @@
<div class="remark">
<p>In an association of the form
- <span class="name">wasAssociatedWith(id;a,ag,-,attr)</span>, the
+ <span class="name">wasAssociatedWith(id; a,ag,-,attr)</span>, the
absence of a plan means: either no plan exists, or a plan exists but
it is not identified. Thus, it is not equivalent to <span
- class="name">wasAssociatedWith(id;a,ag,p,attr)</span> where a
+ class="name">wasAssociatedWith(id; a,ag,p,attr)</span> where a
plan <span class="name">p</span> is given.</p>
</div>
<div class="remark">
<p> A derivation <span
- class="name">wasDerivedFrom(id;e2,e1,a,gen,use,attrs)</span> that
+ class="name">wasDerivedFrom(id; e2,e1,a,gen,use,attrs)</span> that
specifies an activity explicitly indicates that this activity achieved the derivation, with a usage <span
class="name">use</span> of entity <span
class="name">e1</span>, and a generation <span
@@ -1407,7 +1421,7 @@
class="name">e2</span>.
It differs from a derivation of the form
<span
- class="name">wasDerivedFrom(id;e2,e1,-,-,-,attrs)</span> with
+ class="name">wasDerivedFrom(id; e2,e1,-,-,-,attrs)</span> with
missing activity, generation, and usage. In the latter form, it is not specified
if one or more activities are involved in the derivation. </p>
@@ -1428,29 +1442,29 @@
<div class='inference' id='communication-generation-use-inference'>
<p>
<span class="conditional">IF</span>
-<span class="name">wasInformedBy(_id;a2,a1,_attrs)</span>
+<span class="name">wasInformedBy(_id; a2,a1,_attrs)</span>
holds <span class='conditional'>THEN</span>
there exist <span class="name">e</span>, <span
class="name">_id1</span>, <span class="name">_t1</span>, <span
class="name">_id2</span>, and <span class="name">_t2</span>,
-such that <span class="name">wasGeneratedBy(_id1;e,a1,_t1,[])</span> and <span class="name">used(_id2;a2,e,_t2,[])</span> hold.</p>
+such that <span class="name">wasGeneratedBy(_id1; e,a1,_t1,[])</span> and <span class="name">used(_id2; a2,e,_t2,[])</span> hold.</p>
</div>
<p id="generation-use-communication-inference_text">
<div class="note">
-A final check is required on this inference to ensure that it does not lead to non-termination, when combined with
+A final check is required on <a class="rule-text" href="#generation-use-communication-inference"><span>TBD</span></a> this to ensure that it does not lead to non-termination, when combined with
<a class="rule-text" href="#communication-generation-use-inference"><span>TBD</span></a>.
</div>
<div class='inference' id='generation-use-communication-inference'>
<p>
-<span class="conditional">IF</span> <span class="name">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span>
- and <span class="name">used(_id2;a2,e,_t2,_attrs2)</span> hold
+<span class="conditional">IF</span> <span class="name">wasGeneratedBy(_id1; e,a1,_t1,_attrs1)</span>
+ and <span class="name">used(_id2; a2,e,_t2,_attrs2)</span> hold
<span class='conditional'>THEN</span>
there exists <span
class="name">_id</span>
-such that <span class="name">wasInformedBy(_id;a2,a1,[])</span>
+such that <span class="name">wasInformedBy(_id; a2,a1,[])</span>
</p></div>
@@ -1512,7 +1526,7 @@
-->
<p id="entity-generation-invalidation-inference_text">
-From an entity, we can infer that existence of
+From an entity, we can infer the existence of
generation and invalidation events.
</p>
<div class='inference' id='entity-generation-invalidation-inference'>
@@ -1523,7 +1537,7 @@
<span class="name">_id1</span>, <span class="name">_a1</span>, <span class="name">_t1</span>,
<span class="name">_id2</span>, <span class="name">_a2</span>, and <span class="name">_t2</span> such that
<span
- class="name">wasGeneratedBy(_id1;e,_a1,_t1,[])</span> and <span class="name">wasInvalidatedBy(_id2;e,_a2,_t2,[])</span>.
+ class="name">wasGeneratedBy(_id1; e,_a1,_t1,[])</span> and <span class="name">wasInvalidatedBy(_id2; e,_a2,_t2,[])</span>.
</div>
@@ -1537,9 +1551,9 @@
</div>-->
<p id="activity-start-end-inference_text">
-From an activity statement, we can infer that
-start and end events having times matching the start and end times of
-the activity.
+From an activity statement, we can infer
+start and end events whose times match the start and end times of
+the activity, respectively.
</p>
<div class='inference' id='activity-start-end-inference'>
<p>
@@ -1548,43 +1562,43 @@
class="conditional">THEN</span> there exist <span class="name">_id1</span>, <span class="name">_e1</span>, <span class="name">_id2</span>,
and <span class="name">_e2</span> such that
<span
- class="name">wasStartedBy(_id1;a,_e1,_a1,t1,[])</span> and <span class="name">wasEndedBy(_id2;a,_e2,_a2,t2,[])</span>.
+ class="name">wasStartedBy(_id1; a,_e1,_a1,t1,[])</span> and <span class="name">wasEndedBy(_id2; a,_e2,_a2,t2,[])</span>.
</div>
<hr />
-<p id='wasStartedBy-inference_text'>Start of <span class="name">a</span> by trigger <span class="name">e1</span> and starter activity <span
-class="name">a1</span> implies that
-<span class="name">e1</span> was generated by <span
+<p id='wasStartedBy-inference_text'>The start of an activity <span
+class="name">a</span> triggered by entity <span class="name">e1</span>
+implies that
+<span class="name">e1</span> was generated by the starting activity <span
class="name">a1</span>.</p>
<div class='inference' id='wasStartedBy-inference'>
<p><span class='conditional'>IF</span>
- <span class="name">wasStartedBy(_id;a,e1,a1,_t,_attrs)</span>,
+ <span class="name">wasStartedBy(_id; a,e1,a1,_t,_attrs)</span>,
<span class='conditional'>THEN</span> there exist <span
class="name">_gen</span> and <span class="name">_t1</span>
such that
- <span class="name">wasGeneratedBy(_gen;e1,a1,_t1,[])</span>.</p>
+ <span class="name">wasGeneratedBy(_gen; e1,a1,_t1,[])</span>.</p>
</div>
<p>
<hr>
<p id='wasEndedBy-inference_text'>Likewise,
-end of <span class="name">a</span> by trigger <span class="name">e1</span> and ender activity <span
-class="name">a1</span> implies that
-<span class="name">e1</span> was generated by <span
+the ending of activity <span class="name">a</span> by triggering entity <span class="name">e1</span> implies that
+<span class="name">e1</span> was generated by the ending activity <span
class="name">a1</span>.
</p>
<div class='inference' id='wasEndedBy-inference'>
<p><span class='conditional'>IF</span>
- <span class="name">wasEndedBy(_id;a,e1,a1,_t,_attrs)</span>,
+ <span class="name">wasEndedBy(_id; a,e1,a1,_t,_attrs)</span>,
<span class='conditional'>THEN</span> there exist <span
class="name">_gen</span> and <span class="name">_t1</span> such that
- <span class="name">wasGeneratedBy(_gen;e1,a1,_t1,[])</span>.</p>
+ <span class="name">wasGeneratedBy(_gen; e1,a1,_t1,[])</span>.</p>
</div>
@@ -1606,25 +1620,25 @@
<ol>
<li><span class='conditional'>IF</span> <span
- class="name">wasDerivedFrom(_id;e2,e1,a,id2,_id1,_attrs)</span>,
+ class="name">wasDerivedFrom(_id; e2,e1,a,id2,_id1,_attrs)</span>,
<span class='conditional'>THEN</span> there exists <span
class="name">_t2</span>
- such that <span class="name">wasGeneratedBy(id2;e2,a,_t2,[])</span>.
+ such that <span class="name">wasGeneratedBy(id2; e2,a,_t2,[])</span>.
<li><span class='conditional'>IF</span> <span
- class="name">wasDerivedFrom(_id;e2,e1,a,_id2,id1,_attrs)</span>,
+ class="name">wasDerivedFrom(_id; e2,e1,a,_id2,id1,_attrs)</span>,
<span class='conditional'>THEN</span> there exists <span
class="name">_t1</span>
- such that <span class="name">used(id1;a,e1,_t1,[])</span>.
+ such that <span class="name">used(id1; a,e1,_t1,[])</span>.
</ol>
-->
<p>
<span class='conditional'>IF</span> <span
- class="name">wasDerivedFrom(_id;e2,e1,a,id2,id1,_attrs)</span>,
+ class="name">wasDerivedFrom(_id; e2,e1,a,gen2,use1,_attrs)</span>,
<span class='conditional'>THEN</span> there exists <span
class="name">_t1</span> and <span
class="name">_t2</span> such that <span
-class="name">used(id1;a,e1,_t1,[])</span> and <span
-class="name">wasGeneratedBy(id2;e2,a,_t2,[])</span>.
+class="name">used(use1; a,e1,_t1,[])</span> and <span
+class="name">wasGeneratedBy(gen2; e2,a,_t2,[])</span>.
</p>
</div>
<p>
@@ -1636,11 +1650,11 @@
<div class='inference' id='derivation-use'>
<p>
-<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(id;e2,e1,a,-,-,attrs)</span> and <span class="name">wasGeneratedBy(gen;e2,a,_t2,_attrs2)</span> hold, <span
+<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(id; e2,e1,a,-,-,attrs)</span> and <span class="name">wasGeneratedBy(gen; e2,a,_t2,_attrs2)</span> hold, <span
class='conditional'>THEN</span> there exist <span
class="name">_t1</span> and <span class="name">use</span> such
- that <span class="name">used(use;a,e1,_t1,[])</span> and <span
- class="name">wasDerivedFrom(id;e2,e1,a,gen,use,attrs)</span>.
+ that <span class="name">used(use; a,e1,_t1,[])</span> and <span
+ class="name">wasDerivedFrom(id; e2,e1,a,gen,use,attrs)</span>.
</div>
<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity
(see <a class="rule-text" href="#unique-generation"><span>TBD</span></a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
@@ -1654,12 +1668,12 @@
<p> However, a derivation without explicit generation and usage cannot be normalized even when a generation and usage hold.
<span class='conditional'>IF</span>
-<span class="name">wasDerivedFrom(id;e2,e1,a,-,-,attrs)</span>,
-<span class="name">wasGeneratedBy(gen;e2,a,_t2,_attrs2)</span>,
-and <span class="name">used(use;a,e1,_t1,[])</span>, <span
+<span class="name">wasDerivedFrom(id; e2,e1,a,-,-,attrs)</span>,
+<span class="name">wasGeneratedBy(gen; e2,a,_t2,_attrs2)</span>,
+and <span class="name">used(use; a,e1,_t1,[])</span>, <span
class='conditional'>IT IS NOT NECESSARILY THE CASE THAT</span>
<span
- class="name">wasDerivedFrom(id;e2,e1,a,gen,use,attrs)</span>.
+ class="name">wasDerivedFrom(id; e2,e1,a,gen,use,attrs)</span>.
Indeed,
<span
class="name">e1</span> may be used multiple times by
@@ -1681,9 +1695,9 @@
<div class='inference' id='specific-derivation-inference'>
<p><span class='conditional'>IF</span> <span
- class="name">wasDerivedFrom(id;e2,e1,_act,_gen,_use,attrs)</span>,
+ class="name">wasDerivedFrom(id; e2,e1,_act,_gen,_use,attrs)</span>,
<span class='conditional'>THEN</span> <span
- class="name">wasDerivedFrom(id;e2,e1,-,-,-,attrs)</span>.
+ class="name">wasDerivedFrom(id; e2,e1,-,-,-,attrs)</span>.
</p>
</div>
@@ -1695,13 +1709,13 @@
<div class='inference' id='revision-is-alternate'>
<p>
<span class='conditional'>IF</span> <span
- class="name">wasDerivedFrom(_id;e2,e1,[prov:type='prov:Revision'])</span>
+ class="name">wasDerivedFrom(_id; e2,e1,[prov:type='prov:Revision'])</span>
holds, <span class='conditional'>THEN</span> <span
class="name">alternateOf(e2,e1)</span> holds.
</p>
<!--
<li><span class='conditional'>IF</span> <span
- class="name">wasDerivedFrom(_id;e2,e1,_act,_gen,_use,[prov:type='prov:Revision'])</span>
+ class="name">wasDerivedFrom(_id; e2,e1,_act,_gen,_use,[prov:type='prov:Revision'])</span>
holds, <span class='conditional'>THEN</span> <span
class="name">alternateOf(e2,e1)</span> holds.
</li>
@@ -1754,7 +1768,7 @@
<div class='inference' id='attribution-inference'>
<p>
<span class='conditional'>IF</span>
-<span class="name">wasAttributedTo(_att;e,ag,_attrs)</span> holds for some identifiers
+<span class="name">wasAttributedTo(_att; e,ag,_attrs)</span> holds for some identifiers
<span class="name">e</span> and <span class="name">ag</span>,
<span class='conditional'>THEN</span> there exist
<span class="name">a</span>,
@@ -1763,8 +1777,8 @@
<span class="name">_assoc</span>,
<span class="name">_pl</span>,
such that
-<span class="name">wasGeneratedBy(_gen;e,a,_t,[])</span> and
-<span class="name">wasAssociatedWith(_assoc;a,ag,_pl,[])</span> hold.
+<span class="name">wasGeneratedBy(_gen; e,a,_t,[])</span> and
+<span class="name">wasAssociatedWith(_assoc; a,ag,_pl,[])</span> hold.
</p>
</div>
<hr />
@@ -1778,12 +1792,12 @@
<div class='inference' id='delegation-inference'>
<p>
<span class='conditional'>IF</span>
-<span class="name">actedOnBehalfOf(_id;ag1, ag2, a, _attrs)</span>
+<span class="name">actedOnBehalfOf(_id; ag1, ag2, a, _attrs)</span>
<span class='conditional'>THEN</span> there exist <span
class="name">_id1</span>, <span class="name">_pl1</span>, <span
class="name">_id2</span>, and <span class="name">_pl2</span> such that <span
- class="name">wasAssociatedWith(_id1;a, ag1, _pl1, [])</span>
- and <span class="name">wasAssociatedWith(_id2;a, ag2, _pl2, [])</span>.
+ class="name">wasAssociatedWith(_id1; a, ag1, _pl1, [])</span>
+ and <span class="name">wasAssociatedWith(_id2; a, ag2, _pl2, [])</span>.
</p>
</div>
@@ -1809,35 +1823,35 @@
<p>
<ol>
<li>
- <span class="conditional">IF</span> <span class="name">wasGeneratedBy(id;e,a,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasGeneratedBy(id; e,a,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">used(id;a,e,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, e, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">used(id; a,e,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, e, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasInformedBy(id;a2,a1,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, a1, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasInformedBy(id; a2,a1,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, a1, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasStartedBy(id;a2,e,a1,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasStartedBy(id; a2,e,a1,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasEndedBy(id;a2,e,a1,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasEndedBy(id; a2,e,a1,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasInvalidatedBy(id;e,a,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasInvalidatedBy(id; e,a,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasDerivedFrom(id; e2, e1, attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e2, e1, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasDerivedFrom(id; e2, e1, attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e2, e1, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasAttributedTo(id;e,ag,attr)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, ag, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasAttributedTo(id; e,ag,attr)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, ag, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasAssociatedWith(id;a,ag,pl,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, ag, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasAssociatedWith(id; a,ag,pl,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, ag, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; ag2, ag1, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; ag2, ag1, attrs)</span>.
</li>
</ol>
</div>
@@ -1899,8 +1913,8 @@
<p id="specialization-transitive_text">
Similarly, specialization is a
<a>strict partial order</a>: it is <a>irreflexive</a> and
- <a>transitive</a>. Irreflexivity is handled later as a
- constraint.
+ <a>transitive</a>. Irreflexivity is handled later as <a class="rule-ref"
+href="#impossible-specialization-reflexive"><span>TBD</span></a>
</p>
<div class='inference' id="specialization-transitive">
<p>
@@ -2067,7 +2081,9 @@
</li>
<li>If merging fails, then the constraint
is unsatisfiable, so application of the constraint to <span class="math">I</span>
- fails.</li>
+ fails. If this failure occurs during <a>normalization</a> prior to
+validation, then <span class="math">I</span> is invalid, as explained in <a href="#normalization-validity-equivalence">Section 6</a>.
+ </li>
<li>If merging succeeds with a substitution <span class="math">S</span>, then
<span class="math">S</span> is applied to the instance <span class="math">I</span>, yielding result <span class="math">I(S)</span>.</li>
</ol>
@@ -2081,15 +2097,15 @@
class="constraint-example" id="key-example">
<p>The <span
class="name">a<sub>k</sub></span> field is a <span class="conditional">KEY</span> for relation <span
- class="name">r(a<sub>0</sub>;a<sub>1</sub>,...,a<sub>n</sub>)</span>. </p></div>
+ class="name">r(a<sub>0</sub>; a<sub>1</sub>,...,a<sub>n</sub>)</span>. </p></div>
<p> Because of the presence of attributes, key constraints do not
reduce directly to uniqueness constraints. Instead, we enforce key
constraints as follows. </p>
<ol>
<li> Suppose <span
- class="name">r(a<sub>0</sub>;a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> and <span
- class="name">r(b<sub>0</sub>;b<sub>1</sub>,...b<sub>n</sub>,attrs2)</span> hold in PROV instance <span class="math">I</span>, where the key fields <span
+ class="name">r(a<sub>0</sub>; a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> and <span
+ class="name">r(b<sub>0</sub>; b<sub>1</sub>,...b<sub>n</sub>,attrs2)</span> hold in PROV instance <span class="math">I</span>, where the key fields <span
class="name">a<sub>k</sub> = b<sub>k</sub></span> are equal.</li>
<li> Attempt to merge all of the corresponding parameters <span
class="name">a<sub>0</sub> = b<sub>0</sub> </span> and ... and <span
@@ -2099,10 +2115,10 @@
application of the key constraint to <span class="math">I</span> fails.
</li>
<li>If merging succeeds with substitution <span class="math">S</span>, then we remove <span
- class="name">r(a<sub>0</sub>;a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> and <span
- class="name">r(b<sub>0</sub>;b<sub>1</sub>,...b<sub>n</sub>,attrs2)</span> from <span class="math">I</span>, obtaining
+ class="name">r(a<sub>0</sub>; a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> and <span
+ class="name">r(b<sub>0</sub>; b<sub>1</sub>,...b<sub>n</sub>,attrs2)</span> from <span class="math">I</span>, obtaining
instance <span class="math">I'</span>, and return instance <span
- class="name">{r(S(a<sub>0</sub>);S(a<sub>1</sub>),...S(a<sub>n</sub>),attrs1 ∪
+ class="name">{r(S(a<sub>0</sub>); S(a<sub>1</sub>),...S(a<sub>n</sub>),attrs1 ∪
attrs2)}</span> ∪ <span class="math">S(I')</span>.
</ol>
@@ -2143,50 +2159,52 @@
</div>
<hr />
- <p id='key-properties_text'> Likewise, we assume that the identifiers
- of relationships in PROV uniquely identify the corresponding statements a PROV instance, through
- the following key constraints:
+ <p id='key-properties_text'> Likewise, the statements
+in a valid PROV instance must provide consistent information about
+ each identified object or relationship. The following key
+ constraints require that all of the information about each identified
+ statement can be merged into a single, consistent statement:
</p>
<div class='constraint' id='key-properties'>
<p><ol>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasGeneratedBy(id;e,a,t,attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">used(id;a,e,t,attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasInformedBy(id;a2,a1,attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasStartedBy(id;a2,e,a1,t,attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasEndedBy(id;a2,e,a1,t,attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasInvalidatedBy(id;e,a,t,attrs)</span> statement.
+ the <span class="name">wasGeneratedBy(id; e,a,t,attrs)</span> statement.
</li>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasDerivedFrom(id; e2, e1, attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasDerivedFrom(id; e2, e1, a, g2, u1, attrs)</span> statement.
+ the <span class="name">used(id; a,e,t,attrs)</span> statement.
</li>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasAttributedTo(id;e,ag,attr)</span> statement.
+ the <span class="name">wasInformedBy(id; a2,a1,attrs)</span> statement.
</li>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasAssociatedWith(id;a,ag,pl,attrs)</span> statement.
+ the <span class="name">wasStartedBy(id; a2,e,a1,t,attrs)</span> statement.
</li>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasAssociatedWith(id;a,ag,-,attrs)</span> statement.
+ the <span class="name">wasEndedBy(id; a2,e,a1,t,attrs)</span> statement.
</li>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span> statement.
+ the <span class="name">wasInvalidatedBy(id; e,a,t,attrs)</span> statement.
</li>
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
- the <span class="name">wasInfluencedBy(id;o2,o1,attrs)</span> statement.
+ the <span class="name">wasDerivedFrom(id; e2, e1, attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">wasDerivedFrom(id; e2, e1, a, g2, u1, attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">wasAttributedTo(id; e,ag,attr)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">wasAssociatedWith(id; a,ag,pl,attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">wasAssociatedWith(id; a,ag,-,attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">wasInfluencedBy(id; o2,o1,attrs)</span> statement.
</li>
</ol>
</div>
@@ -2208,8 +2226,8 @@
<div class='constraint' id='unique-generation'>
<p>
-<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(id1;e,_a1,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(id2;e,_a2,_t2,_attrs2)</span>,
-<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>.</p>
+<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(id1; e,_a1,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(id2; e,_a2,_t2,_attrs2)</span>,
+<span class='conditional'>THEN</span> <span class="name">id1</span> = <span class="name">id2</span>.</p>
</div>
<hr>
@@ -2218,8 +2236,8 @@
<div class='constraint' id='unique-invalidation'>
<p>
-<span class='conditional'>IF</span> <span class="name">wasInvalidatedBy(id1;e,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(id2;e,_a2,_t2,_attrs2)</span>,
-<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>.</p>
+<span class='conditional'>IF</span> <span class="name">wasInvalidatedBy(id1; e,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(id2; e,_a2,_t2,_attrs2)</span>,
+<span class='conditional'>THEN</span> <span class="name">id1</span> = <span class="name">id2</span>.</p>
</div>
@@ -2241,10 +2259,10 @@
<div class='constraint' id='unique-wasStartedBy'>
<p>
<span class='conditional'>IF</span> <span
- class="name">wasStartedBy(id1;a,_e1,_a1,_t1,_attrs1)</span> and <span
- class="name">wasStartedBy(id2;a,_e2,_a2,_t2,_attrs2)</span>, <span
- class='conditional'>THEN</span> <span class="name">id</span>=<span
- class="name">id'</span>.</p>
+ class="name">wasStartedBy(id1; a,_e1,_a1,_t1,_attrs1)</span> and <span
+ class="name">wasStartedBy(id2; a,_e2,_a2,_t2,_attrs2)</span>, <span
+ class='conditional'>THEN</span> <span class="name">id1</span> = <span
+ class="name">id2</span>.</p>
</div>
<hr />
@@ -2253,10 +2271,10 @@
<div class='constraint' id='unique-wasEndedBy'>
<p>
<span class='conditional'>IF</span> <span
- class="name">wasEndedBy(id1;a,_e1,_a1,_t1,_attrs1)</span> and <span
- class="name">wasEndedBy(id2;a,_e2,_a2,_t2,_attrs2)</span>, <span
- class='conditional'>THEN</span> <span class="name">id</span>=<span
- class="name">id'</span>.</p>
+ class="name">wasEndedBy(id1; a,_e1,_a1,_t1,_attrs1)</span> and <span
+ class="name">wasEndedBy(id2; a,_e2,_a2,_t2,_attrs2)</span>, <span
+ class='conditional'>THEN</span> <span class="name">id1</span> = <span
+ class="name">id2</span>.</p>
</div>
@@ -2271,7 +2289,7 @@
<div class='constraint' id='unique-startTime'>
<p>
-<span class='conditional'>IF</span> <span class="name">activity(a,t,_t',_attrs)</span> and <span class="name">wasStartedBy(id;a,_e1,_a1,t1,_attrs1)</span>, <span class='conditional'>THEN</span> <span class="name">t</span>=<span class="name">t1</span>.</p>
+<span class='conditional'>IF</span> <span class="name">activity(a,t,_t',_attrs)</span> and <span class="name">wasStartedBy(id; a,_e1,_a1,t1,_attrs1)</span>, <span class='conditional'>THEN</span> <span class="name">t</span>=<span class="name">t1</span>.</p>
</div>
<hr>
@@ -2283,7 +2301,7 @@
<p>
<span class='conditional'>IF</span> <span
class="name">activity(a,_t,t',_attrs)</span> and <span
- class="name">wasEndedBy(id;a,_e1,_a1,t1,_attrs1)</span>, <span
+ class="name">wasEndedBy(id; a,_e1,_a1,t1,_attrs1)</span>, <span
class='conditional'>THEN</span> <span class="name">t'</span> = <span class="name">t1</span>.</p>
</div>
@@ -2461,9 +2479,9 @@
<div class='constraint' id='start-precedes-end'>
<p>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span>
+<span class="name">wasEndedBy(end; a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -2480,9 +2498,9 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">used(use;a,e,_t,_attrs)</span>
+<span class="name">used(use; a,e,_t,_attrs)</span>
and
-<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -2490,9 +2508,9 @@
</li>
<li>
<span class="conditional">IF</span>
-<span class="name">used(use;a,e,_t,_attrs)</span>
+<span class="name">used(use; a,e,_t,_attrs)</span>
and
-<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasEndedBy(end; a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">use</span>
<a title="precedes">precedes</a>
@@ -2513,9 +2531,9 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen;_e,a,_t,_attrs)</span>
+<span class="name">wasGeneratedBy(gen; _e,a,_t,_attrs)</span>
and
-<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -2523,9 +2541,9 @@
</li>
<li>
<span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen;_e,a,_t,_attrs)</span>
+<span class="name">wasGeneratedBy(gen; _e,a,_t,_attrs)</span>
and
-<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasEndedBy(end; a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -2552,11 +2570,11 @@
<div class='constraint' id='wasInformedBy-ordering'>
<p>
<span class="conditional">IF</span>
-<span class="name">wasInformedBy(_id;a2,a1,_attrs)</span>
+<span class="name">wasInformedBy(_id; a2,a1,_attrs)</span>
and
-<span class="name">wasStartedBy(start;a1,_e1,_a1',_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; a1,_e1,_a1',_t1,_attrs1)</span>
and
-<span class="name">wasEndedBy(end;a2,_e2,_a2',_t2,_attrs2)</span>
+<span class="name">wasEndedBy(end; a2,_e2,_a2',_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -2581,9 +2599,9 @@
<div class='constraint' id='wasStartedByActivity-ordering'>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start2;a2,-,a1,-)</span>
+<span class="name">wasStartedBy(start2; a2,-,a1,-)</span>
and
-<span class="name">wasStartedBy(start1;a1,-,-,-)</span>
+<span class="name">wasStartedBy(start1; a1,-,-,-)</span>
<span class="conditional">THEN</span>
<span class="name">start1</span>
<a title="precedes">strictly precedes</a>
@@ -2601,8 +2619,8 @@
<p>
As with activities, entities have lifetimes: they are generated, then
-can be used, revised, or other entities can be derived from them, and
-finally they may be invalidated. The constraints on these events are
+can be used, other entities can be derived from them, and finally they
+can be invalidated. The constraints on these events are
illustrated graphically in <a href="#ordering-entity">Figure 3</a> and
<a href="#ordering-entity-trigger">Figure 4</a>.
</p>
@@ -2629,9 +2647,9 @@
<div class='constraint' id='generation-precedes-invalidation'>
<p>
<span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen;e,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -2651,9 +2669,9 @@
<div class='constraint' id='generation-precedes-usage'>
<p> <span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen;e,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span>
and
-<span class="name">used(use;_a2,e,_t2,_attrs2)</span>
+<span class="name">used(use; _a2,e,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -2669,9 +2687,9 @@
<div class='constraint' id='usage-precedes-invalidation'>
<p>
<span class="conditional">IF</span>
-<span class="name">used(use;_a1,e,_t1,_attrs1)</span>
+<span class="name">used(use; _a1,e,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">use</span>
<a title="precedes">precedes</a>
@@ -2698,7 +2716,7 @@
<div class='constraint' id='derivation-usage-generation-ordering'>
<p>
<span class="conditional">IF</span>
-<span class="name">wasDerivedFrom(_d;_e2,_e1,_a,gen2,use1,_attrs)</span>
+<span class="name">wasDerivedFrom(_d; _e2,_e1,_a,gen2,use1,_attrs)</span>
<span class="conditional">THEN</span>
<span class="name">use1</span>
<a title="precedes">strictly precedes</a>
@@ -2718,11 +2736,11 @@
id='derivation-generation-generation-ordering'>
<p>
<span class="conditional">IF</span>
-<span class="name">wasDerivedFrom(_d;e2,e1,attrs)</span>
+<span class="name">wasDerivedFrom(_d; e2,e1,attrs)</span>
and
-<span class="name">wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen1; e1,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span>
+<span class="name">wasGeneratedBy(gen2; e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen1</span>
<a title="precedes">strictly precedes</a>
@@ -2747,18 +2765,18 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start;_a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; _a,e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasGeneratedBy(gen;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasGeneratedBy(gen; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
<span class="name">start</span>.
</li><li>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start;_a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; _a,e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -2779,18 +2797,18 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasEndedBy(end;_a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasEndedBy(end; _a,e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasGeneratedBy(gen;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasGeneratedBy(gen; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
<span class="name">end</span>.
</li><li>
<span class="conditional">IF</span>
-<span class="name">wasEndedBy(end;_a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasEndedBy(end; _a,e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">end</span>
<a title="precedes">precedes</a>
@@ -2799,7 +2817,7 @@
</ol>
</div>
-<div style="text-align: center;">
+<div style="text-align: center; ">
<figure id="ordering-entity-trigger">
<img src="images/constraints/ordering-entity-trigger.png" alt="ordering constraints for trigger entities" />
<br>
@@ -2809,15 +2827,16 @@
<hr />
<p id="specialization-generation_text">
-If an entity specalizes another, then its generation must follow the
-specialized entity's generation.
+If an entity is a specialization of another, then the more
+specific entity must have been generated after the
+less specific entity was generated.
</p>
<div class="constraint" id="specialization-generation">
<p>
<span class="conditional">IF</span> <span
class="name">specializationOf(e2,e1)</span> and <span
- class="name">wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1)</span> and
- <span class="name">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span>
+ class="name">wasGeneratedBy(gen1; e1,_a1,_t1,_attrs1)</span> and
+ <span class="name">wasGeneratedBy(gen2; e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span> <span class="name">gen1</span> <a>precedes</a> <span class="name">gen2</span>.
</div>
@@ -2825,15 +2844,17 @@
<hr />
<p id="specialization-invalidation_text">
-Similarly, if an entity specalizes another, then its invalidation must follow the
-specialized entity's invalidation.
+Similarly, if an entity is a specialization of another entity, and
+then
+the invalidation event of the more specific entity precedes that of
+the less specific entity.
</p><div class="constraint" id="specialization-invalidation">
<p>
<span class="conditional">IF</span> <span
- class="name">specializationOf(e2,e1)</span> and <span
- class="name">wasInvalidatedBy(inv1;e1,_a1,_t1,_attrs1)</span> and
- <span class="name">wasInvalidatedBy(inv2;e2,_a2,_t2,_attrs2)</span>
- <span class="conditional">THEN</span> <span class="name">inv2</span> <a>precedes</a> <span class="name">inv1</span>.
+ class="name">specializationOf(e1,e2)</span> and <span
+ class="name">wasInvalidatedBy(inv2; e2,_a2,_t2,_attrs2)</span> and
+ <span class="name">wasInvalidatedBy(inv1; e1,_a1,_t1,_attrs1)</span>
+ <span class="conditional">THEN</span> <span class="name">inv1</span> <a>precedes</a> <span class="name">inv2</span>.
</p>
</div>
@@ -2842,13 +2863,15 @@
<section>
<h3> Agent constraints</h3>
-<p>
-Like entities and activities, agents have lifetimes that follow a
-familiar pattern: an agent is generated, can participate in
-interactions such as starting, ending or association with an
-activity, attribution, or delegation, and finally the agent is invalidated.
-</p>
-<p>Further constraints associated with agents appear in <a href="#ordering-agents">Figure 5</a> and are discussed below.</p>
+<p> Like entities and activities, agents have lifetimes that follow a
+familiar pattern. An agent that is also an entity can be generated
+and invalidated; an agent that is also an activity can be started or
+ended. During its lifetime, an agent can participate in interactions
+such as starting or ending other activities, association with an
+activity, attribution, or delegation.
+
+</p> <p>Further constraints associated with agents appear in <a
+ href="#ordering-agents">Figure 5</a> and are discussed below.</p>
<div style="text-align: center;">
<figure id="ordering-agents-fig">
@@ -2871,22 +2894,22 @@
<div class='constraint' id='wasAssociatedWith-ordering'>
<ol> <li>
<span class="conditional">IF</span>
-<span class="name">wasAssociatedWith(_assoc;a,ag,_pl,_attrs)</span>
+<span class="name">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span>
and
-<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; ag,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
<span class="name">inv</span>.
</li><li>
<span class="conditional">IF</span>
-<span class="name">wasAssociatedWith(_assoc;a,ag,_pl,_attrs)</span>
+<span class="name">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span>
and
-<span class="name">wasGeneratedBy(gen;ag,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; ag,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span>
+<span class="name">wasEndedBy(end; a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -2912,22 +2935,22 @@
<div class='constraint' id='wasAttributedTo-ordering'>
<ol> <li>
<span class="conditional">IF</span>
-<span class="name">wasAttributedTo(_at;e,ag,_attrs)</span>
-and
-<span class="name">wasGeneratedBy(gen;e,_a1,_t1,_attrs1)</span>
+<span class="name">wasAttributedTo(_at; e,ag,_attrs)</span>
and
-<span class="name">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span>
+<span class="name">wasGeneratedBy(gen2; e,_a2,_t2,_attrs2)</span>
+and
+<span class="name">wasInvalidatedBy(inv1; ag,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
-<span class="name">gen</span>
+<span class="name">gen1</span>
<a title="precedes">precedes</a>
-<span class="name">inv</span>.
+<span class="name">inv2</span>.
</li><li>
<span class="conditional">IF</span>
-<span class="name">wasAttributedTo(_at;e,ag,_attrs)</span>
+<span class="name">wasAttributedTo(_at; e,ag,_attrs)</span>
and
-<span class="name">wasGeneratedBy(gen;ag,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; ag,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -2944,11 +2967,11 @@
<div class='constraint' id='actedOnBehalfOf-ordering'>
<p> <span class="conditional">IF</span>
-<span class="name">actedOnBehalfOf(_del;ag2,ag1,_a,_attrs)</span>
+<span class="name">actedOnBehalfOf(_del; ag2,ag1,_a,_attrs)</span>
and
-<span class="name">wasGeneratedBy(gen;ag1,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; ag1,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv;ag2,_a2,_t2,_attrs2)</span>
+<span class="name">wasInvalidatedBy(inv; ag2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -3032,11 +3055,11 @@
<span class="name">wasAttributedTo</span>,
<span class="name">wasAssociatedWith</span>,
<span class="name">actedOnBehalfOf</span>} such that <span class="name">r</span> and <span class="name">s</span>
- are different relations, the
+ are different relation names, the
following constraint holds:
</p>
<p>
- <span class="conditional">IF</span> <span class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> and <span class="name">s(id;b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
+ <span class="conditional">IF</span> <span class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>)</span> and <span class="name">s(id; b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
</p>
</div>
@@ -3051,8 +3074,8 @@
</p>
<div class='constraint' id='impossible-object-property-overlap'>
<p>
-For each <span class="name">r</span> in <span class="name">entity</span>, <span class="name">activity</span>
- or <span class="name">agent</span> and for each <span class="name">s</span> in {
+For each <span class="name">p</span> in <span class="name">entity</span>, <span class="name">activity</span>
+ or <span class="name">agent</span> and for each <span class="name">r</span> in {
<span class="name">used</span>,
<span class="name">wasGeneratedBy</span>,
<span class="name">wasInvalidatedBy</span>,
@@ -3066,8 +3089,8 @@
<span class="name">actedOnBehalfOf</span>}, the following
impossibility constraint holds:</p>
-<p> <span class="conditional">IF</span> <span class="name">r(id,a<sub>1</sub>,...,a<sub>n</sub>)</span> and
- <span class="name">s(id;b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
+<p> <span class="conditional">IF</span> <span class="name">p(id,a<sub>1</sub>,...,a<sub>n</sub>)</span> and
+ <span class="name">r(id; b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
</p>
</div>
@@ -3093,9 +3116,11 @@
<p>To check if a PROV instance satisfies type constraints, one obtains the types of identifiers by application of
<a class="rule-ref" href="#typing"><span>TBD</span></a>
-and check no impossibility results from rules
+and check that none of the impossibility constraints
<a class="rule-ref" href="#entity-activity-disjoint"><span>TBD</span></a> and
-<a class="rule-ref" href="#membership-empty-collection"><span>TBD</span></a>.</p>
+<a class="rule-ref"
+ href="#membership-empty-collection"><span>TBD</span></a> are
+ violated as a result.</p>
<div class='constraint' id="typing">
@@ -3104,7 +3129,7 @@
<ul>
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasGeneratedBy(gen;e,a,t,attrs)</span>
+ <span class='name'>wasGeneratedBy(gen; e,a,t,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'entity' ∈ typeOf(e)</span> AND
<span class="name">'activity' ∈ typeOf(a)</span>.
@@ -3130,7 +3155,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>used(u;a,e,t,attrs)</span>
+ <span class='name'>used(u; a,e,t,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'activity' ∈ typeOf(a)</span> AND
<span class="name">'entity' ∈ typeOf(e)</span>.
@@ -3139,7 +3164,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasInformedBy(id;a2,a1,attrs)</span>
+ <span class='name'>wasInformedBy(id; a2,a1,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'activity' ∈ typeOf(a2)</span> AND
<span class="name">'activity' ∈ typeOf(a1)</span>.
@@ -3147,7 +3172,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasStartedBy(id;a2,e,a1,t,attrs)</span>
+ <span class='name'>wasStartedBy(id; a2,e,a1,t,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'activity' ∈ typeOf(a2)</span> AND
<span class="name">'entity' ∈ typeOf(e)</span> AND
@@ -3159,7 +3184,7 @@
<span class='conditional'>IF</span>
- <span class='name'>wasEndedBy(id;a2,e,a1,t,attrs)</span>
+ <span class='name'>wasEndedBy(id; a2,e,a1,t,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'activity' ∈ typeOf(a2)</span> AND
<span class="name">'entity' ∈ typeOf(e)</span> AND
@@ -3169,7 +3194,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasInvalidatedBy(id;e,a,t,attrs)</span>
+ <span class='name'>wasInvalidatedBy(id; e,a,t,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'entity' ∈ typeOf(e)</span> AND
<span class="name">'activity' ∈ typeOf(a)</span>.
@@ -3179,7 +3204,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasDerivedFrom(id; e2, e1, a, g2, u1, attrs)</span>
+ <span class='name'>wasDerivedFrom(id; e2, e1, a, g2, u1, attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'entity' ∈ typeOf(e2)</span> AND
<span class="name">'entity' ∈ typeOf(e1)</span> AND
@@ -3188,7 +3213,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasAttributedTo(id;e,ag,attr)</span>
+ <span class='name'>wasAttributedTo(id; e,ag,attr)</span>
<span class='conditional'>THEN</span>
<span class="name">'entity' ∈ typeOf(e)</span> AND
<span class="name">'agent' ∈ typeOf(ag)</span>.
@@ -3196,7 +3221,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasAssociatedWith(id;a,ag,pl,attrs)</span>
+ <span class='name'>wasAssociatedWith(id; a,ag,pl,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'activity' ∈ typeOf(a)</span> AND
<span class="name">'agent' ∈ typeOf(ag)</span> AND
@@ -3207,7 +3232,7 @@
<li>
<span class='conditional'>IF</span>
- <span class='name'>actedOnBehalfOf(id;ag2,ag1,a,attrs)</span>
+ <span class='name'>actedOnBehalfOf(id; ag2,ag1,a,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'agent' ∈ typeOf(ag2)</span> AND
<span class="name">'agent' ∈ typeOf(ag1)</span> AND
@@ -3279,8 +3304,13 @@
<span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
</div>
<div class="remark">
- Note that there is no disjointness between entities and agents. This is because one might want to make statements about the provenance of an agent, by making it an entity.
- Therefore, users MAY assert both <span class="name">entity(a1)</span> and <span class="name">agent(a1)</span> in a valid PROV instance.
+ There is no disjointness between entities and agents. This is because one might want to make statements about the provenance of an agent, by making it an entity.
+ Therefore, users MAY assert both <span
+ class="name">entity(a1)</span> and <span
+ class="name">agent(a1)</span> in a valid PROV instance.
+ Similarly, there is no disjointness between activities and
+ agents, and it is possbile to assert that an object is both an
+ activity and an agent in a valid PROV instance.
<!-- However, it is RECOMMENDED that users refrain from using the same identifier for an entity and an agent unless they refer to the same thing. -->
</div>