* Fixed up to Tim's comment 27
authorJames Cheney <jcheney@inf.ed.ac.uk>
Mon, 06 Aug 2012 18:35:01 +0100
changeset 4279 24b3fc3f7907
parent 4278 26dc6f790bc1
child 4280 b6c650475879
* Fixed up to Tim's comment 27
model/comments/issue-459-tim.txt
model/prov-constraints.html
--- a/model/comments/issue-459-tim.txt	Mon Aug 06 17:24:44 2012 +0100
+++ b/model/comments/issue-459-tim.txt	Mon Aug 06 18:35:01 2012 +0100
@@ -148,6 +148,9 @@
    > 
    > I'd suggest removing these part, so we can get to "This document introduces" more quickly.
    > 
+
+Done.
+
    > 
    > 2)
    > My previous confusion among inference/definition/constraint is budding:
@@ -156,13 +159,25 @@
    > 
    > "These inferences and constraints" (where did definitions go?)
    > 
+
+Added missing "definitions"
+
    > The second paragraph of 1.2 disambiguates the notions, but the wording
    > in the abstract might be revisited for clarity. 
    > 
+
+Hopefully adopting consistent "definitions, inferences, and constraints"
+
    > 3)
    > 
    > "PROV-SEM provides a mathematical semantics." is this still part of the family? It's not listed above.
    > 
+
+I think we still plan to do it (time permitting).  It's in the same
+ballpark as PROV-XML and company.  If it slips, we can presumably
+remove the reference.  For the moment, I've commented the sentence
+out, although we mention PROV-SEM later.
+
    > 
    > 
    > Introduction
@@ -178,12 +193,18 @@
    > 
    > Suggest that we converge on the definition and use it throughout.
    > 
+
+I copied the definition from the LC of PROV-DM.
+
    > 
    > 5)
    > 
    > typo: "Some of these ariables"
    > 
    > 
+
+Fixed.
+
    > 
    > 6)
    > 
@@ -191,6 +212,9 @@
    > http://dvcs.w3.org/hg/prov/raw-file/default/model/releases/ED-prov-constraints-20120723/prov-constraints.html#dfn-valid  
    > 
    > 
+
+Done
+
    > 
    > 
    > 7)
@@ -203,6 +227,10 @@
    > It seems that there are two types of constraints (uniqueness and
    > ordering). Suggest to introduce this distinction before using it. 
    > 
+
+Introduced the three types of constraints earlier, so that we can
+explain how they are used in this summary.
+
    > 
    > 8)
    > 
@@ -217,11 +245,17 @@
    > "definitions, inferences and constraints."
    > "presents inferences and definitions"
    > 
+
+Done (definitions, inferences and constraints throughout)
+
    > 
    > 9)
    > 
    > typo "certain statments"
    > 
+
+Fixed
+
    > 
    > 
    > 10)
@@ -232,17 +266,39 @@
    > kind of constraint. Although this might be "easing into" the details,
    > I find it a bit unsettling to find these additions. 
    > 
+
+Hopefully, introducing the three kinds of constraints in the
+introduction signposts this better now.
+
    > "also defines a class of valid PROV instances by specifying
    > constraints that valid PROV instances must satisfy." is only partly
    > true and thus misleading, since only ordering and impossibility
    > constraints are used to determine validity. 
    > 
+
+Not true: the uniqueness constraints are implicitly checked while they
+are being applied.  This checking can fail, if a uniqueness
+constraint forces us to merge two things that are incompatible:
+
+activity(a,0,1)
+activity(a,3,4) 
+
+
+However, the uniqueness constraints behave more like inferences, and
+need to be applied during normalization (because they can trigger
+further inferences, which can trigger further uniqueness constraints,
+etc.).  So this is somewhat intricate to explain, but what is written
+is technically true: valid PROV instances must satisfy the uniqueness constraints.
+
    > 
    > 11)
    > 
    > Why are "impossibility constraints" not mentioned in the "to summarize" in 1.2?
    > 
    > 
