updates to constraints document
authorLuc Moreau <l.moreau@ecs.soton.ac.uk>
Wed, 18 Apr 2012 22:49:59 +0100
changeset 2374 9655ef6e2063
parent 2373 b95c519598d5
child 2375 79639d7957a4
updates to constraints document
model/working-copy/wd5-prov-dm-constraints-revised.html
--- a/model/working-copy/wd5-prov-dm-constraints-revised.html	Wed Apr 18 13:11:21 2012 -0400
+++ b/model/working-copy/wd5-prov-dm-constraints-revised.html	Wed Apr 18 22:49:59 2012 +0100
@@ -1,7 +1,7 @@
 <!DOCTYPE html>
 
 <html><head> 
-    <title>PROV-DM Part II: Constraints of the Provenance Data Model</title> 
+    <title>Constraints of the Provenance Data Model</title> 
     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> 
     <!-- 
       === NOTA BENE ===
@@ -81,7 +81,7 @@
           specStatus:           "ED",
           
           // the specification's short name, as in http://www.w3.org/TR/short-name/
-          shortName:            "prov-dm-constraints",
+          shortName:            "prov-constraints",
  
           // if your specification has a subtitle that goes below the main
           // formal title, define it here
@@ -155,15 +155,21 @@
 
     <section id="abstract">
 <p>
-PROV-DM, the PROV data model, is a data model for provenance that
-describes the entities, people and activities involved in producing a
-piece of data or thing. PROV-DM is structured in six components,
-dealing with: (1) entities and activities, and the time at which they
-were created, used, or ended; (2) agents bearing responsibility for activities; (3) derivations between entities; (4) properties to link entities that refer to a same thing; (5) collections of entities, whose provenance can itself be tracked; (6) a simple annotation mechanism.</p>
+PROV-DM, the PROV data model, is a data model for provenance that describes
+the entities, people and activities involved in
+producing a piece of data or thing. 
+PROV-DM is structured in six components, dealing with: 
+(1) entities and activities, and the time at which they were created, used, or ended;
+(2) agents bearing responsibility for entities that were generated and activities that happened;
+(3) derivations of entities from entities;
+(4) properties to link entities that refer to a same thing;
+(5) collections forming a logical structure for its members;
+(6) a simple annotation mechanism.
+</p>
 
 
 <p> This document introduces a further set of concepts useful for
-  understanding the PROV-DM data model and defines <i>inferences</i>
+  understanding the PROV data model and defines <i>inferences</i>
   that are allowed on provenance descriptions and <i>validity
   constraints</i> that well-structured provenance descriptions should
   follow. These inferences and constraints are useful for readers who
@@ -174,36 +180,35 @@
 
 <section id="sotd">
 <h4>PROV Family of Specifications</h4>
-This document is part of the PROV family of specifications, a set of specifications aiming to define the various aspects that are necessary to achieve the vision of inter-operable
-interchange of provenance information in heterogeneous environments such as the Web.  The specifications are as follows.
+This document is part of the PROV family of specifications, a set of specifications defining various aspects that are necessary to achieve the vision of inter-operable
+interchange of provenance information in heterogeneous environments such as the Web.  The specifications are:
 <ul>
-<li> PROV-DM, the PROV data model for provenance,</li>
-<li> PROV-DM-CONSTRAINTS, a set of constraints applying to the PROV data model  (this document),</li>
-<li> PROV-N, a notation for provenance aimed at human consumption,</li>
+<li> PROV-DM, the PROV data model for provenance;</li>
+<li> PROV-CONSTRAINTS, a set of constraints applying to the PROV data model  (this document);</li>
+<li> PROV-N, a notation for provenance aimed at human consumption;</li>
 <li> PROV-O, the PROV ontology, an OWL-RL ontology allowing the mapping of PROV to RDF;</li>
 <li> PROV-AQ, the mechanisms for accessing and querying provenance; </li>
-<li> PROV-PRIMER, a primer for the PROV data model,</li>
-<li> PROV-SEM, a formal semantics for the PROV data model.</li>
+<li> PROV-PRIMER, a primer for the PROV data model;</li>
+<li> PROV-SEM, a formal semantics for the PROV data model;</li>
 <li> PROV-XML, an XML schema for the PROV data model.</li>
 </ul>
 <h4>How to read the PROV Family of Specifications</h4>
 <ul>
