constraints
authorLuc Moreau <l.moreau@ecs.soton.ac.uk>
Thu, 19 Jul 2012 09:52:44 +0100
changeset 4155 694286eddd0c
parent 4154 bc744945ce17
child 4156 97be5a50e989
constraints
model/prov-constraints.html
--- a/model/prov-constraints.html	Wed Jul 18 13:37:48 2012 -0400
+++ b/model/prov-constraints.html	Thu Jul 19 09:52:44 2012 +0100
@@ -196,22 +196,23 @@
 
 
         "PROV-DM":
-          "Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes "+
+          "Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, James Cheney, Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes "+
           "<a href=\"http://www.w3.org/TR/prov-dm/\"><cite>PROV-DM: The PROV Data Model</cite></a>. "+
           "2012, Working Draft. "+
           "URL: <a href=\"http://www.w3.org/TR/prov-dm/\">http://www.w3.org/TR/prov-dm/</a>",
 
         "PROV-N":
-          "Luc Moreau and Paolo Missier (eds.) "+
+          "Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes "+
           "<a href=\"http://www.w3.org/TR/prov-n/\"><cite>PROV-N: The Provenance Notation</cite></a>. "+
           "2011, Working Draft. "+
           "URL: <a href=\"http://www.w3.org/TR/prov-n/\">http://www.w3.org/TR/prov-n/</a>",
+
         "PROV-O":
-          "Satya Sahoo and Deborah McGuinness (eds.) Khalid Belhajjame, James Cheney, Daniel Garijo, Timothy Lebo, Stian Soiland-Reyes, and Stephan Zednik "+
+          "Timothy Lebo, Satya Sahoo and Deborah McGuinness (eds.) Khalid Belhajjame, James Cheney, David Corsar, Daniel Garijo, Stian Soiland-Reyes, and Stephan Zednik "+
           "<a href=\"http://www.w3.org/TR/prov-o/\"><cite>Provenance Formal Model</cite></a>. "+
           "2011, Working Draft. "+
           "URL: <a href=\"http://www.w3.org/TR/prov-o/\">http://www.w3.org/TR/prov-o/</a>",
-
+      
         "PROV-AQ":
           "Graham Klyne and Paul Groth (eds.) Luc Moreau, Olaf Hartig, Yogesh Simmhan, James Meyers, Timothy Lebo, Khalid Belhajjame, and Simon Miles "+
           "<a href=\"http://www.w3.org/TR/prov-aq/\"><cite>Provenance Access and Query</cite></a>. "+
@@ -320,7 +321,7 @@
 
 <section id="sotd">
 <h4>Last Call</h4>
-<p>This is the second public release of the PROV-DM document. 
+<p>This is the second public release of the PROV-CONSTRAINTS document. 
 This is a Last Call Working Draft. The design is not expected to change significantly, going forward, and now is the key time for external review.</p>
 
 <p>This specification identifies two  <a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">features at risk</a>, related to Mention  [[PROV-DM]]:
@@ -334,14 +335,14 @@
 <li> <a href="http://www.w3.org/TR/prov-dm/">PROV-DM</a>, the PROV data model for provenance;</li>
 <li> <a href="http://www.w3.org/TR/prov-constraints/">PROV-CONSTRAINTS</a>, a set of constraints applying to the PROV data model  (this document);</li>
 <li> <a href="http://www.w3.org/TR/prov-n/">PROV-N</a>, a notation for provenance aimed at human consumption;</li>
-<li> <a href="http://www.w3.org/TR/prov-o/">PROV-O</a>, the PROV ontology, an OWL-RL ontology allowing the mapping of PROV to RDF;</li>
+<li> <a href="http://www.w3.org/TR/prov-o/">PROV-O</a>, the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF;</li>
 <li> <a href="http://www.w3.org/TR/prov-aq/">PROV-AQ</a>, the mechanisms for accessing and querying provenance; </li>
 <li> <a href="http://www.w3.org/TR/prov-primer/">PROV-PRIMER</a>, a primer for the PROV data model.</li>
 </ul>
 <h4>How to read the PROV Family of Specifications</h4>
 <ul>
 <li>The primer is the entry point to PROV offering an introduction to the provenance model.</li>
-<li>The Linked Data and Semantic Web community should focus on PROV-O defining PROV classes and properties specified in an OWL-RL ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify the constraints applicable to the data model, and its interpretation. PROV-SEM provides a mathematical semantics.</li>
+<li>The 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>
@@ -388,9 +389,9 @@
 
 <h3>Purpose of this document</h3>
 
