* addressed most of Tim's comments
authorJames Cheney <jcheney@inf.ed.ac.uk>
Mon, 06 Aug 2012 20:04:37 +0100
changeset 4280 b6c650475879
parent 4279 24b3fc3f7907
child 4281 03321d46ee14
* addressed most of Tim's comments
model/comments/issue-459-tim.txt
model/prov-constraints.html
--- a/model/comments/issue-459-tim.txt	Mon Aug 06 18:35:01 2012 +0100
+++ b/model/comments/issue-459-tim.txt	Mon Aug 06 20:04:37 2012 +0100
@@ -518,10 +518,8 @@
    > relation?
    > 
 
-To address Stian's comment, since the only one of these thre relations
-(activity) can actually have "-"
-arguments anyway, we just say the two instances of the generic rule.
-This also addresses this comment.
+Done, sort of.  (I prefer "p" to "o", since "p" is more tereotypical as a
+relation name.)
 
    > 
    > 
@@ -555,6 +553,13 @@
    > 
    > (perhaps pull the Remark up to before the table?)
    > 
+
+This comment is just meant to describe what is said more
+systematically in the table: only the plan and activity (and now,
+generation and use) parameters are non-expandable.  Revised to say
+this.  I think it is better for the remarks to go after the definition 
+so that we explain what is going on first and then talk about it.
+
    > 
    > 29)
    > 
@@ -563,6 +568,9 @@
    > 
    > needs borders, a table #, and an anchor to it.
    > 
+
+Done.
+
    > 
    > 
    > 30)
@@ -574,6 +582,9 @@
    > if so, must be given an existential identifier? 
    > 
    > 
+
+Done, added explanation.
+
    > 
    > 
    > 
@@ -585,6 +596,12 @@
    > 
    > 
    > 
+
+To address Stian's similar comment, since the only one of these thre
+relations (activity) can actually have "-" arguments anyway, we just
+say the two instances of the generic rule. This also addresses this
+comment.
+
    > 
    > 
    > 32)
@@ -618,12 +635,18 @@
    > since one is usually trying to "read past it".
    > 
    > 
+
+Done.  (It wasn't fun!)
+
    > 
    > 34)
    > 
    > Thank you for flagging the irrelevant variables with underscores.
    > 
    > 
+
+You're welcome
+
    > 
    > 
    > 35)
@@ -636,6 +659,9 @@
    > 
    > is not situated well.
    > 
+
+Fixed, by adding references to both inferences
+
    > 
    > 
    > 36)
@@ -647,6 +673,9 @@
    > "This inference" - the one above or below
    > 
    > 
+
+See above
+
    > 
    > 
    > 37)
@@ -659,6 +688,9 @@
    > 
    > 
    > 
+
[email protected]: This requires changing the figure and the text in tandem...
+
    > 
    > 38)
    > 
@@ -670,6 +702,9 @@
    > "From an entity, we can infer the existence of generation and invalidation events."
    > 
    > 
+
+Fixed
+
    > 
    > 
    > 39)
@@ -678,6 +713,9 @@
    > 
    > "From an activity statemen,t"
    > 
+
+Fixed
+
    > 
    > 
    > 40)
@@ -693,6 +731,9 @@
    > also, "having times" seems odd.
    > 
    > 
+
+fixed
+
    > 
    > 41)
    > 
@@ -705,6 +746,10 @@
    > "The start of an activity a by trigger e1 implies that e1 was generated by starting activity a1."
    > 
    > 
+
+
+Done
+
    > 
    > same with:
    > 
@@ -713,6 +758,9 @@
    > "Likewise, end of activity a by trigger e1 and ender activity a1 implies that e1 was generated by a1."
    > 
    > 
+
+Fixed
+
    > 
    > 
    > 42)
@@ -728,6 +776,9 @@
    > makes it easier to know what type it is.
    > 
    > 
+
+Done
+
    > 
    > 
    > 43)
@@ -736,6 +787,15 @@
    > 
    > "the fact that the entity denoted by e2 is generated by at most one activity"
    > 