+
+They are now.
+
    > 
    > 2. Rationale
    > 
@@ -257,6 +313,11 @@
    > in different ways, with different descriptions of their partial
    > state." 
    > 
+
+Simplified to "PROV allows for things to be described
+in different ways, with different descriptions of their 
+state.  "
+
    > 
    > 13)
    > 
@@ -266,6 +327,9 @@
    > 
    > "state during the entity's lifetime"
    > 
+
+Done
+
    > 
    > 14)
    > 
@@ -276,6 +340,9 @@
    > "Different entities that fix aspects of the same thing"
    > 
    > 
+
+Done
+
    > 
    > 15)
    > 
@@ -286,6 +353,9 @@
    > 
    > sugest to replace with "and preserves the characteristics provided"
    > 
+
+Stale text; done.
+
    > 
    > 
    > 2.2 Events
@@ -298,6 +368,9 @@
    > great discussion on global clocks!
    > 
    > 
+
+Thanks
+
    > 
    > 
    > 17)
@@ -319,24 +392,38 @@
    > 
    > suggest to reorder for clarity.
    > 
-   > 
+
+It's been this way for a long time; your suggestion is adopted.
+
+  > 
    > 
    > 
    > 18)
    > 
    > great definitions on events.
    > 
+
+Thanks
    > 
    > 19)
    > 
    > 
    > Table 5's column says "Definitions, Constraints, Inferences" but I see no "Defintion X" in that column.
    > 
+
+Removed "Definition".  
+
    > 
    > 20)
    > 
    > Suggest to move Table 5's column 3 to column 1
    > 
+
+The format of the table is the same as that in PROV-DM table 5.  So I
+would prefer to leave it as is.  (Also, as it is the most important
+information is to the left-hand side of the page, which I think makes
+it easier to read if you print it out...)
+
    > 
    > 
    > Section 4
@@ -347,6 +434,17 @@
    > 
    > Should "A definition is a rule that" be "A definition is an inference"?
    > 
+
+No, because both definitions and inferences are rules (formulas).  We
+are using "inference" in a somewhat different technical sense later
+(as an implication rather than an if and only if).
+
+Added clarifying text "a definition is a rule that can be applied to
+  PROV instances to replace defined expressions with definitions.  A definition states that a
+  provenance statement is equivalent to some other statements, whereas
+  an inference only states one direction of an implication; thus,
+  defined provenance statements can be replaced by their definitions."
+
    > 
    > 
    > 22)
@@ -361,6 +459,9 @@
    > 
    > suggest to drop parens and to restructure sentence.
    > 
+
+Done
+
    > 
    > 23)
    > 
@@ -374,6 +475,16 @@
    > "In contrast, distinct URIs or literal values in PROV are assumed to
    > be distinct for the purpose of checking validity or inferences." 
    > 
+
+Implementations should decide up front what equational reasoning from
+sameAs assertions should be applied, and rewrite the instance (by
+substituting identifiers) to make this explicit, before doing
+validation.  I don't think we want to explicitly deal with sameAs in
+the constraints, since this is a OWL/RDF specific phenomenon.
+
+A remark to this effect has been added to the beginning of section 6.
+--jrc
+
    > 
    > 24)
    > 
@@ -384,11 +495,19 @@
    > 
    > "Identifiers can sometimes be omitted in [PROV-N] notation."
    > 
+
+In PROV-O, you can't write "-" and have it be treated as a blank
+node/existential varaible, though there are other ways of
+accomplishing this.  
+
    > 
    > 25)
    > 
    > Is "desugar" a technical term that should stay in a Recommendation?
    > 
+
+No; revised to "Definitions 1, 2, and 3 explain how to expand the compact forms of PROV-N notation into a normal form."
+
    > 
    > 26)
    > 
@@ -398,6 +517,12 @@
    > , to help make the distinction between an object and an influence
    > 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.
+
    > 
    > 
    > 27)