-<li>The primer is the entry point to PROV offering a pedagogical presentation of the provenance model.</li>
-<li>The Linked Data and Semantic Web community should focus on PROV-O defining PROV classes and properties specified in an OWL-RL ontology. For further details, PROV-DM and PROV-DM-CONSTRAINTS specify the constraints applicable to the data model, and its interpretation. PROV-SEM provides a mathematical semantics.</li>
-<li>The XML community should focus on PROV-XML defining an XML schema for PROV-DM. Further details can also be found in PROV-DM, PROV-DM-CONSTRAINTS, and PROV-SEM.</li>
-<li>Developers seeking to retrieve or publish provenance should focus of PROV-AQ.</li>
+<li>The primer is the entry point to PROV offering an introduction to the provenance model.</li>
+<li>The Linked Data and Semantic Web community should focus on PROV-O defining PROV classes and properties specified in an OWL-RL ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify the constraints applicable to the data model, and its interpretation. PROV-SEM provides a mathematical semantics.</li>
+<li>The XML community should focus on PROV-XML defining an XML schema for PROV-DM. Further details can also be found in PROV-DM, PROV-CONSTRAINTS, and PROV-SEM.</li>
+<li>Developers seeking to retrieve or publish provenance should focus on PROV-AQ.</li>
 <li>Readers seeking to implement other PROV serializations
-should focus on PROV-DM and PROV-DM-CONSTRAINTS.  PROV-O, PROV-N, PROV-XML offer examples of mapping to RDF, text, and XML, respectively.</li>
+should focus on PROV-DM and PROV-CONSTRAINTS.  PROV-O, PROV-N, PROV-XML offer examples of mapping to RDF, text, and XML, respectively.</li>
 </ul>
 
-
-<h4>Fourth Public Working Draft</h4>
- <p>This is the fourth public release of the PROV-DM
+<h4>First Public Working Draft</h4>
+ <p>This is the first public release of the PROV-CONSTRAINTS
 document. Following feedback, the Working Group has decided to
-reorganize this document substantially, separating the data model,
+reorganize the PROV-DM document substantially, separating the data model,
 from its constraints, and the notation used to illustrate it. The
-PROV-DM release is synchronized with the release of the PROV-O,
-PROV-PRIMER, PROV-N, PROV-DM-CONSTRAINTS documents.
+PROV-CONSTRAINTS release is synchronized with the release of the PROV-DM, PROV-O,
+PROV-PRIMER, and PROV-N documents.
 </p>
 </section>
 
@@ -214,10 +219,10 @@
       <h2>Introduction<br>
 </h2> 
 
-<p> Provenance records describe the people, institutions,
+<p> Provenance is a record that describes the people, institutions,
   entities, and activities, involved in producing, influencing, or
-  delivering a piece of data or a thing.  This document is part of a
-  specification [[PROV-DM]] that defines a data model for
+  delivering a piece of data or a thing.  This document complements
+  the PROV-DM specification [[PROV-DM]] that defines a data model for
   provenance on the Web.  </p>
 
 <!-- Commented out since seems redundant -- jcheney
@@ -229,7 +234,7 @@
 <li>A data model for provenance, which is presented in three documents:
 <ul>
 <li> PROV-DM (part I): the provenance data model itself, expressed in natural language  [[PROV-DM]];
-<li> PROV-DM-CONSTRAINTS (part II): inferences and constraints on
+<li> PROV-CONSTRAINTS (part II): inferences and constraints on
   valid PROV-DM data (this document);
 <li> PROV-N (part III): a notation to express instances of that data model for human consumption [[PROV-N]];
 </ul> 
@@ -285,18 +290,18 @@
 <h3>Purpose of this document</h3>
 
 <p>