+
+It follows from other constraints (unique-generation and the key
+constraint for generation) that there is at most one generating
+activity.  We don't have a way to say that an activity is a
+sub-activity of another (and say that both participated in a
+generation event simultaneously).  This may be a limitation of PROV,
+but this is outside the scope of PROV-CONSTRAINTS.  Perhaps thisis an
+argument against imposing unique-generation.
+
    > 
    > 
    > 44)
@@ -766,7 +826,7 @@
    > 
    > 
 
-This is ISSUE-452.
+This is ISSUE-452.  @TODO
 
    > 
    > 46)
@@ -796,6 +856,9 @@
    > irreflexive and transitive. Irreflexivity is handled later as a
    > constraint." 
    > 
+
+Done
+
    > 
    > 48)
    > 
@@ -806,6 +869,14 @@
    > with instance I. 
    > 
    > 
+
+I wanted to avoid forward references to section 6.  There, it says
+that if application of a uniqueness constraint fails during
+normalization, then normalization fails (which implies invalidity.)  
+
+Added "If this failure occurs during normalization prior to
+validation, then I is invalid, as explained in section 6."
+
    > 
    > 
    > 49)
@@ -816,6 +887,9 @@
    > uniquely identify the corresponding statements a PROV instance" 
    > 
    > 
+
+Revised to make this hopefully clearer.
+
    > 
    > 
    > 50)
@@ -828,6 +902,12 @@
    > suggest to rename uniqueness constraints to identity constraints.
    > 
    > 
+
+I'd rather not make this change, as these are essentially key
+constraints / functional dependenct constraints, that enforce
+"uniqueness" on information pertaining to each identifier.  This is
+editorial so we can rename it later.
+
    > 
    > 
    > 51)
@@ -838,6 +918,9 @@
    > IF wasEndedBy(id1;a,_e1,_a1,_t1,_attrs1) and wasEndedBy(id2;a,_e2,_a2,_t2,_attrs2), THEN id=id'.
    > 
    > 
+
+Fixed
+
    > 
    > 52)
    > 
@@ -847,6 +930,9 @@
    > 
    > suggest to carry this convention into the rest of the subfigures.
    > 
+
[email protected]?
+
    > 
    > 
    > 53)
@@ -867,6 +953,9 @@
    > help avoid confusion and distraction while reading the figures. 
    > 
    > 
+
[email protected]?
+
    > 
    > 54)
    > 
@@ -888,6 +977,10 @@
    > Suggest to make the start and end vertical lines BLUE to match the activity.
    > 
    > 
+
[email protected]?
+
+
    > 
    > 55)
    > 
@@ -901,6 +994,9 @@
    > 	• IF used(use;a,e,_t,_attrs) and wasEndedBy(end;a,_e1,_a1,_t1,_attrs1) THEN use precedes end.
    > 
    > 
+
+Done (I changed all the 1's to 2's)
+
    > 
    > 56)
    > 
@@ -916,6 +1012,10 @@
    > can be invalidated." 
    > 
    > 
+
+
+Done
+
    > 
    > 57)
    > 
@@ -927,6 +1027,9 @@
    > "Similarly, if an entity specializes another"
    > 
    > 
+
+Done
+
    > 
    > 58)
    > 
@@ -954,6 +1057,9 @@
    > suggest the more specialized OR more general entity. 
    > 
    > 
+
+Fixed.
+
    > 
    > 59)
    > 
@@ -969,6 +1075,9 @@
    > must change to be less ambiguous, since it is currently misleading.
    > 
    > 
+
+Fixed.  
+
    > 
    > 60)
    > 
@@ -983,6 +1092,9 @@
    > a natural ordering) 
    > 
    > 
+
+I swapped 1's and 2's everywhere in the rule.
+
    > 
    > 61)
    > 
@@ -994,6 +1106,14 @@
    > attribution, or delegation, and finally the agent is invalidated." 
    > 
    > 
+
+Rewrote to: "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."
+
    > 
    > 
    > 62)
@@ -1007,11 +1127,18 @@
    > wasInvalidatedBy(inv;e,_a2,_t2,_attrs2) THEN gen precedes inv. 
    > 
    > 
+
+Swapped 1 and 2, added subscripts to gen and inv
+
    > 
    > make generation of agent _t0, generation of entity _t1 , invalidation
    > of entity _t2 and invalidation of agent _t3 
    > 
    > 