-<p> PROV-DM is a conceptual data model for provenance, which is
-realizable using different serializations such as PROV-N, PROV-O, or
-PROV-XML. A PROV <dfn>instance</dfn> is a set of PROV statements,
+<p>The PROV Data Model, PROV-DM, is a conceptual data model for provenance, which is
+realizable using different serializations such as PROV-N and PROV-O.
+A PROV <dfn>instance</dfn> is a set of PROV statements,
 possibly including <a>bundles</a>, or named sets of statements. For
 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
@@ -507,10 +508,10 @@
 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
-thing are called <em>alternate</em>, and the PROV-DM relations of
+thing are called <em>alternate</em>, and the PROV relations of
 specialization and alternate can be used to link such entities.</p>
 
-<p>Besides entities, a variety of other PROV-DM objects have
+<p>Besides entities, a variety of other PROV objects have
 attributes, including activity, generation, usage, start, end,
 communication, attribution, association, responsibility, and
 derivation. Each object has an associated duration interval (which may
@@ -591,7 +592,7 @@
 
 
 <p>Five kinds of <a title="instantaneous event">instantaneous
-events</a> are used in PROV-DM. The <strong>activity start</strong>
+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
@@ -629,9 +630,9 @@
 
 <div class="note">Table: work in progress; do after constraints are done.</div>
 
-<div id="prov-dm-constraints-fig" style="text-align: left;">
+<div id="prov-constraints-fig" style="text-align: left;">
 <table  class="thinborder" style="margin-left: auto; margin-right: auto;">
-<caption id="prov-dm-constraints">Table 5: Summary of definitions, constraints, and inferences for PROV-DM Types and Relations</caption>
+<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 style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
 
@@ -982,8 +983,28 @@
 </div>
 </div>
 
+<div class="note">Luc: The narrative is not right for both
+<a class="rule-text" href="#inference-entity-generation-invalidation"><span>TBD</span></a> and <a class="rule-text" href="#inference-activity-start-end"><span>TBD</span></a>, since "there must have existed" does not work for entities and activities that are still extant. However, from a constraint checking, it is ok, to add such invalidation/end events, with a future time.</div>
+
 <hr />
-<p id="activity-start-end-inference">
+<p id="entity-generation-invalidation-inference_text">
+From an entity, we can infer that the existence of
+generation and invalidation events.
+</p>
+<div class='inference' id='inference-entity-generation-invalidation'>
+<p>
+<span class='conditional'>IF</span> <span
+  class="name">entity(e,_attrs)</span> <span
+  class="conditional">THEN</span> there exist 
+<span class="name">_id1</span>, <span class="name">_a1</span>, <span class="name">_t1</span>, <span class="name">_attrs1</span>, 
+<span class="name">_id2</span>, <span class="name">_a2</span>, <span class="name">_t2</span>, and <span class="name">_attrs2</span> such that
+  <span
+  class="name">wasGeneratedBy(_id1;e,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(_id2;e,_a2,_t2,_attrs2)</span>.
+</div> 
+
+
+<hr />
+<p id="activity-start-end-inference_text">
 From an activity statement we can infer that there must have existed
 start and end events having times matching the start and end times of
 the activity.
@@ -1044,9 +1065,6 @@
 
 <hr>
 <p id='derivation-generation-use_text'>Derivations with explicit activity, generation, and usage admit the  following inference: </p>
-<div class="note">
-Luc: Here in first case, we really mean id2 specified (irrespective of _id1 specified), in the second case, we mean id1 specified (irrespective of _id2 specified).
-</div>
 <div class='inference' id='derivation-generation-use'>
 <p>
 <ol>
@@ -1066,15 +1084,16 @@
 <hr>
 <p id='derivation-use_text'>Derivations with an explicit activity and
 no specified generation and usage admit the  following inference: </p>
-<div class="note">
-Luc: Here we really mean, no usage, no generation specified. What notation do we use?
-</div>
 <div class='inference' id='derivation-use'>
 <p>
-<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(_id;e2,e1,a,gen,use,_attrs)</span> and <span class="name">wasGeneratedBy(gen;e2,a,_t2,_attrs2)</span> hold, <span
-class='conditional'>THEN</span> there exist <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>:
+<ul>
+<li>
+ there exist <span
   class="name">_t1</span> and <span class="name">_attrs1</span> such
-  that <span class="name">used(use;a,e1,_t1,_attrs1)</span> also holds.
+  that <span class="name">used(use;a,e1,_t1,_attrs1)</span>;
+<li> furthermore, <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>. 
@@ -1278,13 +1297,13 @@
 
 
        <div class='inference' id="alternate-transitive">
-<p>    For any entities <span class='name'>e1</span>, <span
-    class='name'>e2</span>, <span class='name'>e3</span>, <span class="conditional">IF</span> <span class='name'>alternateOf(e1,e2)</span> and
+<p><!-- For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>,  -->
+<span class="conditional">IF</span> <span class='name'>alternateOf(e1,e2)</span> and
    <span class='name'>alternateOf(e2,e3)</span> <span class="conditional">THEN</span> <span class='name'>alternateOf(e1,e3)</span>.</p>
     </div>
    <div class='inference' id="alternate-symmetric">
-<p>
-    For any entity <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span>  <span class='name'>alternateOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e2,e1)</span>.</p>
+<p><!-- For any entity <span class='name'>e1</span>, <span class='name'>e2</span>, -->
+<span class='conditional'>IF</span>  <span class='name'>alternateOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e2,e1)</span>.</p>
     </div>
 
 <p>