-PROV-DM specifies a data model for provenance (realizable using
-PROV-N, PROV-RDF, or PROV-XML).  However, nothing in PROV-DM part 1
-forces such provenance data to be meaningful, that is, to correspond
+PROV-DM is a conceptual data model for provenance (realizable using
+PROV-N, PROV-RDF, or PROV-XML).  However, nothing in the PROV-DM specification [[PROV-DM]] forces PROV
+descriptions to be meaningful, that is, to correspond
 to a consistent history of objects and interactions.  Furthermore,
-nothing in PROV-DM part 1 enables applications to perform standard
-inferences over provenance information.  
+nothing in the PROV-DM specification enables applications to perform 
+inferences over provenance descriptions.  
 </p>
 
-<p> This document specifies <em>inferences</em> over PROV-DM data that
+<p> This document specifies <em>inferences</em> over PROV descriptions that
 applications MAY employ, including definitions of some provenance
-expressions in terms of others, and also defines a class of <em>valid</em>
-PROV-DM data by specifying <em>constraints</em> that valid PROV-DM data must
+descriptions in terms of others, and also defines a class of <em>valid</em>
+PROV descriptions by specifying <em>constraints</em> that valid PROV descriptions must
 satisfy. Applications SHOULD produce valid provenance and
 MAY reject provenance that is not valid in order to increase
 the usefulness of provenance and reliability of applications that
@@ -308,24 +313,26 @@
 class="sectionRef"></a>), and then
 considers two kinds of validity constraints (<a href="#constraints"
 class="sectionRef"></a>): <em>structural constraints</em> that
-prescribe properties of PROV-DM instances that can be checked directly
+prescribe properties of <dfn title="PROV instance">PROV instances</dfn> that can be checked directly
 by inspecting the syntax, and <em>event ordering</em> constraints that
-require that the records in a PROV-DM instance are consistent with a
+require that the records in a <a>PROV instance</a> are consistent with a
 sensible ordering of events relating the activities, entities and
 agents involved.  In separate sections we consider additional
 constraints specific to collections and accounts (<a
  href="#collection-constraints" class="sectionRef"></a> and <a
  href="#account-constraints" class="sectionRef"></a>).  </p>
 
+<div class="note">Question to James: The term 'PROV Instance' seems to have a precise meaning. I read this as a PROV Description Set. Should we define it? Every where it occurs, there is a link to its first occurrence.</div>
+
 <p>
 The specification also describes how the inferences, definitions, and
 constraints should be used (<a href="#compliance"
-class="sectionRef"></a>).  Briefly, a PROV-DM compliant application is
-allowed (but not required) to treat two PROV-DM instances as the same
+class="sectionRef"></a>).  Briefly, a PROV compliant application is
+allowed (but not required) to treat two <a title="PROV instance">PROV instances</a> as the same
 if they are equal after applying the inference rules and possibly
-reordering expressions, and we can define a canonical form for PROV-DM
-instances obtained by applying all possible inference rules.  In
-addition, a validating PROV-DM application is required to check that
+reordering expressions, and we can define a canonical form for <a title="PROV instance">PROV
+instances</a> obtained by applying all possible inference rules.  In
+addition, a validating PROV application is required to check that
 the constraints are satisfied in (the normal form of) provenance data generated or consumed by the application.
 </p>
 
@@ -342,7 +349,7 @@
 <section id="audience">
 <h3> Audience </h3>
 
-<p> The audience for PROV-DM-CONSTRAINTS is the same as for PROV-DM: developers
+<p> The audience for this document is the same as for [[PROV-DM]]: developers
 and users who wish to create, process, share or integrate provenance
 records on the (Semantic) Web.  Not all PROV-compliant applications
 need to check validity when processing provenance, but many
@@ -365,11 +372,11 @@
 <h2>Inferences and Definitions</h2>
 
 <p>
-In this section we describe <a title="inference">inferences</a> and <a title="definition">definitions</a> that MAY be used on
+In this section, we describe <a title="inference">inferences</a> and <a title="definition">definitions</a> that MAY be used on
   provenance data, and a notion of <a
-title="equivalence">equivalence</a> on PROV-DM instances.  
+title="equivalence">equivalence</a> on <a title="PROV instance">PROV instances</a>.  
 An  <dfn id="inference">inference</dfn> is a rule that can be applied