+
+Huh?  gen is not a time, it's an event.  Likewise, inv is an
+event. Please clarify.
+
    > 
    > 63)
    > 
@@ -1019,18 +1146,40 @@
    > 
    > do we know what "different relations" means?
    > 
+
+I assume you mean impossible-property-overlap...
+
+This literally just means that r and s are different strings from the
+set given.  Rephrased to "different relation names"
+
+
    > constraint 52 and 53:
    > 
    > should more be said about a_1 and b_1 being different?
    > 
    > 
    > 
+
+(regarding impossible-property-overlap and
+impossible-object-property-overlap).
+
+No, the values do not matter (they could be underscored variables.)  The point is that it is an error to use the same id for two
+different relations (unless one of then is influence, as stated in the
+remark).  In OWL terms, this amounts to saying that Usage, Generation,
+etc. are pairwise disjoint subclasses of Influence.  (thogh PROV-O
+doesn't enforce this AFAIK, nor need it).
+
+I also renamed r to p and s to r.
+
    > 
    > 64)
    > 
    > The phrase "and check no impossibility results from rules" seems odd to me. Could it be clearer?
    > 
    > 
+
+Rephrased.
+
    > 
    > 
    > 65)
@@ -1041,6 +1190,19 @@
    > 
    > Suggest to put it much sooner in the document.
    > 
+
+I assume you mean (typing)?  This constraint is introduced
+in the appropriate place for where it happens in constraint checking,
+and it relies on notation not introduced until this point.
+
+Moreover, I believe these constraints are effectively stated
+informally in PROV-DM.  I am happy to address it by putting a table or
+figure that summarizes the typing constraints early in
+PROV-CONSTRAINTS (in the non-normative section), if that helps.
+
[email protected]
+
+
    > 
    > 66)
    > 
@@ -1050,11 +1212,20 @@
    > 'agent' ∈ typeOf(ag) AND 'entity' ∈ typeOf(pl). 
    > 
    > 
+
+I suppose it should be, but since there are no specific disjointness
+constraints about plans (aside from those inherited from entity),
+it doesn't seem to matter.
+
    > 
    > Why is 'bundle' not a type in constraint 54:
    > 
    > IF mentionOf(e2,e1,b) THEN 'entity' ∈ typeOf(e2) AND 'entity' ∈ typeOf(e1) AND 'entity' ∈ typeOf(b).
    > 
+
+Same reason.
+
+
    > 
    > 
    > Why is c not a prov:Collection in constraint 54:
@@ -1064,6 +1235,12 @@
    > typeOf(c) AND 'prov:EmptyCollection' ∈ typeOf©.
    > 
    > 
+
+Same reason, I think...
+
+If this seems important, we can obviously add plan, bundle, and
+collection as base types.
+
    > 
    > 67)
    > 
@@ -1077,3 +1254,5 @@
    > 
    > Suggest to balance out this remark to indicate that an agent can be viewed as either.
 
+
+Done.
--- 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 &#8746;
+  class="name">{r(S(a<sub>0</sub>); S(a<sub>1</sub>),...S(a<sub>n</sub>),attrs1 &#8746;
   attrs2)}</span>  &#8746; <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' &isin; typeOf(e)</span> AND
 <span class="name">'activity' &isin; 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' &isin; typeOf(a)</span> AND
 <span class="name">'entity' &isin; 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' &isin; typeOf(a2)</span> AND
 <span class="name">'activity' &isin; 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' &isin; typeOf(a2)</span> AND
 <span class="name">'entity' &isin; 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' &isin; typeOf(a2)</span> AND
 <span class="name">'entity' &isin; 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' &isin; typeOf(e)</span> AND
 <span class="name">'activity' &isin; 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' &isin; typeOf(e2)</span> AND
 <span class="name">'entity' &isin; 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' &isin; typeOf(e)</span> AND
 <span class="name">'agent' &isin; 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' &isin; typeOf(a)</span> AND
 <span class="name">'agent' &isin; 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' &isin; typeOf(ag2)</span> AND
 <span class="name">'agent' &isin; 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>