@@ -1325,8 +1344,8 @@
 
        <div class='inference' id="specialization-transitive">
 <p>
-    For any
-    entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, <span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span>
+<!--    For any   entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, -->
+<span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span>
     and
 	 <span class='name'>specializationOf(e2,e3)</span> <span class='conditional'>THEN</span> <span class='name'>specializationOf(e1,e3)</span>.</p>
     </div> 
@@ -1340,7 +1359,8 @@
     
        <div class='inference' id="specialization-alternate">
 <p>
-    For any entities  <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e1,e2)</span>.</p>
+<!--    For any entities  <span class='name'>e1</span>, <span class='name'>e2</span>, -->
+<span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e1,e2)</span>.</p>
     </div> 
 
 <hr />
@@ -1352,8 +1372,9 @@
 
 <div class="inference" id="specialization-attributes">
   <p>
-  For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>entity(e1, [a=x])</span> holds for some
-  attribute <span class='name'>a</span> with value <span class='name'>x </span> and <span class='name'>specializationOf(e2,e1)</span> holds <span class='conditional'>THEN </span>
+<!--  For any entities <span class='name'>e1</span>, <span class='name'>e2</span>,-->
+<span class='conditional'>IF</span> <span class='name'>entity(e1, [a=x])</span> holds for some
+  attribute <span class='name'>a</span> with value <span class='name'>x </span> and <span class='name'>specializationOf(e2,e1)</span> holds, <span class='conditional'>THEN </span>
   <span class='name'>entity(e2, [a=x])</span> also holds.</p>
   </div>
 
@@ -1539,7 +1560,7 @@
 <p>
 <hr>
 
-  <p id='key_text'> We assume that the various identified objects of PROV-DM have
+  <p id='key_text'> We assume that the various identified objects of PROV have
   unique statements describing them within a PROV instance, through
   the following key constraints:
   </p>
@@ -1560,7 +1581,7 @@
 
    <hr />
    <p id='key_relation_text'> Likewise, we assume that the identifiers
-   of relationships in PROV-DM uniquely identify the corresponding statements a PROV instance, through
+   of relationships in PROV uniquely identify the corresponding statements a PROV instance, through
   the following key constraints:
   </p>
   <div class='constraint' id='key-relation'>
@@ -1744,7 +1765,7 @@
 
 
 <p>To allow for minimalistic clock assumptions, like Lamport
-[[CLOCK]], PROV-DM relies on a notion of relative ordering of <a title="instantaneous event">instantaneous events</a>,
+[[CLOCK]], PROV relies on a notion of relative ordering of <a title="instantaneous event">instantaneous events</a>,
 without using physical clocks. This specification assumes that a preorder exists between <a title="instantaneous event">instantaneous events</a>.
 </p>
 
@@ -1767,7 +1788,7 @@
 <a>transitive</a> relation. </p>
 
 
-<p>PROV-DM also allows for time observations to be inserted in
+<p>PROV also allows for time observations to be inserted in
 specific provenance statements, for each of the five kinds of <a
  title="instantaneous event">instantaneous events</a> introduced in
 this specification.  Times in provenance records arising from
@@ -2441,7 +2462,7 @@
 
   <p>Two PROV instances are <dfn>equivalent</dfn> if they have the
 same normal form (that is, after applying all possible inference
-rules, the two instances produce the same set of PROV-DM statements,
+rules, the two instances produce the same set of PROV statements,
 up to reordering of statements and attributes within attribute lists).
 Equivalence has the following characteristics: </p>
 
@@ -2466,7 +2487,7 @@
   <li>Equivalence is <a>reflexive</a>, <a>symmetric</a>, and <a>transitive</a>.</li>
 </ul>
 
-<p> An application that processes PROV-DM data SHOULD handle
+<p> An application that processes PROV data SHOULD handle
 equivalent instances in the same way. (Common exceptions to this rule
 include, for example, pretty printers that seek to preserve the
 original order of statements in a file and avoid expanding