-  to PROV-DM to add new provenance expressions.  A <dfn
+  to PROV descriptions to add new provenance expressions.  A <dfn
   id="definition">definition</dfn> is a rule that states that a
   provenance expression is equivalent to some other expressions; thus,
   defined provenance expressions can be replaced by their definitions,
@@ -378,14 +385,14 @@
 
 <p> Inferences have the following general form:
 <div class='inference' id='inference-example'>
-  <span class='conditional'>IF</span> hyp_1 and ... and
-hyp_k <span class='conditional'>THEN</span> there exists a_1,..., a_m such that conclusion_1 ... conclusion_n.
+  <span class='conditional'>IF</span> <span class="name">hyp_1</span> and ... and
+<span class="name">hyp_k</span> <span class='conditional'>THEN</span> there exists <span class="name">a_1</span>,..., <span class="name">a_m</span> such that <span class="name">conclusion_1</span> ... <span class="name">conclusion_n</span>.
   </div>
 
-  This means that if provenance expressions matching hyp_1... hyp_k
-  can be found in a PROV-DM instance, we can add the expressions
-  concl_1 ... concl_n to the instance, possibly after generating fresh
-  identifiers a_1,...,a_m for unknown objects.  These fresh
+  This means that if provenance expressions matching <span class="name">hyp_1</span>... <span class="name">hyp_k</span>
+  can be found in a <a>PROV instance</a>, we can add the expressions
+  <span class="name">concl_1</span> ... <span class="name">concl_n</span> to the instance, possibly after generating fresh
+  identifiers <span class="name">a_1</span>,...,<span class="name">a_m</span> for unknown objects.  These fresh
   identifiers might later be found to be equal to known identifiers;
   they play a similar role in PROV-DM to existential variables in logic.
 </p>
@@ -397,26 +404,26 @@
 
 <p> Definitions have the following general form:
 <div class='definition' id='definition-example'>
-  defined_exp holds <span class='conditional'>IF AND ONLY IF </span>
-  there exists a_1,..., a_m such that defining_exp_1 ... defining_exp_n.
+  <span class="name">defined_exp</span> holds <span class='conditional'>IF AND ONLY IF </span>
+  there exists <span class="name">a_1</span>,..., <span class="name">a_m</span> such that <span class="name">defining_exp_1</span> ... <span class="name">defining_exp_n</span>.
   </div>
 
   This means that a provenance expression defined_exp is defined in
   terms of other expressions.  This can be viewed as a two-way
-  inference:  If defined_exp
-  can be found in a PROV-DM instance, we can add the expressions
-defining_exp_1 ... defining_exp_n to the instance, possibly after generating fresh
-  identifiers a_1,...,a_m for unknown objects.  Conversely, if there
-  exist identifiers a_1...a_m such that defining_exp_1
-  ... defining_exp_n hold in the instance, we can add the defined
-  expression def_exp.  When an expression is defined in terms of
+  inference:  If <span class="name">defined_exp</span>
+  can be found in a <a>PROV instance</a>, we can add the expressions
+<span class="name">defining_exp_1</span> ... <span class="name">defining_exp_n</span> to the instance, possibly after generating fresh
+  identifiers <span class="name">a_1</span>,...,<span class="name">a_m</span> for unknown objects.  Conversely, if there
+  exist identifiers <span class="name">a_1</span>...<span class="name">a_m</span> such that <span class="name">defining_exp_1</span>
+  ... <span class="name">defining_exp_n</span> hold in the instance, we can add the defined
+  expression <span class="name">def_exp</span>.  When an expression is defined in terms of
   others, it is in a sense redundant; it is safe to replace it with
   its definition.
 </p>
   
 <p>Applications that process provenance MAY use these definitions or
 inferences.  Moreover, they SHOULD apply all applicable inferences
-before determining whether an instance of PROV-DM is <a
+before determining whether an <a>PROV instance</a> is <a
  title="valid">valid</a>.  In particular, applications that generate
 provenance SHOULD check that the generated provenance is valid even if
 some of these inferences or definitions are applied to it by another
@@ -586,6 +593,7 @@
  each other.
 </p>
 
+
   <div class="note">
   Motivation for quotation inference
   </div>
@@ -822,7 +830,7 @@
 
 
   For the purpose of checking inferences and constraints, we define a