@@ -415,6 +540,9 @@
    > which are expanded by the rules in Definition 2." 
    > 
    > 
+
+Done.
+
    > 
    > 
    > 28)
@@ -637,6 +765,9 @@
    > wasAssociatedWith(_id2;a, ag2, -, [])."  
    > 
    > 
+
+This is ISSUE-452.
+
    > 
    > 46)
    > 
@@ -647,6 +778,14 @@
    > Why is this stated, and what are its consequences? Narrative is needed.
    > 
    > 
+
+This is because of ISSUE-29.  That is, after a long discussion we
+decided that alternateOf is reflexive, symmetric, and transitive, that
+is, an equivalence relation.  Is your concern that it wasn't clear how
+the concept of "equivalence relation" and "reflexive, symmetric,
+transitive" are related?  If so I have added (minimal) additional text
+to explain this, and made "equivalence relation" a definition in the glossary.
+
    > 
    > 
    > 47)
--- a/model/prov-constraints.html	Mon Aug 06 17:24:44 2012 +0100
+++ b/model/prov-constraints.html	Mon Aug 06 18:35:01 2012 +0100
@@ -399,14 +399,31 @@
 
     <section id="abstract">
 <p>
-Provenance is information about entities, activities, and people involved in producing a piece of data or thing, which can be used to form assessments about its quality, reliability or trustworthiness. PROV-DM is the conceptual data model that forms a basis for the W3C provenance (PROV) family of specifications. PROV-DM distinguishes core structures, forming the essence of provenance information, from extended structures catering for more specific uses of provenance. PROV-DM is organized in six components, respectively dealing with: (1) entities and activities, and the time at which they were created, used, or ended; (2) derivations of entities from entities; (3) agents bearing responsibility for entities that were generated and activities that happened; (4) a notion of bundle, a mechanism to support provenance of provenance; (5) properties to link entities that refer to the same thing; and, (6) collections forming a logical structure for its members.
+Provenance is information about entities, activities, and people
+involved in producing a piece of data or thing, which can be used to
+form assessments about its quality, reliability or
+trustworthiness. PROV-DM is the conceptual data model that forms a
+basis for the W3C provenance (PROV) family of specifications.
+<!--
+PROV-DM
+distinguishes core structures, forming the essence of provenance
+information, from extended structures catering for more specific uses
+of provenance. PROV-DM is organized in six components, respectively
+dealing with: (1) entities and activities, and the time at which they
+were created, used, or ended; (2) derivations of entities from
+entities; (3) agents bearing responsibility for entities that were
+generated and activities that happened; (4) a notion of bundle, a
+mechanism to support provenance of provenance; (5) properties to link
+entities that refer to the same thing; and, (6) collections forming a
+logical structure for its members.
+-->
 </p>
 
 
-<p> This document introduces <a>inferences</a> and <a>definitions</a>
+<p> This document introduces <a>definitions</a> and <a>inferences</a>
   that are allowed on provenance statements and <a>constraints</a>
   that PROV instances MUST satisfy in order to be considered
-  <a>valid</a>. These inferences and constraints are useful for
+  <a>valid</a>. These definitions, inferences, and constraints are useful for
   readers who develop applications that generate provenance or reason
   over provenance.  They can also be used to <a title="normal form">normalize</a> PROV
   instances to forms that can easily be compared in order to determine
@@ -440,7 +457,13 @@
 <h4>How to read the PROV Family of Specifications</h4>
 <ul>
 <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 OWL2 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 Linked Data and Semantic Web community should focus on PROV-O
+defining PROV classes and properties specified in an OWL2
+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>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-CONSTRAINTS.  PROV-O and PROV-N offer examples of mapping to RDF and text, respectively.</li>
@@ -455,9 +478,9 @@
       <h2>Introduction<br>
 </h2> 
 
-<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 complements
+<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 complements
   the PROV-DM specification [[PROV-DM]] that defines a data model for
   provenance on the Web.  </p>
 
@@ -474,7 +497,7 @@
       [[!RFC2119]].</p>
 
 <p>In this document, logical formulas contain variables written as
