--- a/model/prov-constraints.html Fri Oct 26 13:22:18 2012 +0100
+++ b/model/prov-constraints.html Fri Oct 26 13:40:56 2012 +0100
@@ -554,7 +554,7 @@
<a title="valid">validity</a>. Equivalence of two PROV
instances can be determined by comparing their normal forms. For PROV
documents, validity and equivalence amount to checking the validity or
-pairwise equivalence of their respective documents.
+pairwise equivalence of their respective instances.
</p>
<p>
This document outlines an algorithm for validity checking based on
@@ -1379,8 +1379,11 @@
notion of equivalence of normal forms is <em>isomorphism</em>. Two
instances <span class="math">I<sub>1</sub></span> and <span class="math">I<sub>2</sub></span> are <em>isomorphic</em> if there is an invertible
substitution <span class="math">S</span> mapping existential variables to existential variables such that <span class="math">S(I<sub>1</sub>) = I<sub>2</sub></span>.
+<!--
This is similar to the notion of equivalence used in [[RDF]], where
- blank nodes play an analogous role to existential variables. </p>
+ blank nodes play an analogous role to existential variables.
+ -->
+ </p>
<p>Equivalence can be checked by normalizing instances, checking that
both instances are valid, then
@@ -1398,15 +1401,21 @@
<h4>From Instances to Bundles and Documents</h4>
<p>PROV documents can contain multiple instances: a <a>toplevel
-instance</a> consisting of the set of statements not appearing within a bundle, and
-zero or more named instances called <a>bundle</a>s. For the purpose
+instance</a>, and
+zero or more additional, named instances called <a>bundle</a>s. For the purpose
of inference and constraint checking, these instances are treated independently. That is,
a PROV document is valid provided that each instance in it is valid
-and the names of its bundles are distinct. Similarly, a PROV document is
+and the names of its bundles are distinct. In other words, there are
+no validity constraints that need to be checked across the different
+instances in a PROV document; the contents of one instance in a
+multi-instance PROV document cannot affect the validity of another instance.
+Similarly, a PROV document is
equivalent to another if their toplevel instances are equivalent, they
have the same number of bundles with the same names, and the instances
-of their corresponding bundles are equivalent. Analogously to blank nodes in
-[[RDF]], the scope of an existential variable in PROV is the instance
+of their corresponding bundles are equivalent.
+<!--Analogously to blank nodes in
+[[RDF]],-->
+The scope of an existential variable in PROV is delimited at the instance
level, so existential variables with the same name occurring in
different instances do not necessarily denote the same term. This
is a consequence of the fact that the instances of two equivalent
@@ -1808,7 +1817,9 @@
identifiers might later be found to be equal to known identifiers;
they play a similar role in PROV constraints to existential
variables in logic, to "labeled nulls" in database theory
- [[DBCONSTRAINTS]], or to blank nodes in [[!RDF]]. In general, omitted optional parameters to
+ [[DBCONSTRAINTS]].
+ <!--, or to blank nodes in [[!RDF]].-->
+ In general, omitted optional parameters to
[[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
@@ -1822,8 +1833,11 @@
should be viewed as existentially quantified variables, meaning that
through subsequent reasoning steps they may turn out to be equal to
other identifiers that are already known, or to other existentially
- quantified variables. Their treatment is analogous to that of blank
- nodes in RDF. In contrast, distinct URIs or literal values in PROV
+ quantified variables.
+ <!--
+ Their treatment is analogous to that of blank
+ nodes in RDF.-->
+ In contrast, distinct URIs or literal values in PROV
are assumed to be distinct for the purpose of checking validity or
inferences. This issue is discussed in more detail under <a
href="#uniqueness-constraints">Uniqueness Constraints</a>.
@@ -2952,14 +2966,14 @@
</p>
<div class='constraint' id='key-object'>
<p><ol>
- <li>The identifier field <span class="name">e</span> is a <span class="conditional">KEY</span> for
- the <span class="name">entity(e,attrs)</span> statement.
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">entity(id,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">a</span> is a <span class="conditional">KEY</span> for
- the <span class="name">activity(a,t1,t2,attrs)</span> statement.
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">activity(id,t1,t2,attrs)</span> statement.
</li>
-<li>The identifier field <span class="name">ag</span> is a <span class="conditional">KEY</span> for
- the <span class="name">agent(ag,attrs)</span> statement.
+<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
+ the <span class="name">agent(id,attrs)</span> statement.
</li>
</ol>
</div>
@@ -3208,7 +3222,7 @@
orders: we say <span class="name">e1</span> <dfn>strictly precedes</dfn> <span
class="name">e2</span> to indicate that <span class="name">e1</span>
happened before <span class="name">e2</span>, but not at the same time. This is a
-<a>transitive</a> relation. </p>
+<a>transitive</a>, <a>irreflexive</a> relation. </p>
<p>PROV also allows for time observations to be inserted in
@@ -3926,7 +3940,7 @@
<p>
<hr />
-<p id='actedOnBehalfOf-ordering_text'>For delegation, two agents need to have some overlap in their lifetime.</p>
+<p id='actedOnBehalfOf-ordering_text'>For delegation, the responsible agent has to precede or have some overlap with the subordinate agent.</p>
<div class='constraint' id='actedOnBehalfOf-ordering'>