-notion of <a>equivalence</a> of PROV-DM instances.  Equivalence is
+notion of <a>equivalence</a> of <a title="PROV instance">PROV instances</a>.  Equivalence is
 has the following characteristics:
 
 
@@ -834,13 +842,13 @@
   <li> Redundant expressions are merged according to uniqueness
   constraints. </li>
   <li>
-  The order of provenance expressions is irrelevant to the meaning of a PROV-DM instance.  That is, a
-  PROV-DM instance is equivalent to any other instance obtained by
+  The order of provenance expressions is irrelevant to the meaning of a <a>PROV instance</a>.  That is, a
+  <a>PROV instance</a> is equivalent to any other instance obtained by
   permuting its expressions.
   </li>
   <li>
-  Inference rules and definitions preserve equivalence.  That is, a PROV-DM
-  instance is equivalent to the instance obtained by applying any
+  Inference rules and definitions preserve equivalence.  That is, a <a>PROV
+  instance</a> is equivalent to the instance obtained by applying any
   inference rule.
   </li>
   <li>Equivalence is reflexive, symmetric, and transitive.</li>
@@ -894,10 +902,10 @@
 
 
 <p>
-We define the <dfn>normal form</dfn> of a PROV-DM instance as the set
+We define the <dfn>normal form</dfn> of a <a>PROV instance</a> as the set
 of provenance expressions resulting from merging all of the overlapping
 expressions in the instance and applying all possible inference rules
-to this set.  Formally, we say that two PROV-DM instances are
+to this set.  Formally, we say that two <a title="PROV instance">PROV instances</a> are
 <dfn>equivalent</dfn> if they have the same normal form (that is,
 after applying all possible inference rules, the two instances produce
 the same set of PROV-DM expressions.)
@@ -926,19 +934,18 @@
 
 
 <p>
-This section defines a collection of constraints on instances of
-  PROV-DM.  An instance of PROV-DM is <dfn id="dfn-valid">valid</dfn>
+This section defines a collection of constraints on <a title="PROV instance">PROV instances</a>.  An <a>PROV instance</a> is <dfn id="dfn-valid">valid</dfn>
   if, after applying all possible inference and definition rules from
   <a href="#inferences">Section 2</a>, the resulting instance
   satisfies all of the constraints specified in this section.
-  Applications that process PROV-DM data SHOULD check that the data
+  Applications that process PROV descriptions SHOULD check that the data
   they generate is <a title="valid">valid</a> and MAY reject input
   provenance data that is not <a title="valid">valid</a>.
   </p>
 
   <p> There are two kinds of constraints:
-  <ul><li><em>uniqueness constraints</em> that say that a PROV-DM
-  instance can contain at most one expression or that multiple
+  <ul><li><em>uniqueness constraints</em> that say that a <a>PROV
+  instance</a> can contain at most one expression or that multiple
   expressions about the same objects need to have the same values (for
   example, if we describe the same generation event twice, then the
   two expressions should have the same times);
@@ -946,13 +953,13 @@
     <li> and <em>event ordering constraints</em> that say that it
   should be possible to arrange the 
   events (generation, usage, invalidation, start, end) described in a
-  PROV-DM instance into a partial order that corresponds to a sensible
+  <a>PROV instance</a> into a partial order that corresponds to a sensible
   "history" (for example, an entity should not be generated after it
   is used).
     </li>
     </ul>
 
-<p>The PROV-DM data model is implicitly based on a notion of <dfn
+<p>The PROV data model is implicitly based on a notion of <dfn
   id="dfn-event">instantaneous event</dfn>s (or just <a
   title="instantaneous event">event</a>s), that mark
 transitions in the world.  Events include generation, usage, or
@@ -987,7 +994,7 @@
 </div>
 
   <p> We assume that the various identified objects of PROV-DM have
-  unique expressions describing them within a PROV-DM instance.
+  unique expressions describing them within a <a>PROV instance</a>.
   </p>
   <div class='constraint' id='entity-unique'>
 <p>Given an entity identifier <span class="name">e</span>, there is at