-    lower-case identifiers.  Some of these ariables are written
+    lower-case identifiers.  Some of these variables are written
     beginning with the underscore character <span
     class="name">_</span>, by convention, to indicate that they
     (intentionally) appear only once in the formula; thus, the textual
@@ -494,17 +517,20 @@
 example, such a PROV instance could be a .provn document, the result
 of a query, a triple store containing PROV statements in RDF, etc. The
 PROV-DM specification [[PROV-DM]] imposes minimal requirements upon
-PROV instances. A <em>valid</em> PROV instance corresponds to a
+PROV instances. A <a>valid</a> PROV instance corresponds to a
 consistent history of objects and interactions to which logical
 reasoning can be safely applied. By default, PROV instances need not
-be valid.  </p>
+be <a>valid</a>.  </p>
 
 <p> This document specifies <em>inferences</em> over PROV instances
 that applications MAY employ, including <em>definitions</em> of some
 provenance statements in terms of others, and also defines a class of
-<em>valid</em> PROV instances by specifying <em>constraints</em> that
-valid PROV instances must satisfy. Applications SHOULD produce valid
-provenance and MAY reject provenance that is not valid.  Applications
+<a>valid</a> PROV instances by specifying <em>constraints</em> that
+<a>valid</a> PROV instances must satisfy. There are three kinds of
+constraints: <em>uniqueness constraints</em>, <em>event ordering
+constraints</em>, and <em>impossibility 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
 PROV instances in order to determine whether two such instances convey
 the same information.
@@ -512,8 +538,8 @@
 
 <p>To summarize: compliant applications use definitions,
 inferences, and uniqueness constraints to normalize PROV instances,
-and then apply event ordering constraints to determine whether the
-instance has a consistent event ordering.  If so, the instance is
+and then check event ordering and impossibility 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
 same normal form are considered <a>equivalent</a>.  Further discussion
@@ -533,14 +559,13 @@
 requirements for compliance with this document, which are specified in
 detail in the rest of the document.  </p>
 
-<p> <a href="#inferences">Section 4</a> presents inferences and
-definitions.  Definitions allow replacing shorthand notation in [[!PROV-N]]
+<p> <a href="#inferences">Section 4</a> presents definitions and inferences.  Definitions allow replacing shorthand notation in [[!PROV-N]]
 with more explicit and complete statements; inferences allow adding
 new facts representing implicit knowledge about the structure of
 provenance.  </p>
 
 <p><a href="#constraints">Section 5</a> presents three kinds of constraints,
-<em>uniqueness</em> constraints that prescribe that certain statments
+<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
@@ -587,9 +612,8 @@
 is how to deal with change.  Real-world objects, information objects
 and Web resources change over time, and the characteristics that make
 them identifiable in a given situation are sometimes subject to change
-as well.  To avoid over-reliance on assumptions that identifying
-characteristics do not change, PROV allows for things to be described
-in different ways, with different descriptions of their partial
+as well.  PROV allows for things to be described
+in different ways, with different descriptions of their 
 state.  
 </p>
 
@@ -602,12 +626,12 @@
 and its <a title="entity invalidation event">invalidation event</a>.
 An entity's attributes are established when the entity is
 created and describe the entity's situation and (partial) state
-during an entity's lifetime.</p>
+during the entity's lifetime.</p>
 
 <p>
 A different entity (perhaps representing a different user or
 system perspective) may fix other aspects of the same thing, and its provenance
-may be different.  Different entities that are aspects of the same
+may be different.  Different entities that fix aspects of the same
 thing are called <em>alternate</em>, and the PROV relations of
 specialization and alternate can be used to link such entities.</p>
 
@@ -657,7 +681,7 @@
 
 <p>An activity is not an entity.  Indeed, an entity exists in full at
 any point in its lifetime, persists during this interval, and