@@ -1332,15 +1339,15 @@
 the activity denoted by <span class="name">a2</span>.
   -->
     <span class="conditional">IF</span>
-<span class="name">wasStartedBy(a2,a1)</span> 
+<span class="name">wasStartedByActivity(a2,a1)</span> 
 and
 <span class="name">wasStartedBy(start1,a1,-,-)</span> 
 and
 <span class="name">wasStartedBy(start2,a2,-,-)</span> 
 <span class="conditional">THEN</span>
-<span class="name">start</span> 
+<span class="name">start1</span> 
 <a>precedes</a>
-<span class="name">end</span>.
+<span class="name">start2</span>.
 
 </div>
 
@@ -1446,9 +1453,9 @@
        <span class="conditional">IF</span>
 <span class="name">wasDerivedFrom(d,e2,e1,a,g2,u1,-)</span> 
 <span class="conditional">THEN</span>
-<span class="name">g2</span> 
+<span class="name">u1</span> 
 <a>precedes</a>
-<span class="name">u1</span>.  
+<span class="name">g2</span>.  
 
 </div>
 <hr />
@@ -1485,6 +1492,82 @@
 which implies ordering ordering between the usage of <span class="name">e1</span> and
 generation of <span class="name">e2</span>.  </p>
 
+<hr />
+
+<p>The entity that triggered the start of an activity must exist before the activity starts.
+This is
+illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (a) and  expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
+
+
+<div class='constraint' id='wasStartedBy-ordering'>
+<!--Given an activity denoted by <span class="name">a</span> and an entity
+denoted by   <span class="name">e</span>, <span class='conditional'>IF</span>  <span
+class="name">wasStartedBy(a,e)</span>
+ holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
+<a title="activity start event">start</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
+<a>precedes</a> the invalidation event of 
+the same entity.-->
+
+  <ol>
+    <li>
+    <span class="conditional">IF</span>
+<span class="name">wasStartedBy(start,a,e,-)</span> 
+and
+<span class="name">wasGeneratedBy(gen,e,-,-)</span> 
+<span class="conditional">THEN</span>
+<span class="name">gen</span> 
+<a>precedes</a>
+<span class="name">start</span>.
+  </li><li>
+    <span class="conditional">IF</span>
+<span class="name">wasStartedBy(start,a,e,-)</span> 
+and
+<span class="name">wasInvalidatedBy(inv,e,-,-)</span> 
+<span class="conditional">THEN</span>
+<span class="name">start</span> 
+<a>precedes</a>
+<span class="name">inv</span>.
+  </li>
+  </ol>
+</div>
+<hr />
+
+<p> Similarly,  the entity that triggered the end of an activity must exist before the activity ends, as illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (b).</p> 
+
+
+<div class='constraint' id='wasEndedBy-ordering'>
+  <!--
+Given an activity denoted by <span class="name">a</span> and an entity denoted by   <span class="name">e</span>, <span class='conditional'>IF</span>  <span
+class="name">wasEndedBy(a,e)</span>
+ holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
+<a title="activity end event">end</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
+<a>precedes</a> the invalidation event of 
+the same entity.-->
+  <ol>
+      <li>
+    <span class="conditional">IF</span>
+<span class="name">wasEndedBy(end,a,e,-)</span> 
+and
+<span class="name">wasGeneratedBy(gen,e,-,-)</span> 
+<span class="conditional">THEN</span>
+<span class="name">gen</span> 
+<a>precedes</a>
+<span class="name">end</span>.
+  </li><li>
+    <span class="conditional">IF</span>
+<span class="name">wasEndedBy(end,a,e,-)</span> 
+and
+<span class="name">wasInvalidatedBy(inv,e,-,-)</span> 
+<span class="conditional">THEN</span>
+<span class="name">end</span> 
+<a>precedes</a>
+<span class="name">inv</span>.
+  </li>
+  </ol>
+</div>
+
+
+
 </section>
 
 <section>
@@ -1507,89 +1590,6 @@
 
 <hr />
 
-<p>The agent that started an activity must exist before the activity starts.
-This is
-illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (a) and  expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
-
-
-<div class='constraint' id='wasStartedBy-ordering'>
-<!--Given an activity denoted by <span class="name">a</span> and an entity
-denoted by   <span class="name">e</span>, <span class='conditional'>IF</span>  <span
-class="name">wasStartedBy(a,e)</span>
- holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
-<a title="activity start event">start</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
-<a>precedes</a> the invalidation event of 
-the same entity.-->
-
-  <ol>
-    <li>
-    <span class="conditional">IF</span>
-<span class="name">wasStartedBy(a,e)</span> 
-and
-<span class="name">wasStartedBy(start,a,-,-)</span> 
-and
-<span class="name">wasGeneratedBy(gen,e,-,-)</span> 
-<span class="conditional">THEN</span>
-<span class="name">gen</span> 
-<a>precedes</a>
-<span class="name">start</span>.
-  </li><li>
-    <span class="conditional">IF</span>
-<span class="name">wasStartedBy(a,e)</span> 
-and
-<span class="name">wasStartedBy(start,a,-,-)</span> 
-and
-<span class="name">wasInvalidatedBy(inv,e,-,-)</span> 
-<span class="conditional">THEN</span>
-<span class="name">start</span> 
-<a>precedes</a>
-<span class="name">inv</span>.
-  </li>
-  </ol>
-</div>
-<hr />
-
-<p> Similarly, if an agent is associated with an activity then the
-agent must exist before the activity starts and persist until the
-activity ends, as illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (b).</p>
-
-
-<div class='constraint' id='wasEndedBy-ordering'>
-  <!--
-Given an activity denoted by <span class="name">a</span> and an entity denoted by   <span class="name">e</span>, <span class='conditional'>IF</span>  <span
-class="name">wasEndedBy(a,e)</span>
- holds, <span class='conditional'>THEN</span> the following ordering constraints hold: the
-<a title="activity end event">end</a> event of the activity  denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
-<a>precedes</a> the invalidation event of 
-the same entity.-->
-  <ol>
-      <li>
-    <span class="conditional">IF</span>
-<span class="name">wasEndedBy(a,e)</span> 
-and
-<span class="name">wasEndedBy(end,a,-,-)</span> 
-and
-<span class="name">wasGeneratedBy(gen,e,-,-)</span> 
-<span class="conditional">THEN</span>
-<span class="name">gen</span> 
-<a>precedes</a>
-<span class="name">end</span>.
-  </li><li>
-    <span class="conditional">IF</span>
-<span class="name">wasEndedBy(a,e)</span> 
-and
-<span class="name">wasEndedBy(end,a,-,-)</span> 
-and
-<span class="name">wasInvalidatedBy(inv,e,-,-)</span> 
-<span class="conditional">THEN</span>
-<span class="name">end</span> 
-<a>precedes</a>
-<span class="name">inv</span>.
-  </li>
-  </ol>
-</div>
-
-<hr />
 
 <p>An activity that was associated with an agent must have some overlap with the agent. The agent may be generated, or may only become associated with the activity, after the activity start: so, the agent is required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start.
 This is
@@ -2009,9 +2009,8 @@
   <ul><li>When processing provenance obtained from another source, an
     application MAY apply the inferences and definitions in <a
     href="#inferences" class='sectionRef'></a>.</li>
-    <li>An application SHOULD process <a>equivalent</a> PROV-DM
-  instances in the same way, described in <a href="#equivalence" class="sectionRef"></a>
-    <li>When determining whether a PROV-DM instance is <a>valid</a>, an
+    <li>An application SHOULD process <a>equivalent</a> PROV-DM instances in the same way, described in <a href="#equivalence" class="sectionRef"></a>
+    <li>When determining whether a <a>PROV instance</a> is <a>valid</a>, an
     application MUST check that all of the
     constraints of <a href="#constraints" class="sectionRef"></a> are
   satisfied  on the <a>normal form</a> of the instance.</li>
@@ -2019,7 +2018,7 @@
     use, the application SHOULD produce <a>valid</a> provenance. </li>
   </ul>
   <div class="note">
-    Should we specify a way for PROV-DM instances to say whether they
+    Should we specify a way for <a title="PROV instance">PROV instances</a> to say whether they
     are meant to be validated or not?  Seems outside the scope of this document.
   </div>