-preserves the characteristics that make it identifiable.  In
+preserves the characteristics provided.  In
 contrast, an activity is something that occurs, happens, unfolds, or
 develops through time, but is typically not identifiable by the
 characteristics it exhibits at any point during its duration.  This
@@ -694,8 +718,8 @@
 <p>Five kinds of <a title="instantaneous event">instantaneous
 events</a> are used in PROV. The <strong>activity start</strong>
 and <strong>activity end</strong> events delimit the beginning and the
-end of activities, respectively. The <strong>entity usage</strong>,
-<strong>entity generation</strong>, and <strong>entity
+end of activities, respectively. The 
+<strong>entity generation</strong>, <strong>entity usage</strong>, and <strong>entity
 invalidation</strong> events apply to entities, and the generation and
 invalidation events delimit the <a>lifetime</a> of an entity. More
 precisely:
@@ -705,13 +729,15 @@
 
 <p>An <dfn id="dfn-end-event">activity end event</dfn> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity ends.</p>
 
+<p>An <dfn id="dfn-generation-event">entity generation event</dfn> is the <a title="instantaneous event">instantaneous event</a> that marks the  final instant of an entity's creation timespan, after which
+it is available for use.  The entity did not exist before this event.</p>
+
+
 <p>An <dfn id="dfn-usage-event">entity usage event</dfn> is the <a
 title="instantaneous event">instantaneous event</a> that marks the first instant of
 an entity's consumption timespan by an activity.  Before this instant
 the entity had not begun to be used by the activity.</p>
 
-<p>An <dfn id="dfn-generation-event">entity generation event</dfn> is the <a title="instantaneous event">instantaneous event</a> that marks the  final instant of an entity's creation timespan, after which
-it is available for use.  The entity did not exist before this event.</p>
 
 <p>An <dfn id="dfn-invalidation-event">entity invalidation event</dfn>
 is the <a title="instantaneous event">instantaneous event</a> that
@@ -733,7 +759,8 @@
 <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>
-<tr><td><a><b>Type or Relation Name</b></a></td><td><b>Definitions, Constraints, Inferences</b></td><td><b>Component</b></td></tr>
+<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>
 
 <tr class="component1-color">
@@ -1039,10 +1066,11 @@
 PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef"></a>).
 An  <dfn id="inference">inference</dfn> is a rule that can be applied
   to PROV instances to add new PROV statements.  A <dfn
-  id="definition">definition</dfn> is a rule that states that a
-  provenance statement is equivalent to some other statements; thus,
-  defined provenance statements can be replaced by their definitions,
-and vice versa.
+  id="definition">definition</dfn> is a rule that can be applied to
+  PROV instances to replace defined expressions with definitions.  A definition states that a
+  provenance statement is equivalent to some other statements, whereas
+  an inference only states one direction of an implication; thus,
+  defined provenance statements can be replaced by their definitions.
 </p>
 
 <p> Inferences have the following general form:</p>
@@ -1064,11 +1092,12 @@
   class="name">a<sub>m</sub></span> for unknown objects.  These fresh
   identifiers might later be found to be equal to known identifiers;
   they play a similar role in PROV constraints to existential
-  variables in logic, "labeled nulls" in database theory [[DBCONSTRAINTS]],  or to blank nodes in [[RDF]].  With a few
-  exceptions (discussed below), omitted optional parameters to
+  variables in logic, "labeled nulls" in database theory
+  [[DBCONSTRAINTS]],  or to blank nodes in [[RDF]].  In general, omitted optional parameters to
   [[PROV-N]] statements, or explicit <span class="name">-</span>
   markers, are placeholders for existentially quantified variables;
-  that is, they denote unknown values.  </p>
+  that is, they denote unknown values.  There are a few exceptions to
+  this general rule, which are explained below.</p>
 
 <p> Definitions have the following general form:</p>
 
@@ -1112,13 +1141,21 @@
 
   <p>Many PROV relation statements have an identifier, identifying a
   link between two or more related objects.  Identifiers can sometimes
-  be omitted in [[PROV-N]] notation.  For the purpose of inference and
+  be omitted in [[PROV-O]] notation.  For the purpose of inference and
   validity checking, we generate special identifiers called
   <dfn>existential variables</dfn> denoting the unknown values.
   Existential variables can be <em>substituted</em> with constant
   identifiers, literals, the placeholder <span class="name">-</span>,
   or other <a>existential variables</a>.  
-We note that  Definitions 1, 2, and 3 desugar compact PROV-N notation into a normal form.
+<a class="rule-ref" href="#optional-identifiers"><span>TBD</span></a>,
+<a class="rule-ref" href="#optional-attributes"><span>TBD</span></a>,
+, and
+<a class="rule-ref" href="#definition-short-forms"><span>TBD</span></a>,
+ explain how to expand the compact forms of PROV-N notation into a
+  normal form.  <a class="rule-ref"
+  href="#optional-placeholders"><span>TBD</span></a> indicates when
+  other optional parameters can be replaced by <a>existential
+  variables</a>.  
 </p>
 
   <div class="definition" id="optional-identifiers">
@@ -1151,14 +1188,15 @@
    <div class="definition" id="optional-attributes">
 <ol>
   <li>
-For each  <span class="name">r</span> in {<span
+  For each  <span class="name">r</span> in {<span
    class="name">entity</span>, <span class="name">activity</span>,
-   <span class="name">agent</span>}, if <span class="name">a_n</span> is not an attribute
+   <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> 
    holds <span  class="conditional">IF AND ONLY IF</span>   <span
-   class="name">r(a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li>
-     <li>
+   class="name">r(a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.
+  </li>
+  <li>
      For each <span class="name">r</span> in { 
 <span class="name">used</span>,
 <span class="name">wasGeneratedBy</span>,
@@ -1170,7 +1208,7 @@
 <span class="name">wasDerivedFrom</span>,
 <span class="name">wasAttributedTo</span>,
 <span class="name">wasAssociatedWith</span>,
-<span class="name">actedOnBehalfOf</span>}, if <span class="name">a_n</span> is not an
+<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
@@ -1221,11 +1259,10 @@
    form is not defined in terms of the long form in this case.</p>-->
 
   <p>
-  There
-   are also no expansion rules for entity, agent, communiction,
-   attribution, influence, alternate, or specialization, because these have no optional parameters aside
-   from the identifier and attribute, which are expanded by other
-   rules above.</p>
+There are no expansion rules for entity, agent, communiction,
+ attribution, influence, alternate, or specialization, because these
+ have no optional parameters aside from the identifier and attributes,
+ which are expanded by the rules in <a class="rule-ref" href="#optional-attributes"><span>TBD</span></a>.  </p>
    </div>
 
 <!--<div id="optional-attributes1"> -->
@@ -1317,7 +1354,14 @@
     
   <div class="definition" id="optional-placeholders">
     <ol><li>
-For each <span class="name">r</span> in {<span
+      <span class="name">activity(id,-,t2,attrs)</span> <span  class="conditional">IF AND ONLY
+   IF</span> there exists <span class="name">t1</span> such that <span class="name">activity(id,t1,t2,attrs)</span>.
+  </li>
+<li>  <span class="name">activity(id,t1,-,attrs)</span> <span  class="conditional">IF AND ONLY
+   IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>.
+</li>
+<!--
+<li>For each <span class="name">r</span> in {<span
     class="name">entity</span>, <span class="name">activity</span>,
     <span class="name">agent</span>}, the following definition
     holds:
@@ -1325,6 +1369,7 @@
       <span class="name">r(a<sub>0</sub>,...,a<sub>i-1</sub>, -, a<sub>i+1</sub>, ...,a<sub>n</sub>) </span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">a'</span>
     such that <span class="name">r(a<sub>0</sub>,...,a<sub>i-1</sub>,a',a<sub>i+1</sub>,...,a<sub>n</sub>)</span>.
     </li>
+    -->
     <li>For each  <span class="name">r</span> in { 
 <span class="name">used</span>,
 <span class="name">wasGeneratedBy</span>,
@@ -1346,7 +1391,7 @@
 
   <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
@@ -1492,7 +1537,7 @@
     </div>-->
 
 <p id="activity-start-end-inference_text">
-From an activity statemen,t we can infer that 
+From an activity statement, we can infer that 
 start and end events having times matching the start and end times of
 the activity.
 </p>
@@ -1813,9 +1858,13 @@
 
   
 <hr>
-  <p id="alternate-reflexive_text">The relation <span class='name'>alternateOf</span> is an equivalence relation: <a>reflexive</a>,
-  <a>transitive</a> and <a>symmetric</a>.</p>
-  
+  <p id="alternate-reflexive_text">The relation <span
+  class='name'>alternateOf</span> is an <a>equivalence relation</a>: that is,
+  it is <a>reflexive</a>,
+  <a>transitive</a> and <a>symmetric</a>.  As a consequence, the
+  following inferences can be applied:</p>
+
+ 
 <div class='inference' id="alternate-reflexive">
 <p>
     For any entity <span class='name'>e</span>, we have <span class='name'>alternateOf(e,e)</span>.
@@ -3263,7 +3312,18 @@
 for PROV instances that consist of a single, unnamed <a>bundle</a> of
 statements, called the <dfn>toplevel bundle</dfn>.</p>
 
-
+<div class="remark">
+
+  Implementations should decide up front what reasoning about
+  coreference should be applied, and rewrite the instance (by
+  replacing coreferent identifiers with a single common identifier) to
+  make this explicit, before doing validation, equivalence checking,
+  or normalization.
+  All of the following definitions assume that the application has
+  already determined which URIs in the PROV instance are co-referent
+  (e.g. <span class="name">owl:sameAs</span> as a result of OWL
+  reasoning).
+  </div>
 
 <p> We define the <dfn>normal form</dfn> of a PROV instance as the set
 of provenance statements resulting from merging to resolve all
@@ -3296,7 +3356,7 @@
     of <span class="math">I<sub>3</sub></span> (that is, proceed by recursively normalizing <span class="math">I<sub>3</sub></span>).
  </ol>
  
-<p>Because of the potential interaction among inferences, definitions and
+<p>Because of the potential interaction among definitions, inferences, and
   constraints, the above algorithm is recursive.  Nevertheless,
   all of our constraints fall into a class of <a>tuple-generating
   dependencies</a> and <a>equality-generating dependencies</a> that
@@ -3312,7 +3372,7 @@
  A PROV instance is <dfn id="dfn-valid">valid</dfn>
 if its normal form exists and satisfies all of
   the validity constraints; this implies that the instance satisfies
-  all of the inferences, definitions and constraints.  
+  all of the definitions, inferences, and constraints.  
   The following algorithm can be used to test
   validity:</p>
 
@@ -3453,7 +3513,10 @@
       for any elements <span class="math">x</span>, <span class="math">y</span> of <span class="math">X</span>, if <span class="math">x R y</span> and <span class="math">y R x</span> then <span class="math">x = y</span>.</li>
        <li> <dfn>asymmetric</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>asymmetric</a> if
       <span class="math">x R y</span> and <span class="math">y R x</span> do not hold for any elements <span class="math">x</span>, <span class="math">y</span> of <span class="math">X</span>.</li>
-        <li> <dfn>irreflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>irreflexive</a> if
+        <li><dfn>equivalence relation</dfn>: An equivalence relation is a relation
+      that is <a>reflexive</a>, <a>symmetric</a>, and
+       <a>transitive</a>.</li>
+       <li> <dfn>irreflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>irreflexive</a> if
       for <span class="math">x R x</span> does not hold for any element <span class="math">x</span> of <span class="math">X</span>.</li>
         <li> <dfn>reflexive</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a>reflexive</a> if
       for any element <span class="math">x</span> of <span class="math">X</span>, we have <span class="math">x R x</span>.</li>