--- a/model/diff-c.html Wed Aug 08 13:58:16 2012 +0200
+++ b/model/diff-c.html Wed Aug 08 13:07:28 2012 +0100
@@ -490,7 +490,7 @@
pre.sh_sourceCode .sh_attribute { color: #006400; }
</style><link href="./extra.css" rel="stylesheet" type="text/css" charset="utf-8"><link href="http://www.w3.org/StyleSheets/TR/W3C-ED" rel="stylesheet" type="text/css" charset="utf-8"></head>
- <body style="display: inherit; "><div class="head"><p><a href="http://www.w3.org/"><img width="72" height="48" src="http://www.w3.org/Icons/w3c_home" alt="W3C"></a></p><h1 class="title" id="title">Constraints of the Provenance Data Model</h1><h2 id="subtitle"><span class="delete">Version for</span><a href="diff-c.html"><span class="insert">Changes</span></a><span class="insert"> since</span> internal <span class="delete">review</span><span class="insert">release (pre-LC)</span></h2><h2 id="w3c-editor-s-draft-07-august-2012"><acronym title="World Wide Web Consortium">W3C</acronym> Editor's Draft <span class="delete">23 July</span><span class="insert">07 August</span> 2012</h2><dl><dt>This version:</dt><dd><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</a></dd><dt>Latest published version:</dt><dd><a href="http://www.w3.org/TR/prov-constraints/">http://www.w3.org/TR/prov-constraints/</a></dd><dt>Latest editor's draft:</dt><dd><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</a></dd><dt>Previous version:</dt><dd><a href="http://www.w3.org/TR/2012/WD-prov-constraints-20120503/">http://www.w3.org/TR/2012/WD-prov-constraints-20120503/</a></dd><dt>Editors:</dt><dd><a href="http://homepages.inf.ed.ac.uk/jcheney">James Cheney</a>, University of Edinburgh</dd>
+ <body style="display: inherit; "><div class="head"><p><a href="http://www.w3.org/"><img width="72" height="48" src="http://www.w3.org/Icons/w3c_home" alt="W3C"></a></p><h1 class="title" id="title">Constraints of the Provenance Data Model</h1><h2 id="subtitle"><span class="delete">Version for</span><a href="diff-c.html"><span class="insert">Changes</span></a><span class="insert"> since</span> internal <span class="delete">review</span><span class="insert">release (pre-LC)</span></h2><h2 id="w3c-editor-s-draft-08-august-2012"><acronym title="World Wide Web Consortium">W3C</acronym> Editor's Draft <span class="delete">23 July</span><span class="insert">08 August</span> 2012</h2><dl><dt>This version:</dt><dd><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</a></dd><dt>Latest published version:</dt><dd><a href="http://www.w3.org/TR/prov-constraints/">http://www.w3.org/TR/prov-constraints/</a></dd><dt>Latest editor's draft:</dt><dd><a href="http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html">http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html</a></dd><dt>Previous version:</dt><dd><a href="http://www.w3.org/TR/2012/WD-prov-constraints-20120503/">http://www.w3.org/TR/2012/WD-prov-constraints-20120503/</a></dd><dt>Editors:</dt><dd><a href="http://homepages.inf.ed.ac.uk/jcheney">James Cheney</a>, University of Edinburgh</dd>
<dd><a href="http://www.cs.ncl.ac.uk/people/Paolo.Missier">Paolo Missier</a>, Newcastle University</dd>
<dd><a href="http://www.ecs.soton.ac.uk/~lavm/">Luc Moreau</a>, University of Southampton</dd>
<dt>Author:</dt><dd><a href="http://users.ugent.be/~tdenies/">Tom De Nies</a>, IBBT - Ghent University</dd>
@@ -508,14 +508,25 @@
</p>
-<p> This document introduces <a><span class="insert">definitions</span></a><span class="insert"> and </span><a>inferences<span class="delete"> and </span><span class="delete">definitions</span></a>
- that are allowed on provenance statements and <a>constraints</a>
- that PROV instances <em class="rfc2119" title="must">must</em> satisfy in order to be considered
- <a href="#dfn-valid" class="internalDFN">valid</a>. These <span class="delete">inferences</span><span class="insert">definitions, inferences,</span> 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" href="#dfn-normal-form" class="internalDFN">normalize</a> PROV
- instances to forms that can easily be compared in order to determine
- whether two PROV instances are <a href="#dfn-equivalent" class="internalDFN">equivalent</a>.</p>
+<p> This document <span class="delete">introduces</span><span class="insert">defines a subset of PROV instances called
+</span><i><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a></i><span class="insert"> PROV instances. A </span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert"> PROV instance corresponds to a
+consistent history of objects and interactions to which logical
+reasoning can be safely applied.
+Valid PROV instances satisfy
+certain </span><a><span class="insert">definitions</span></a><span class="insert">,</span> <a>inferences</a><span class="delete"> and </span><span class="delete">definitions</span><span class="delete">
+ that are allowed on provenance statements and </span><span class="insert">, and
+</span><a>constraints</a><span class="delete">
+ that PROV instances </span><span class="delete">must</span><span class="delete"> satisfy in order to be considered
+ </span><span class="delete">valid</span>. These <span class="delete">inferences</span><span class="insert">definitions, inferences,</span> and constraints<span class="delete"> are useful</span><span class="insert">
+provide a measure of consistency checking</span> for<span class="delete">
+ readers who develop applications that generate</span> provenance <span class="delete">or reason
+ </span><span class="insert">and reasoning
+</span>over provenance. They can also be used to <a title="normal
+form" href="#dfn-normal-form" class="internalDFN">normalize</a> PROV
+ instances to forms that can easily be
+compared in order to determine
+ whether two PROV instances are
+<a href="#dfn-equivalent" class="internalDFN">equivalent</a>.</p>
</div><div id="sotd" class="introductory section"><h2>Status of This Document</h2><p><em>This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current <acronym title="World Wide Web Consortium">W3C</acronym> publications and the latest revision of this technical report can be found in the <a href="http://www.w3.org/TR/"><acronym title="World Wide Web Consortium">W3C</acronym> technical reports index</a> at http://www.w3.org/TR/.</em></p>
<h4 id="last-call">Last Call</h4>
@@ -555,7 +566,7 @@
</ul>
<p>This document was published by the <a href="http://www.w3.org/2011/prov/">Provenance Working Group</a> as an Editor's Draft. If you wish to make comments regarding this document, please send them to <a href="mailto:public-prov-comments@w3.org">public-prov-comments@w3.org</a> (<a href="mailto:public-prov-comments-request@w3.org?subject=subscribe">subscribe</a>, <a href="http://lists.w3.org/Archives/Public/public-prov-comments/">archives</a>). All feedback is welcome.</p><p>Publication as an Editor's Draft does not imply endorsement by the <acronym title="World Wide Web Consortium">W3C</acronym> Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.</p><p>This document was produced by a group operating under the <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/">5 February 2004 <acronym title="World Wide Web Consortium">W3C</acronym> Patent Policy</a>. <acronym title="World Wide Web Consortium">W3C</acronym> maintains a <a href="http://www.w3.org/2004/01/pp-impl/46974/status" rel="disclosure">public list of any patent disclosures</a> made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/#def-essential">Essential Claim(s)</a> must disclose the information in accordance with <a href="http://www.w3.org/Consortium/Patent-Policy-20040205/#sec-Disclosure">section 6 of the <acronym title="World Wide Web Consortium">W3C</acronym> Patent Policy</a>.</p></div><div id="toc" class="section"><h2 class="introductory">Table of Contents</h2><ul class="toc"><li class="tocline"><a href="#introduction" class="tocxref"><span class="secno">1. </span>Introduction<br>
-</a><ul class="toc"><li class="tocline"><a href="#conventions" class="tocxref"><span class="secno">1.1 </span>Conventions</a></li><li class="tocline"><a href="#purpose" class="tocxref"><span class="secno">1.2 </span>Purpose of this document</a></li><li class="tocline"><a href="#structure-of-this-document" class="tocxref"><span class="secno">1.3 </span>Structure of this document</a></li><li class="tocline"><a href="#audience" class="tocxref"><span class="secno">1.4 </span> Audience </a></li></ul></li><li class="tocline"><a href="#rationale" class="tocxref"><span class="secno">2. </span>Rationale</a><ul class="toc"><li class="tocline"><a href="#entities--activities-and-agents" class="tocxref"><span class="secno">2.1 </span>Entities, Activities and Agents</a></li><li class="tocline"><a href="#events" class="tocxref"><span class="secno">2.2 </span>Events</a></li><li class="tocline"><a href="#summary-of-constraints-and-inferences" class="tocxref"><span class="secno">2.3 </span>Summary of constraints and inferences</a></li></ul></li><li class="tocline"><a href="#compliance" class="tocxref"><span class="secno">3. </span>Compliance with this document</a></li><li class="tocline"><a href="#inferences" class="tocxref"><span class="secno">4. </span>Inferences and Definitions</a><ul class="toc"><li class="tocline"><a href="#optional-identifiers-and-attributes" class="tocxref"><span class="secno">4.1 </span>Optional Identifiers and Attributes</a></li><li class="tocline"><a href="#entities-and-activities" class="tocxref"><span class="secno">4.2 </span>Entities and Activities</a></li><li class="tocline"><a href="#derivations" class="tocxref"><span class="secno">4.3 </span>Derivations</a></li><li class="tocline"><a href="#agents" class="tocxref"><span class="secno">4.4 </span>Agents</a></li><li class="tocline"><a href="#alternate-and-specialized-entities" class="tocxref"><span class="secno">4.5 </span>Alternate and Specialized Entities</a></li></ul></li><li class="tocline"><a href="#constraints" class="tocxref"><span class="secno">5. </span>Constraints</a><ul class="toc"><li class="tocline"><a href="#uniqueness-constraints" class="tocxref"><span class="secno">5.1 </span>Uniqueness Constraints</a></li><li class="tocline"><a href="#event-ordering-constraints" class="tocxref"><span class="secno">5.2 </span>Event Ordering Constraints</a><ul class="toc"><li class="tocline"><a href="#activity-constraints" class="tocxref"><span class="secno">5.2.1 </span>Activity constraints</a></li><li class="tocline"><a href="#entity-constraints" class="tocxref"><span class="secno">5.2.2 </span> Entity constraints</a></li><li class="tocline"><a href="#agent-constraints" class="tocxref"><span class="secno">5.2.3 </span> Agent constraints</a></li></ul></li><li class="tocline"><a href="#impossibility-constraints" class="tocxref"><span class="secno">5.3 </span>Impossibility constraints</a></li><li class="tocline"><a href="#type-constraints" class="tocxref"><span class="secno">5.4 </span>Type Constraints</a></li></ul></li><li class="tocline"><a href="#normalization-validity-equivalence" class="tocxref"><span class="secno">6. </span>Normalization, Validity, and Equivalence</a><ul class="toc"><li class="tocline"><a href="#bundle-constraints" class="tocxref"><span class="secno">6.1 </span>Bundles</a></li></ul></li><li class="tocline"><a href="#acknowledgements" class="tocxref"><span class="secno">A. </span>Acknowledgements</a></li><li class="tocline"><a href="#glossary" class="tocxref"><span class="secno">B. </span>Glossary</a></li><li class="tocline"><a href="#termination" class="tocxref"><span class="secno">C. </span>Termination of normalization</a></li><li class="tocline"><a href="#references" class="tocxref"><span class="secno">D. </span>References</a><ul class="toc"><li class="tocline"><a href="#normative-references" class="tocxref"><span class="secno">D.1 </span>Normative references</a></li><li class="tocline"><a href="#informative-references" class="tocxref"><span class="secno">D.2 </span>Informative references</a></li></ul></li></ul></div>
+</a><ul class="toc"><li class="tocline"><a href="#conventions" class="tocxref"><span class="secno">1.1 </span>Conventions</a></li><li class="tocline"><a href="#purpose" class="tocxref"><span class="secno">1.2 </span>Purpose of this document</a></li><li class="tocline"><a href="#structure-of-this-document" class="tocxref"><span class="secno">1.3 </span>Structure of this document</a></li><li class="tocline"><a href="#audience" class="tocxref"><span class="secno">1.4 </span> Audience </a></li></ul></li><li class="tocline"><a href="#rationale" class="tocxref"><span class="secno">2. </span>Rationale</a><ul class="toc"><li class="tocline"><a href="#entities--activities-and-agents" class="tocxref"><span class="secno">2.1 </span>Entities, Activities and Agents</a></li><li class="tocline"><a href="#events" class="tocxref"><span class="secno">2.2 </span>Events</a></li><li class="tocline"><a href="#validation-process-overview-1" class="tocxref"><span class="secno"><span class="insert">2.3 </span></span><span class="insert">Validation Process Overview</span></a></li><li class="tocline"><a href="#summary-of-constraints-and-inferences" class="tocxref"><span class="secno"><span class="delete">2.3</span><span class="insert">2.4</span> </span>Summary of constraints and inferences</a></li></ul></li><li class="tocline"><a href="#compliance" class="tocxref"><span class="secno">3. </span>Compliance with this document</a></li><li class="tocline"><a href="#inferences" class="tocxref"><span class="secno">4. </span><span class="insert">Definitions and </span>Inferences<span class="delete"> and Definitions</span></a><ul class="toc"><li class="tocline"><a href="#optional-identifiers-and-attributes" class="tocxref"><span class="secno">4.1 </span>Optional Identifiers and Attributes</a></li><li class="tocline"><a href="#entities-and-activities" class="tocxref"><span class="secno">4.2 </span>Entities and Activities</a></li><li class="tocline"><a href="#derivations" class="tocxref"><span class="secno">4.3 </span>Derivations</a></li><li class="tocline"><a href="#agents" class="tocxref"><span class="secno">4.4 </span>Agents</a></li><li class="tocline"><a href="#alternate-and-specialized-entities" class="tocxref"><span class="secno">4.5 </span>Alternate and Specialized Entities</a></li></ul></li><li class="tocline"><a href="#constraints" class="tocxref"><span class="secno">5. </span>Constraints</a><ul class="toc"><li class="tocline"><a href="#uniqueness-constraints" class="tocxref"><span class="secno">5.1 </span>Uniqueness Constraints</a></li><li class="tocline"><a href="#event-ordering-constraints" class="tocxref"><span class="secno">5.2 </span>Event Ordering Constraints</a><ul class="toc"><li class="tocline"><a href="#activity-constraints" class="tocxref"><span class="secno">5.2.1 </span>Activity constraints</a></li><li class="tocline"><a href="#entity-constraints" class="tocxref"><span class="secno">5.2.2 </span> Entity constraints</a></li><li class="tocline"><a href="#agent-constraints" class="tocxref"><span class="secno">5.2.3 </span> Agent constraints</a></li></ul></li><li class="tocline"><a href="#impossibility-constraints" class="tocxref"><span class="secno">5.3 </span>Impossibility constraints</a></li><li class="tocline"><a href="#type-constraints" class="tocxref"><span class="secno">5.4 </span>Type Constraints</a></li></ul></li><li class="tocline"><a href="#normalization-validity-equivalence" class="tocxref"><span class="secno">6. </span>Normalization, Validity, and Equivalence</a><span class="delete">6.1 </span><span class="delete">Bundles</span><span class="delete">A. </span><span class="delete">Acknowledgements</span><span class="delete">B. </span><span class="delete">Glossary</span><span class="delete">C. </span><span class="delete">Termination of normalization</span></li><li class="tocline"><a href="#references" class="tocxref"><span class="secno"><span class="delete">D.</span><span class="insert">A.</span> </span>References</a><ul class="toc"><li class="tocline"><a href="#normative-references" class="tocxref"><span class="secno"><span class="delete">D.1</span><span class="insert">A.1</span> </span>Normative references</a></li><li class="tocline"><a href="#informative-references" class="tocxref"><span class="secno"><span class="delete">D.2</span><span class="insert">A.2</span> </span>Informative references</a></li></ul></li></ul></div>
@@ -590,8 +601,8 @@
<p>In this document, logical formulas contain variables written as
lower-case identifiers. Some of these <span class="delete">ariables</span><span class="insert">variables</span> 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
- variable name is mnemonic only. </p>
+ <span class="delete">(intentionally) </span>appear only once in the <span class="delete">formula; thus, the textual</span><span class="insert">formula. Such variables are</span>
+ <span class="delete">variable name is mnemonic only.</span><span class="insert">provided merely as an aid to the reader.</span> </p>
</div>
@@ -601,7 +612,7 @@
<h3><span class="secno">1.2 </span>Purpose of this document</h3>
<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.
+realizable using different <span class="delete">serializations</span><span class="insert">representations</span> such as PROV-N and PROV-O.
A PROV <dfn id="dfn-instance">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
@@ -612,31 +623,62 @@
reasoning can be safely applied. By default, PROV instances need not
be <span class="delete">valid.</span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert">.</span> </p>
-<p> This document specifies <em>inferences</em> over PROV instances
-that applications <em class="rfc2119" title="may">may</em> employ, including <em>definitions</em> of some
+<p> This document specifies <em><span class="insert">definitions</span></em><span class="insert"> of some
+provenance statements in terms of others, </span><em>inferences</em> over PROV instances
+that applications <em class="rfc2119" title="may">may</em> employ, <span class="delete">including </span><span class="delete">definitions</span><span class="insert">and also defines a class</span> of<span class="delete"> some
provenance statements in terms of others, and also defines a class of
+</span>
<a href="#dfn-valid" class="internalDFN">valid</a> PROV instances by specifying <em>constraints</em> that
-<a href="#dfn-valid" class="internalDFN">valid</a> PROV instances must satisfy. <span class="insert">There are four kinds of
-constraints: </span><em><span class="insert">uniqueness constraints</span></em><span class="insert">, </span><em><span class="insert">event ordering
-constraints</span></em><span class="insert">, </span><em><span class="insert">impossibility constraints</span></em><span class="insert">, and </span><em><span class="insert">type constraints</span></em><span class="insert">.
-</span>Applications <em class="rfc2119" title="should">should</em> produce valid
-provenance and <em class="rfc2119" title="may">may</em> reject provenance that is not <span class="delete">valid.</span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert">.</span> Applications
-<em class="rfc2119" title="should">should</em> also use definitions, inferences and constraints to normalize
+<span class="delete">valid PROV instances must satisfy. Applications </span><span class="delete">should</span><span class="delete"> produce valid
+provenance and </span><span class="delete">may</span><span class="delete"> reject provenance that is not valid. Applications
+</span><span class="delete">should</span><span class="delete"> also use definitions, inferences and constraints to normalize
PROV instances in order to determine whether two such instances convey
the same information.
-</p><p>To summarize: compliant applications use definitions,
+</span><span class="delete">To summarize: compliant applications use definitions,
inferences, and uniqueness constraints to normalize PROV instances,
-and then <span class="delete">apply</span><span class="insert">check</span> event <span class="delete">ordering constraints to determine whether the
-instance has a consistent event ordering.</span><span class="insert">ordering, impossibility, and type constraints.</span> If <span class="delete">so,</span><span class="insert">these
-checks succeed,</span> the instance is
-<a href="#dfn-valid" class="internalDFN">valid</a>, and the normal form is considered <a href="#dfn-equivalent" class="internalDFN">equivalent</a> to
-the original instance. Also, any two PROV instances that yield the
-same normal form are considered <a href="#dfn-equivalent" class="internalDFN">equivalent</a>. Further discussion
-of the semantics of PROV statements, which justifies the inferences
+and then apply event ordering constraints to determine whether the
+instance has a consistent event ordering. If so, the instance is
+</span><a href="#dfn-valid" class="internalDFN">valid</a><span class="insert"> PROV instances must satisfy. There are four kinds of
+constraints: </span><em><span class="insert">uniqueness constraints</span></em>, <span class="delete">and the normal form is considered </span><span class="delete">equivalent</span><span class="delete"> to
+the original instance. Also, any two</span><em><span class="insert">event ordering
+constraints</span></em><span class="insert">, </span><em><span class="insert">impossibility constraints</span></em><span class="insert">, and </span><em><span class="insert">type
+constraints</span></em><span class="insert">.
+Further discussion
+of the semantics of</span> PROV <span class="delete">instances that yield the
+same normal form are considered </span><span class="delete">equivalent</span><span class="delete">. Further discussion
+of the semantics of PROV </span>statements, which justifies the<span class="insert"> definitions,</span> inferences
and constraints, can be found in the formal semantics [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-SEM">PROV-SEM</a></cite>].
</p>
+
+<p><span class="insert">We define validity and equivalence in terms of a
+concept called </span><a title="normal form" href="#dfn-normal-form" class="internalDFN"><span class="insert">normalization</span></a><span class="insert">. Definitions, inferences,
+and uniqueness constraints can be applied to </span><a title="normal
+form" href="#dfn-normal-form" class="internalDFN"><span class="insert">normalize</span></a><span class="insert"> PROV instances, and event ordering, typing, and
+impossibility constraints are checked on the normal form to determine
+</span><a title="valid" href="#dfn-valid" class="internalDFN"><span class="insert">validity</span></a><span class="insert">. Equivalence of two PROV
+instances can be determined by comparing their normal forms.
+</span></p>
+<p><span class="insert">
+This document outlines an algorithm for validity checking based on
+</span><a title="normal form" href="#dfn-normal-form" class="internalDFN"><span class="insert">noramlization</span></a><span class="insert">. Applications </span><em class="rfc2119" title="may"><span class="insert">may</span></em><span class="insert"> implement
+validity and equivalence checking using normalization, as suggested
+here, or in
+any other way as long as the same instances are considered valid or
+equivalent, respectively.
+</span></p>
+
+<p><span class="insert">Checking validity or equivalence are </span><em class="rfc2119" title="recommended"><span class="insert">recommended</span></em><span class="insert">, but not required, for
+applications compliant with PROV. This specification defines how
+validity and equivalence are to be checked, if an application elects
+to support them at all.
+Applications producing provenance </span><em class="rfc2119" title="should"><span class="insert">should</span></em><span class="insert"> ensure that it is
+</span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert">, and similarly applications consuming provenance </span><em class="rfc2119" title="may"><span class="insert">may</span></em><span class="insert"> reject provenance that is not </span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert">. Applications
+which are determining whether PROV instances convey the same
+information </span><em class="rfc2119" title="should"><span class="insert">should</span></em><span class="insert"> check equivalence as specified here, and </span><em class="rfc2119" title="should"><span class="insert">should</span></em><span class="insert">
+treat equivalent instances in the same way.</span>
+</p>
</div>
<div id="structure-of-this-document" class="section">
<h3><span class="secno">1.3 </span>Structure of this document</h3>
@@ -695,8 +737,9 @@
<div id="rationale" class="informative section">
<h2><span class="secno">2. </span>Rationale</h2><p><em>This section is non-normative.</em></p>
-<p> In this section we give a high-level rationale that provides some
- further background for the constraints. </p>
+<p> <span class="delete">In this</span><span class="insert">This</span> section <span class="delete">we give</span><span class="insert">gives</span> a high-level rationale that provides some
+ further background for the <span class="delete">constraints. </span><span class="insert">constraints, but does not affect the
+technical content of the rest of the specification.</span></p>
<div id="entities--activities-and-agents" class="section">
<h3><span class="secno">2.1 </span>Entities, Activities and Agents</h3>
@@ -720,15 +763,16 @@
between its <a title="entity generation event" href="#dfn-generation-event" class="internalDFN">generation event</a>
and its <a title="entity invalidation event" href="#dfn-invalidation-event" class="internalDFN">invalidation event</a>.
An entity's attributes are established when the entity is
-created and describe the entity's situation and (partial) state
-during <span class="delete">an</span><span class="insert">the</span> entity's lifetime.</p>
+created and <span class="insert">(partially) </span>describe the entity's situation and <span class="delete">(partial) </span>state
+during <span class="delete">an</span><span class="insert">the entirety of the</span> 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 <span class="delete">are</span><span class="insert">fix</span> 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>
+may be different. Different entities that <span class="insert">fix aspects of the same
+thing </span>are <span class="delete">aspects of the same
+thing are </span>called <em><span class="delete">alternate</span><span class="insert">alternates</span></em>, and the PROV relations of
+<span class="delete">specialization and alternate</span><span class="name"><span class="insert">specializationOf</span></span><span class="insert"> and </span><span class="name"><span class="insert">alternateOf</span></span> can be used to link such entities.</p>
<p>Besides entities, a variety of other PROV objects have
attributes, including activity, generation, usage, invalidation, start, end,
@@ -750,9 +794,9 @@
over which relevant attributes of the thing are not fixed, a PROV
instance would describe multiple entities, each with its own
identifier, <a href="#lifetime" class="internalDFN">lifetime</a>, and fixed attributes, and express dependencies between
- the various entities using events. For example, if we want to
+ the various entities using <span class="delete">events.</span><i><a href="instantaneous event"><span class="insert">events</span></a></i><span class="insert">.</span> For example, <span class="delete">if we want</span><span class="insert">in order</span> to
describe the provenance of several versions of a document, involving
- attributes such as authorship that change over time, we need
+ attributes such as authorship that change over time, <span class="delete">we need</span><span class="insert">one can use</span>
different entities for the versions linked by appropriate
generation, usage, revision, and invalidation events.
</p>
@@ -766,10 +810,12 @@
attributes; this leads to potential ambiguity, which is mitigated through the
use of identifiers.</p>
-<p>An <a>activity</a> is delimited by its <a title="activity start event" href="#dfn-start-event" class="internalDFN">start</a> and its <a title="activity end event" href="#dfn-end-event" class="internalDFN">end</a> events; hence, it occurs over
+<p>An <a>activity</a><span class="insert">'s lifetime</span> is delimited by its <a title="activity start
+event" href="#dfn-start-event" class="internalDFN">start</a> and its <a title="activity end event" href="#dfn-end-event" class="internalDFN">end</a><span class="delete"> events; hence, it</span><span class="insert">
+events. It</span> occurs over
an interval delimited by two <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous
events</a>. However, an activity statement need not mention start or end time information, because they may not be known.
-An activity's attribute-value pairs are expected to describe the activity's situation during its interval, i.e. an interval between two instantaneous events, namely its <a title="activity start event" href="#dfn-start-event" class="internalDFN">start</a> event and its <a title="activity end event" href="#dfn-end-event" class="internalDFN">end</a> event.
+An activity's attribute-value pairs are expected to describe the activity's situation during its <span class="delete">interval, i.e. an interval between two instantaneous events, namely its </span><span class="delete">start</span><span class="delete"> event and its </span><span class="delete">end</span><span class="delete"> event.</span><span class="insert">lifetime.</span>
</p>
@@ -778,8 +824,8 @@
any point in its lifetime, persists during this interval, and
preserves the characteristics <span class="delete">that make it identifiable.</span><span class="insert">provided.</span> 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
+develops through <span class="delete">time, but is typically not identifiable by the
+characteristics it exhibits at any point during its duration.</span><span class="insert">time.</span> This
distinction is similar to the distinction between 'continuant' and
'occurrent' in logic [<cite><a class="bibref" rel="biblioentry" href="#bib-Logic">Logic</a></cite>].</p>
@@ -792,7 +838,7 @@
in many different contexts within individual systems and across the
Web. Different systems may use different clocks which may not be
precisely synchronized, so when provenance statements are combined by
-different systems, we may not be able to align the times involved to a
+different systems, <span class="delete">we</span><span class="insert">an application</span> may not be able to align the times involved to a
single global timeline. Hence, PROV is designed to minimize
assumptions about time. Instead, PROV talks about (identified)
events. </p>
@@ -823,18 +869,20 @@
<p>An <dfn id="dfn-end-event">activity end event</dfn> is the <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> that marks the instant an activity ends.</p>
-<p>An <dfn id="dfn-generation-event"><span class="insert">entity generation event</span></dfn><span class="insert"> is the </span><a title="instantaneous event" href="#dfn-event" class="internalDFN"><span class="insert">instantaneous event</span></a><span class="insert"> 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.</span></p>
-
-
-<p><span class="insert">An </span><dfn id="dfn-usage-event">entity usage event</dfn> is the <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> that marks the first instant of
+<p>An <span class="delete">entity usage event</span><span class="delete"> is the </span><span class="delete">instantaneous event</span><span class="delete"> 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>
-
-<span class="delete">An </span><span class="delete">entity generation event</span><span class="delete"> is the </span><span class="delete">instantaneous event</span><span class="delete"> 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.</span>
-
-
+the entity had not begun to be used by the activity.</span>
+
+<span class="delete">An </span><dfn id="dfn-generation-event">entity generation event</dfn> is the <a title="instantaneous event" href="#dfn-event" class="internalDFN">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><span class="insert">An </span><dfn id="dfn-usage-event"><span class="insert">entity usage event</span></dfn><span class="insert"> is the </span><a title="instantaneous event" href="#dfn-event" class="internalDFN"><span class="insert">instantaneous event</span></a><span class="insert"> that marks the first instant of
+an entity's consumption timespan by an activity. The described usage
+had not started before this instant, although the activity could
+potentially have used the same entity at a different time.</span></p>
<p>An <dfn id="dfn-invalidation-event">entity invalidation event</dfn>
@@ -845,8 +893,26 @@
</div>
+<div id="validation-process-overview-1" class="section">
+<h3><span class="secno">2.3 </span><span class="insert">Validation Process Overview</span></h3>
+
+<div style="text-align: center;">
+<span class="figure">
+<img src="images/constraints/prov-c.graffle.svg/overview.svg" alt="validation process overview">
+<br>
+<span class="figcaption" id="validation-process-overview"><span class="insert">Figure 1</span><sup><a class="internalDFN" href="#validation-process-overview"><span class="diamond"><span class="insert"> ◊:</span></span></a></sup><span class="insert"> Overview of the Validation Process</span></span>
+</span>
+</div>
+
+<div class="note"><span class="insert">
+ James to add prose
+ </span></div>
+
+
+</div>
+
<div id="summary-of-constraints-and-inferences" class="section">
-<h3><span class="secno">2.3 </span>Summary of constraints and inferences</h3>
+<h3><span class="secno"><span class="insert">2.4</span> </span>Summary of constraints and inferences</h3>
<p><a href="">Table <span class="delete">5</span><span class="insert">1</span></a> summarizes the definitions, inferences, and
constraints of this document.
@@ -1118,27 +1184,35 @@
<p>
For the purpose of compliance, the normative sections of this document
- are <a href="#compliance" class="sectionRef">section 3. Compliance with this document</a>, <a href="#inferences" class="sectionRef">section 4. Inferences and Definitions</a>, <a href="#constraints" class="sectionRef">section 5. Constraints</a>, and <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>.
+ are <a href="#compliance" class="sectionRef">section 3. Compliance with this document</a>, <a href="#inferences" class="sectionRef">section 4. <span class="insert">Definitions and </span>Inferences<span class="delete"> and Definitions</span></a>, <a href="#constraints" class="sectionRef">section 5. Constraints</a>, and <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>.
To be compliant:
</p><ol><li>When processing provenance, an
- application <em class="rfc2119" title="may">may</em> apply the inferences and definitions in <a href="#inferences" class="sectionRef">section 4. Inferences and Definitions</a>.</li>
- <li>When determining whether a PROV instance is <a href="#dfn-valid" class="internalDFN">valid</a>, an
+ application <em class="rfc2119" title="may">may</em> apply the inferences and definitions in <a href="#inferences" class="sectionRef">section 4. <span class="insert">Definitions and </span>Inferences<span class="delete"> and Definitions</span></a>.</li>
+ <li><span class="delete">When</span><span class="insert">If</span> determining whether a PROV instance is <a href="#dfn-valid" class="internalDFN">valid</a>, an
application <em class="rfc2119" title="must">must</em> check that all of the
constraints of <a href="#constraints" class="sectionRef">section 5. Constraints</a> are
- satisfied on the <a href="#dfn-normal-form" class="internalDFN">normal form</a> of the instance.</li>
- <li> When producing provenance meant for other applications to
+ satisfied on the <a href="#dfn-normal-form" class="internalDFN">normal form</a> of the instance. </li>
+ <li> <span class="delete">When</span><span class="insert">If</span> producing provenance meant for other applications to
use, the application <em class="rfc2119" title="should">should</em> produce <a href="#dfn-valid" class="internalDFN">valid</a> provenance, as specified in <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>. </li>
- <li>When determining whether two PROV instances are
+ <li><span class="delete">When</span><span class="insert">If</span> determining whether two PROV instances are
<a href="#dfn-equivalent" class="internalDFN">equivalent</a>, an application <em class="rfc2119" title="must">must</em> determine whether their
normal forms are equal, as specified in <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</a>.
</li></ol>
+
+
+ <p><span class="insert">Compliant applications are not required to explicitly compute
+ normal forms; however, if checking validity or equivalence, the
+ results should be the same as would be obtained by computing normal
+ forms as defined in this specification.</span></p>
+
<p>
- All diagrams are for illustration purposes
- only. Text in appendices and
+ All <span class="delete">diagrams</span><span class="insert">figures</span> are for illustration purposes
+ only.<span class="insert"> Information in tables is normative if it appears in a
+ normative section; specifically, </span><a href="#expandable-parameters-fig"><span class="insert">Table 2</span></a><span class="insert"> is normative.</span> Text in appendices and
in boxes labeled "Remark" is informative. Where there is any apparent
ambiguity between the descriptive text and the formal text in a
"definition", "inference" or "constraint" box, the formal text takes
@@ -1152,63 +1226,104 @@
+
+
+
<div id="inferences" class="section">
-<h2><span class="secno">4. </span>Inferences and Definitions</h2>
+<h2><span class="secno">4. </span><span class="insert">Definitions and </span>Inferences<span class="delete"> and Definitions</span></h2>
<p>
-In this section, we describe <a title="inference" href="#inference" class="internalDFN">inferences</a> and <a title="definition" href="#definition" class="internalDFN">definitions</a> that <em class="rfc2119" title="may">may</em> be used on
+<span class="delete">In this section, we describe</span><span class="insert">This section describes </span><a title="definition" href="#definition" class="internalDFN"><span class="insert">definitions</span></a><span class="insert"> and</span> <a title="inference" href="#inference" class="internalDFN">inferences<span class="delete"> and </span><span class="delete">definitions</span></a> that <em class="rfc2119" title="may">may</em> be used on
provenance data, and preserve <a>equivalence</a> on <a href="#dfn-valid" class="internalDFN">valid</a>
PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef">section 6. Normalization, Validity, and Equivalence</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 <span class="insert">can be applied to
- PROV instances to replace defined expressions with definitions. A definition </span>states that a
- provenance statement is equivalent to some other <span class="delete">statements;</span><span class="insert">statements, whereas
- an inference only states one direction of an implication;</span> thus,
- defined provenance statements can be replaced by their <span class="delete">definitions,
+<span class="insert">A </span><dfn id="definition"><span class="insert">definition</span></dfn><span class="insert"> is a rule that can be applied to
+ PROV instances to replace defined expressions with definitions. </span>An <dfn id="inference">inference</dfn> is a rule that can be applied
+ to PROV instances to add new PROV statements. A definition<span class="insert"> states that a
+ provenance statement</span> is <span class="delete">a rule that</span><span class="insert">equivalent to some other statements, whereas
+ an inference only</span> states <span class="delete">that a
+ </span><span class="insert">one direction of an implication; thus,
+ defined </span>provenance <span class="delete">statement is equivalent to some other statements; thus,
+ defined provenance </span>statements can be replaced by their <span class="delete">definitions,
and vice versa.</span><span class="insert">definitions.</span>
</p>
-<p> Inferences have the following general form:</p>
-<div class="inference-example" id="inference-example"><div class="ruleTitle"><a class="internalDFN" href="#inference-example">Inference-example NNN (inference-example)</a></div>
-<p>
- <span class="conditional">IF</span> <span class="name">hyp<sub>1</sub></span> and ... and
-<span class="name">hyp<sub>k</sub></span> <span class="conditional">THEN</span>
- there exists <span class="name">a<sub>1</sub></span> and ... and <span class="name">a<sub>m</sub></span> such that <span class="name">conclusion<sub>1</sub></span> and ... and <span class="name">conclusion<sub>n</sub></span>.</p>
- </div>
+<span class="delete"> Inferences have the following general form:</span>
+<span class="delete">Inference-example NNN (inference-example)</span>
+
+ <span class="delete">IF</span> <span class="delete">hyp</span><span class="delete">1</span><span class="delete"> and ... and
+</span><span class="delete">hyp</span><span class="delete">k</span> <span class="delete">THEN</span><span class="delete">
+ there exists </span><span class="delete">a</span><span class="delete">1</span><span class="delete"> and ... and </span><span class="delete">a</span><span class="delete">m</span><span class="delete"> such that </span><span class="delete">conclusion</span><span class="delete">1</span><span class="delete"> and ... and </span><span class="delete">conclusion</span><span class="delete">n</span><span class="delete">.</span>
+
-<p> This means that if all of the provenance statements matching
- <span class="name">hyp<sub>1</sub></span>... <span class="name">hyp<sub>k</sub></span>
+<span class="delete"> This means that if all of the provenance statements matching
+ </span><span class="delete">hyp</span><span class="delete">1</span><span class="delete">... </span><span class="delete">hyp</span><span class="delete">k</span><span class="delete">
can be found in a PROV instance, we can add all of the statements
- <span class="name">concl<sub>1</sub></span> ... <span class="name">concl<sub>n</sub></span> to the instance, possibly after
- generating fresh identifiers <span class="name">a<sub>1</sub></span>,...,<span class="name">a<sub>m</sub></span> for unknown objects. These fresh
+ </span><span class="delete">concl</span><span class="delete">1</span><span class="delete"> ... </span><span class="delete">concl</span><span class="delete">n</span><span class="delete"> to the instance, possibly after
+ generating fresh identifiers </span><span class="delete">a</span><span class="delete">1</span><span class="delete">,...,</span><span class="delete">a</span><span class="delete">m</span><span class="delete"> 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
- [<cite><a class="bibref" rel="biblioentry" href="#bib-DBCONSTRAINTS">DBCONSTRAINTS</a></cite>], or to blank nodes in [<cite><a class="bibref" rel="biblioentry" href="#bib-RDF">RDF</a></cite>]. <span class="delete">With a few
- exceptions (discussed below),</span><span class="insert">In general,</span> omitted optional parameters to
- [<cite><a class="bibref" rel="biblioentry" href="#bib-PROV-N">PROV-N</a></cite>] statements, or explicit <span class="name">-</span>
+ variables in logic, "labeled nulls" in database theory [</span><span class="delete">DBCONSTRAINTS</span><span class="delete">], or to blank nodes in [</span><span class="delete">RDF</span><span class="delete">]. With a few
+ exceptions (discussed below), omitted optional parameters to
+ [</span><span class="delete">PROV-N</span><span class="delete">] statements, or explicit </span><span class="delete">-</span><span class="delete">
markers, are placeholders for existentially quantified variables;
- that is, they denote unknown values. <span class="insert">There are a few exceptions to
- this general rule, which are specified in </span><a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a></p>
+ that is, they denote unknown values. </span>
+
+
+
<p> Definitions have the following general form:</p>
<div class="definition-example" id="definition-example"><div class="ruleTitle"><a class="internalDFN" href="#definition-example">Definition-example NNN (definition-example)</a></div>
<p>
- <span class="name">defined_exp</span> holds <span class="conditional">IF AND ONLY IF</span>
- there exists <span class="name">a<sub>1</sub></span>,..., <span class="name">a<sub>m</sub></span> such that <span class="name">defining_exp<sub>1</sub></span> and ... and <span class="name">defining_exp<sub>n</sub></span>.</p>
+ <span class="name"><span class="delete">defined_exp</span><span class="delete"> holds</span><span class="insert">defined_stmt</span></span> <span class="conditional">IF AND ONLY IF</span>
+ there exists <span class="name">a<sub>1</sub></span>,..., <span class="name">a<sub>m</sub></span> such that <span class="name"><span class="delete">defining_exp</span><span class="insert">defining_stmt</span><sub>1</sub></span> and ... and <span class="name"><span class="delete">defining_exp</span><span class="insert">defining_stmt</span><sub>n</sub></span>.</p>
</div>
<p>
- This means that a provenance statement <span class="name">defined_exp</span> is defined in
- terms of other statements. This can be viewed as a two-way
- inference: If <span class="name">defined_exp</span>
- can be found in a PROV instance, we can add all of the statements
-<span class="name">defining_exp<sub>1</sub></span> ... <span class="name">defining_exp<sub>n</sub></span> to the instance, possibly after generating fresh
- identifiers <span class="name">a<sub>1</sub></span>,...,<span class="name">a<sub>m</sub></span> for unknown objects. It is safe to replace
+ <span class="delete">This means that</span><span class="insert">A definition can be applied to</span> a <span class="delete">provenance statement </span><span class="delete">defined_exp</span><span class="insert">PROV instance, since its </span><span class="name"><span class="insert">defined_stmt</span></span> is defined in
+ terms of other statements. <span class="delete">This </span><span class="insert">Applying a
+ definition to an instance means that if an occurrence of a defined
+ provenance statement </span><span class="name"><span class="insert">defined_stmt</span></span>
+ can be <span class="delete">viewed as</span><span class="insert">found in</span> a <span class="delete">two-way
+ inference: If </span><span class="delete">defined_exp</span>
+ <span class="insert">PROV instance, then we </span>can <span class="delete">be found in a PROV instance, we can</span><span class="insert">remove it and</span> add all of the statements
+<span class="name"><span class="delete">defining_exp</span><span class="insert">defining_stmt</span><sub>1</sub></span> ... <span class="name"><span class="delete">defining_exp</span><span class="insert">defining_stmt</span><sub>n</sub></span> to the instance, possibly after generating fresh
+ identifiers <span class="name">a<sub>1</sub></span>,...,<span class="name">a<sub>m</sub></span> for <span class="insert">existential variables. In
+ other words, it is safe to replace
+ a defined statement with
+ its definition.
+</span></p>
+
+
+ <p><span class="insert"> Inferences have the following general form:</span></p>
+<div class="inference-example" id="inference-example"><div class="ruleTitle"><a class="internalDFN" href="#inference-example"><span class="insert">Inference-example NNN (inference-example)</span></a></div>
+<p>
+ <span class="conditional"><span class="insert">IF</span></span> <span class="name"><span class="insert">hyp</span><sub><span class="insert">1</span></sub></span><span class="insert"> and ... and
+</span><span class="name"><span class="insert">hyp</span><sub><span class="insert">k</span></sub></span> <span class="conditional"><span class="insert">THEN</span></span><span class="insert">
+ there exists </span><span class="name"><span class="insert">a</span><sub><span class="insert">1</span></sub></span><span class="insert"> and ... and </span><span class="name"><span class="insert">a</span><sub><span class="insert">m</span></sub></span><span class="insert"> such that </span><span class="name"><span class="insert">concl</span><sub><span class="insert">1</span></sub></span><span class="insert"> and ... and </span><span class="name"><span class="insert">concl</span><sub><span class="insert">n</span></sub></span><span class="insert">.</span></p>
+ </div>
+
+<p><span class="insert"> Inferences can be applied to PROV instances. Applying an inference to an instance means that if all of the provenance statements matching
+ </span><span class="name"><span class="insert">hyp</span><sub><span class="insert">1</span></sub></span><span class="insert">... </span><span class="name"><span class="insert">hyp</span><sub><span class="insert">k</span></sub></span><span class="insert">
+ can be found in the instance, then we check whether the conclusion
+ </span><span class="name"><span class="insert">concl</span><sub><span class="insert">1</span></sub></span><span class="insert"> ... </span><span class="name"><span class="insert">concl</span><sub><span class="insert">n</span></sub></span><span class="insert"> is satisfied for some values
+ of existential variables. If so, application of the inference has
+ no effect on the instance. If not, then a copy the
+ conclusion should be added to the instance, after
+ generating fresh identifiers </span><span class="name"><span class="insert">a</span><sub><span class="insert">1</span></sub></span><span class="insert">,...,</span><span class="name"><span class="insert">a</span><sub><span class="insert">m</span></sub></span><span class="insert"> for the existential variables. 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, to "labeled nulls" in database theory
+ [</span><cite><a class="bibref" rel="biblioentry" href="#bib-DBCONSTRAINTS"><span class="insert">DBCONSTRAINTS</span></a></cite><span class="insert">], or to blank nodes in [</span><cite><a class="bibref" rel="biblioentry" href="#bib-RDF"><span class="insert">RDF</span></a></cite><span class="insert">]. In general, omitted optional parameters to
+ [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-N"><span class="insert">PROV-N</span></a></cite><span class="insert">] statements, or explicit </span><span class="name"><span class="insert">-</span></span><span class="insert">
+ markers, are placeholders for existentially quantified variables;
+ that is, they denote </span>unknown <span class="delete">objects.</span><span class="insert">values.</span> <span class="delete">It is safe</span><span class="insert">There are a few exceptions</span> to<span class="delete"> replace
a defined statement with
its definition.
-</p>
+</span><span class="insert">
+ this general rule, which are specified in </span><a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a><span class="insert">.</span></p>
+
+
<p> Definitions and inferences can be viewed as logical formulas;
similar formalisms are often used in rule-based reasoning [<cite><a class="bibref" rel="biblioentry" href="#bib-CHR">CHR</a></cite>]
and in databases [<cite><a class="bibref" rel="biblioentry" href="#bib-DBCONSTRAINTS">DBCONSTRAINTS</a></cite>]. In particular, the identifiers
@@ -1219,7 +1334,7 @@
quantified variables. Their treatment is analogous to that of blank
nodes in RDF. In contrast, distinct URIs or literal values in PROV
are assumed to be distinct for the purpose of checking validity or
- inferences. This issue is discussed in more detail under <a href="#uniqueness-constraints">Uniqueness Constraints</a> below.
+ inferences. This issue is discussed in more detail under <a href="#uniqueness-constraints">Uniqueness Constraints</a><span class="delete"> below.</span><span class="insert">.</span>
</p>
<div id="optional-identifiers-and-attributes" class="section">
@@ -1230,18 +1345,27 @@
be omitted in [<cite><span class="delete">PROV-N</span><a class="bibref" rel="biblioentry" href="#bib-PROV-O"><span class="insert">PROV-O</span></a></cite>] notation. For the purpose of inference and
validity checking, we generate special identifiers called
<dfn id="dfn-existential-variables">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 href="#dfn-existential-variables" class="internalDFN">existential variables</a>.
-<span class="delete">We note that</span><a class="rule-ref" href="#optional-identifiers"><span><span class="insert">Definition 1 (optional-identifiers)</span></span></a><span class="insert">,
-</span><a class="rule-ref" href="#optional-attributes"><span><span class="insert">Definition 2 (optional-attributes)</span></span></a><span class="insert">,
-, and
+
+</p>
+<p>
+Existential variables can be <a title="substitution" href="#dfn-substitution" class="internalDFN">substituted </a>
+ with <span class="delete">constant
+ </span><span class="insert">other terms. Specifically, a
+ </span><dfn id="dfn-substitution"><span class="insert">substitution</span></dfn><span class="insert"> is a function from a set of existential
+ variables to </span>identifiers, literals, the placeholder <span class="name">-</span>,
+ or other <a href="#dfn-existential-variables" class="internalDFN">existential variables</a>.<span class="insert"> A substitution </span><span class="math"><span class="insert">S</span></span><span class="insert"> can be
+ applied to an instance </span><span class="math"><span class="insert">I</span></span><span class="insert"> by replacing all occurrences of existential
+ variables </span><span class="math"><span class="insert">x</span></span><span class="insert"> in the instance with </span><span class="math"><span class="insert">S(x)</span></span><span class="insert">. </span></p><div class="note"><span class="insert">More explanation may be needed</span></div>
+<p></p>
+<p>
+<a class="rule-ref" href="#optional-identifiers"><span><span class="insert">Definition 1 (optional-identifiers)</span></span></a><span class="insert">,
+</span><a class="rule-ref" href="#optional-attributes"><span><span class="insert">Definition 2 (optional-attributes)</span></span></a><span class="insert">, and
</span><a class="rule-ref" href="#definition-short-forms"><span><span class="insert">Definition 3 (definition-short-forms)</span></span></a><span class="insert">,
explain how to expand the compact forms of PROV-N notation into a
- normal form.</span> <span class="delete">Definitions 1, 2, and 3 desugar compact PROV-N notation into a normal form.
-</span><a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a><span class="insert"> indicates when
+ normal form. </span><a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a><span class="insert"> indicates when
other optional parameters can be replaced by </span><a href="#dfn-existential-variables" class="internalDFN"><span class="insert">existential
- variables</span></a><span class="insert">.
+ variables</span></a><span class="insert">.</span>
+<span class="delete">We note that Definitions 1, 2, and 3 desugar compact PROV-N notation into a normal form.
</span></p>
<div class="definition" id="optional-identifiers"><div class="ruleTitle"><a class="internalDFN" href="#optional-identifiers">Definition 1 (optional-identifiers)</a></div>
@@ -1259,10 +1383,10 @@
<span class="name">actedOnBehalfOf</span>}, the following
definitional rules hold:</p>
<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"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
- <li> <span class="name"><span class="delete">r(-;a</span><span class="insert">r(-; a</span><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"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
+ <span class="name">r(a<sub>1</sub>,...,a<sub>n</sub>) </span> <span class="delete">holds </span><span class="conditional">IF AND ONLY IF</span>
+ there exists <span class="name">id</span> such that <span class="name"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>)</span><span class="delete"> holds.</span><span class="insert">.</span></li>
+ <li> <span class="name"><span class="delete">r(-;a</span><span class="insert">r(-; a</span><sub>1</sub>,...,a<sub>n</sub>) </span> <span class="delete">holds </span><span class="conditional">IF AND ONLY IF</span>
+ there exists <span class="name">id</span> such that <span class="name"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>)</span><span class="delete"> holds.</span><span class="insert">.</span></li>
</ol>
</div>
@@ -1277,8 +1401,8 @@
<span class="name">agent</span>}, if <span class="name"><span class="delete">a_n</span><span class="insert">a</span><sub><span class="insert">n</span></sub></span> is not an attribute
list parameter then the following definitional rule holds:
<p><span class="name"><span class="delete">r(a</span><span class="insert">p(a</span><sub>1</sub>,...,a<sub>n</sub>)</span>
- holds <span class="conditional">IF AND ONLY IF</span> <span class="name"><span class="delete">r(a</span><span class="insert">p(a</span><sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.
- </p></li>
+ <span class="delete">holds </span><span class="conditional">IF AND ONLY IF</span> <span class="name"><span class="delete">r(a</span><span class="insert">p(a</span><sub>1</sub>,...,a<sub>n</sub>,[])</span><span class="delete"> holds.</span><span class="insert">.
+ </span></p></li>
<li>
For each <span class="name">r</span> in {
@@ -1295,8 +1419,9 @@
<span class="name">actedOnBehalfOf</span>}, if <span class="name"><span class="delete">a_n</span><span class="insert">a</span><sub><span class="insert">n</span></sub></span> is not an
attribute list parameter then the following definition holds:
- <p> <span class="name"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>)</span> holds
- <span class="conditional">IF AND ONLY IF</span> <span class="name"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</p></li></ol>
+ <p> <span class="name"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>)</span><span class="delete"> holds
+ </span>
+ <span class="conditional">IF AND ONLY IF</span> <span class="name"><span class="delete">r(id;a</span><span class="insert">r(id; a</span><sub>1</sub>,...,a<sub>n</sub>,[])</span><span class="delete"> holds.</span><span class="insert">.</span></p></li></ol>
</div>
<p> Finally, many PROV
@@ -1334,14 +1459,14 @@
<p>
-There
- are <span class="delete">also </span>no expansion rules for entity, agent, <span class="delete">communiction,
- </span><span class="insert">communication,
- </span>attribution, influence, alternate, or specialization, because these
- have no optional parameters aside
- from the identifier and <span class="delete">attribute, </span><span class="insert">attributes,
- </span>which are expanded by <span class="delete">other
- </span><span class="insert">the </span>rules <span class="delete">above.</span><span class="insert">in </span><a class="rule-ref" href="#optional-attributes"><span><span class="insert">Definition 2 (optional-attributes)</span></span></a><span class="insert">. </span></p>
+There<span class="insert"> are no expansion rules for entity, agent, communication,
+ attribution, influence, alternate, specialization, or mention</span>
+ <span class="insert">relations, because these
+ have no optional parameters aside from the identifier and attributes,
+ which </span>are <span class="delete">also no expansion</span><span class="insert">expanded by the</span> rules <span class="delete">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.</span><span class="insert">in </span><a class="rule-ref" href="#optional-identifiers"><span><span class="insert">Definition 1 (optional-identifiers)</span></span></a> <a class="rule-ref" href="#optional-attributes"><span><span class="insert">Definition 2 (optional-attributes)</span></span></a><span class="insert">. </span></p>
</div>
@@ -1352,9 +1477,11 @@
by fresh existential variables, distinct from any others occurring in
the instance.
The only <span class="delete">exceptions,</span><span class="insert">exceptions to this general rule,</span> where <span class="name">-</span> <span class="delete">must</span><span class="insert">are to</span> be left
- in place, are the <a href="http://www.w3.org/TR/prov-dm/#derivation.activity">activity<span class="delete"> parameter</span></a><span class="insert">, </span><a href="http://www.w3.org/TR/prov-dm/#derivation.generation"><span class="insert">generation</span></a><span class="insert">, and </span><a href="http://www.w3.org/TR/prov-dm/#derivation.usage"><span class="insert">usage</span></a><span class="insert"> parameters</span> 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>.
+ in place, are the <a href="http://www.w3.org/TR/prov-dm/#derivation.activity">activity </a><span class="insert">, </span><a href="http://www.w3.org/TR/prov-dm/#derivation.generation"><span class="insert">generation</span></a><span class="insert">, and </span><a href="http://www.w3.org/TR/prov-dm/#derivation.usage"><span class="insert">usage</span></a><span class="insert"> parameters in </span><span class="name"><span class="insert">wasDerivedFrom</span></span><span class="insert"> and
+ the </span><a href="http://www.w3.org/TR/prov-dm/#association.plan"><span class="insert">plan</span></a>
+ parameter in <span class="name"><span class="delete">wasDerivedFrom</span><span class="delete"> and
+ the </span><span class="delete">plan</span><span class="delete"> parameter</span><span class="insert">wasAssociatedWith</span></span><span class="insert">. This is
+ further explained</span> in <span class="delete">wasAssociatedWith</span><span class="delete">.</span><span class="insert">remarks below.</span>
</p>
<p>The <span class="delete">following table characterizes the</span><span class="insert">treatment of optional parameters is specified formally using
@@ -1366,7 +1493,8 @@
parameter</a>s of the properties of PROV, needed in <span class="delete">the
following definition.</span><a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a><span class="insert">.</span> For emphasis, the <span class="delete">two</span><span class="insert">four</span> optional parameters
that are not <a title="expandable parameter" href="#dfn-expandable-parameter" class="internalDFN">expandable</a> are
- also listed.</p>
+ also listed.<span class="insert"> Parameters that cannot have value </span><span class="name"><span class="insert">-</span></span><span class="insert">, and identifiers that are
+ expanded by </span><a class="rule-ref" href="#optional-identifiers"><span><span class="insert">Definition 1 (optional-identifiers)</span></span></a><span class="insert">, are not listed.</span></p>
<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"><span class="insert">Table 2: Expandable and
@@ -1377,99 +1505,122 @@
<th>Expandable </th>
<th>Non-expandable</th>
</tr>
- <tr>
- <td class="name"><span class="delete">wasGeneratedBy(id;e,a,t,attrs)</span><span class="insert">wasGeneratedBy(id; e,a,t,attrs)</span></td>
- <td class="name">id,a,t</td>
- <td></td>
- </tr>
- <tr>
- <td class="name"><span class="delete">used(id;a,e,t,attrs)</span><span class="insert">used(id; a,e,t,attrs)</span></td>
- <td class="name">id,e,t</td>
- <td></td>
- </tr>
- <tr>
- <td class="name"><span class="delete">wasInformedBy(id;a2,a1,attrs)</span><span class="insert">wasInformedBy(id; a2,a1,attrs)</span></td>
- <td class="name">id</td>
- <td></td>
- </tr>
- <tr>
- <td class="name"><span class="delete">wasStartedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasStartedBy(id; a2,e,a1,t,attrs)</span></td>
- <td class="name">id,e,a1,t</td>
+ <tr>
+ <td class="name"><span class="insert">used(id; a,e,t,attrs)</span></td>
+ <td class="name"><span class="insert">e,t</span></td>
<td></td>
</tr>
<tr>
- <td class="name"><span class="delete">wasEndedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasEndedBy(id; a2,e,a1,t,attrs)</span></td>
- <td class="name">id,e,a1,t</td>
+ <td class="name"><span class="delete">wasGeneratedBy(id;e,a,t,attrs)</span><span class="insert">wasGeneratedBy(id; e,a,t,attrs)</span></td>
+ <td class="name"><span class="delete">id,a,t</span><span class="insert">a,t</span></td>
<td></td>
- </tr>
+ </tr>
<tr>
- <td class="name"><span class="delete">wasInvalidatedBy(id;e,a,t,attrs)</span><span class="insert">wasInvalidatedBy(id; e,a,t,attrs)</span></td>
- <td class="name">id,a,t</td>
+ <td class="name"><span class="delete">used(id;a,e,t,attrs)</span><span class="insert">wasInformedBy(id; a2,a1,attrs)</span></td>
+ <td class="name"><span class="delete">id,e,t</span></td>
<td></td>
</tr>
<tr>
- <td class="name"><span class="delete">wasDerivedFrom(id;e2,e1,a,g2,u1,attrs)</span><span class="insert">wasDerivedFrom(id; e2,e1,a,g2,u1,attrs)</span></td>
- <td class="name"><span class="delete">id,g2,u1</span><span class="insert">id</span></td>
- <td class="name"><span class="delete">a</span><span class="insert">a,g2,u1</span></td>
+ <td class="name"><span class="delete">wasInformedBy(id;a2,a1,attrs)</span><span class="insert">wasStartedBy(id; a2,e,a1,t,attrs)</span></td>
+ <td class="name"><span class="delete">id</span><span class="insert">e,a1,t</span></td>
+ <td></td>
</tr>
<tr>
- <td class="name"><span class="delete">wasDerivedFrom(id;e2,e1,attrs)</span><span class="insert">wasDerivedFrom(id; e2,e1,attrs)</span></td>
- <td class="name">id</td>
+ <td class="name"><span class="delete">wasStartedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasEndedBy(id; a2,e,a1,t,attrs)</span></td>
+ <td class="name"><span class="delete">id,e,a1,t</span><span class="insert">e,a1,t</span></td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name"><span class="delete">wasEndedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasInvalidatedBy(id; e,a,t,attrs)</span></td>
+ <td class="name"><span class="delete">id,e,a1,t</span><span class="insert">a,t</span></td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name"><span class="delete">wasInvalidatedBy(id;e,a,t,attrs)</span><span class="insert">wasDerivedFrom(id; e2,e1,a,g2,u1,attrs)</span></td>
+ <td class="name"><span class="delete">id,a,t</span><span class="insert">e1,e2</span></td>
+ <td class="name"><span class="insert">a,g2,u1</span></td>
+ </tr>
+
+
+ <tr>
+ <td class="name"><span class="delete">wasDerivedFrom(id;e2,e1,a,g2,u1,attrs)</span><span class="insert">wasAttributedTo(id; e,ag,attr)</span></td>
+ <td class="name"><span class="delete">id,g2,u1</span>
+ <span class="delete">a</span>
+
+
+ <span class="delete">wasDerivedFrom(id;e2,e1,attrs)</span>
+ <span class="delete">id</span></td>
<td></td>
</tr>
<tr>
- <td class="name"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAttributedTo(id; e,ag,attr)</span></td>
- <td class="name">id</td>
- <td></td>
- </tr>
- <tr>
- <td class="name"><span class="delete">wasAssociatedWith(id;a,ag,pl,attrs)</span><span class="insert">wasAssociatedWith(id; a,ag,pl,attrs)</span></td>
- <td class="name">id,ag</td>
+ <td class="name"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAssociatedWith(id; a,ag,pl,attrs)</span></td>
+ <td class="name"><span class="delete">id</span>
+
+
+
+ <span class="delete">wasAssociatedWith(id;a,ag,pl,attrs)</span>
+ <span class="delete">id,ag</span><span class="insert">ag</span></td>
<td class="name">pl</td>
</tr>
<tr>
<td class="name"><span class="delete">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span><span class="insert">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span></td>
- <td class="name">id,a</td>
+ <td class="name"><span class="delete">id,a</span><span class="insert">a</span></td>
<td></td>
</tr>
<tr>
- <td class="name"><span class="delete">wasInfluencedBy(id;e2,e1,attrs)</span><span class="insert">wasInfluencedBy(id; e2,e1,attrs)</span></td>
- <td class="name">id</td>
+ <td class="name"><span class="delete">wasInfluencedBy(id;e2,e1,attrs)</span><span class="insert">wasInfluencedBy(id; o2,o1,attrs)</span></td>
+ <td class="name"><span class="delete">id</span></td>
<td></td>
</tr>
</tbody></table>
</div>
+
+<p> <a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a><span class="insert"> states how parameters are to be expanded,
+ using the expandable parameters defined in the </span><a href="#expandable-parameters-fig"><span class="insert">Table 2</span></a><span class="insert">.</span></p>
<div class="definition" id="optional-placeholders"><div class="ruleTitle"><a class="internalDFN" href="#optional-placeholders">Definition 4 (optional-placeholders)</a></div>
- <ol><li><span class="delete">
-For each </span><span class="delete">r</span><span class="delete"> in {</span><span class="delete">entity</span><span class="delete">, </span><span class="delete">activity</span><span class="delete">,
- </span><span class="delete">agent</span><span class="delete">}, the following definition
- holds:</span>
-
- <span class="delete">r(a</span><span class="delete">0</span><span class="delete">,...,a</span><span class="delete">i-1</span><span class="delete">, -, a</span><span class="delete">i+1</span><span class="delete">, ...,a</span><span class="delete">n</span><span class="delete">) </span><span class="name"><span class="insert">activity(id,-,t2,attrs)</span></span> <span class="conditional">IF AND ONLY
- IF</span> there exists <span class="name"><span class="delete">a'</span>
- <span class="insert">t1</span></span> such that <span class="name"><span class="delete">r(a</span><span class="delete">0</span><span class="delete">,...,a</span><span class="delete">i-1</span><span class="delete">,a',a</span><span class="delete">i+1</span><span class="delete">,...,a</span><span class="delete">n</span><span class="delete">)</span><span class="insert">activity(id,t1,t2,attrs)</span></span>.
-
- </li>
-
+ <ol><li>
+
+ <span class="name"><span class="insert">activity(id,-,t2,attrs)</span></span> <span class="conditional"><span class="insert">IF AND ONLY
+ IF</span></span><span class="insert"> there exists </span><span class="name"><span class="insert">t1</span></span><span class="insert"> such that </span><span class="name"><span class="insert">activity(id,t1,t2,attrs)</span></span><span class="insert">.
+ </span></li>
<li> <span class="name"><span class="insert">activity(id,t1,-,attrs)</span></span> <span class="conditional"><span class="insert">IF AND ONLY
IF</span></span><span class="insert"> there exists </span><span class="name"><span class="insert">t2</span></span><span class="insert"> such that </span><span class="name"><span class="insert">activity(id,t1,t2,attrs)</span></span><span class="insert">.
</span></li>
- <li>For each <span class="name">r</span> in {
-<span class="name">used</span>,
-<span class="name">wasGeneratedBy</span>,
-<span class="name">wasInfluencedBy</span>,
-<span class="name">wasInvalidatedBy</span>,
-<span class="name">wasStartedBy</span>,
-<span class="name">wasEndedBy</span>,
-<span class="name">wasInformedBy</span>,
-<span class="name">wasDerivedFrom</span>,
-<span class="name">wasAttributedTo</span>,
-<span class="name">wasAssociatedWith</span>,
-<span class="name">actedOnBehalfOf</span>}, if the <span class="name">i</span>th parameter
+ <li>For each <span class="name">r</span> in {<span class="delete">entity</span>
+<span class="name"><span class="insert">used</span></span>, <span class="delete">activity</span>
+<span class="name"><span class="insert">wasGeneratedBy</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasInformedBy</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasStartedBy</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasEndedBy</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasInvalidatedBy</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasDerivedFrom</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasAttributedTo</span></span><span class="insert">,
+</span><span class="name"><span class="insert">wasAssociatedWith</span></span><span class="insert">,
+</span><span class="name"><span class="insert">actedOnBehalfOf</span></span>,
+ <span class="name"><span class="delete">agent</span><span class="delete">}, the following definition
+ holds:
+ </span>
+ <span class="delete">r(a</span><span class="delete">0</span><span class="delete">,...,a</span><span class="delete">i-1</span><span class="delete">, -, a</span><span class="delete">i+1</span><span class="delete">, ...,a</span><span class="delete">n</span><span class="delete">) </span> <span class="delete">IF AND ONLY IF</span><span class="delete"> there exists </span><span class="delete">a'</span><span class="delete">
+ such that </span><span class="delete">r(a</span><span class="delete">0</span><span class="delete">,...,a</span><span class="delete">i-1</span><span class="delete">,a',a</span><span class="delete">i+1</span><span class="delete">,...,a</span><span class="delete">n</span><span class="delete">)</span><span class="delete">.
+ </span>
+ <span class="delete">For each </span><span class="delete">r</span><span class="delete"> in {
+</span><span class="delete">used</span><span class="delete">,
+</span><span class="delete">wasGeneratedBy</span><span class="delete">,
+</span>wasInfluencedBy<span class="delete">,
+</span><span class="delete">wasInvalidatedBy</span><span class="delete">,
+</span><span class="delete">wasStartedBy</span><span class="delete">,
+</span><span class="delete">wasEndedBy</span><span class="delete">,
+</span><span class="delete">wasInformedBy</span><span class="delete">,
+</span><span class="delete">wasDerivedFrom</span><span class="delete">,
+</span><span class="delete">wasAttributedTo</span><span class="delete">,
+</span><span class="delete">wasAssociatedWith</span><span class="delete">,
+</span><span class="delete">actedOnBehalfOf</span></span>}, if the <span class="name">i</span>th parameter
of <span class="name">r</span> is an <a href="#dfn-expandable-parameter" class="internalDFN">expandable parameter</a>
- of <span class="name">r</span> then the following definition holds:
+ of <span class="name">r</span> <span class="insert">
+ as specified in </span><a href="#expandable-parameters-fig"><span class="insert">Table 2</span></a>
+then the following definition holds:
<p> <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>.
</p></li></ol>
@@ -1503,28 +1654,29 @@
-<p id="communication-generation-use-inference_text">Communication between activities is <a title="definition" href="#definition" class="internalDFN">defined</a> as the existence of an underlying
-entity generated by one activity and used by the other.</p>
+<p id="communication-generation-use-inference_text">Communication between activities <span class="delete">is </span><a title="definition" href="#definition" class="internalDFN"><span class="delete">defined</span><span class="delete"> as</span><span class="insert">implies</span></a> the existence of an underlying
+entity generated by one activity and used by the <span class="delete">other.</span><span class="insert">other, and vice versa.</span></p>
<div class="inference" id="communication-generation-use-inference"><div class="ruleTitle"><a class="internalDFN" href="#communication-generation-use-inference">Inference 5 (communication-generation-use-inference)</a></div>
<p>
<span class="conditional">IF</span>
-<span class="name"><span class="delete">wasInformedBy(_id;a2,a1,_attrs)</span><span class="insert">wasInformedBy(_id; a2,a1,_attrs)</span></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"><span class="delete">wasGeneratedBy(_id1;e,a1,_t1,[])</span><span class="delete"> and </span><span class="delete">used(_id2;a2,e,_t2,[])</span><span class="insert">wasGeneratedBy(_id1; e,a1,_t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">used(_id2; a2,e,_t2,[])</span></span> hold.</p>
+<span class="name"><span class="delete">wasInformedBy(_id;a2,a1,_attrs)</span><span class="delete">
+holds </span><span class="insert">wasInformedBy(_id; a2,a1,_attrs)</span></span>
+<span class="conditional">THEN</span>
+ there exist <span class="name">e</span>, <span class="name"><span class="delete">_id1</span><span class="insert">_gen</span></span>, <span class="name">_t1</span>, <span class="name"><span class="delete">_id2</span><span class="insert">_use</span></span>, and <span class="name">_t2</span>,
+such that <span class="name"><span class="delete">wasGeneratedBy(_id1;e,a1,_t1,[])</span><span class="delete"> and </span><span class="delete">used(_id2;a2,e,_t2,[])</span><span class="insert">wasGeneratedBy(_gen; e,a1,_t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">used(_use; a2,e,_t2,[])</span></span> hold.</p>
</div>
<p id="generation-use-communication-inference_text">
</p><div class="note">
-A final check is required on <a class="rule-text" href="#generation-use-communication-inference_text"><span><span class="insert">Inference 6 (generation-use-communication-inference)</span></span></a> this<span class="delete"> inference</span> to ensure that it does not lead to non-termination, when combined with
+A final check is required on <span class="delete">this inference</span><a class="rule-text" href="#generation-use-communication-inference_text"><span><span class="insert">Inference 6 (generation-use-communication-inference)</span></span></a> to ensure that it does not lead to non-termination, when combined with
<a class="rule-text" href="#communication-generation-use-inference_text"><span>Inference 5 (communication-generation-use-inference)</span></a>.
</div>
<div class="inference" id="generation-use-communication-inference"><div class="ruleTitle"><a class="internalDFN" href="#generation-use-communication-inference">Inference 6 (generation-use-communication-inference)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name"><span class="delete">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(_id1; e,a1,_t1,_attrs1)</span></span>
+<span class="conditional">IF</span> <span class="name"><span class="delete">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(_gen; e,a1,_t1,_attrs1)</span></span>
and <span class="name"><span class="delete">used(_id2;a2,e,_t2,_attrs2)</span><span class="insert">used(_id2; a2,e,_t2,_attrs2)</span></span> hold
<span class="conditional">THEN</span>
there exists <span class="name">_id</span>
@@ -1538,20 +1690,22 @@
<pre class="codeexample">wasInformedBy(a2,a1)
wasInformedBy(a3,a2)
</pre>
-<p> We cannot infer <span class="name">wasInformedBy(a3,a1)</span> from these statements. Indeed,
+<p> We cannot infer <span class="name">wasInformedBy(a3,a1)</span>
+ from these <span class="delete">statements.</span><span class="insert">statements alone.</span> Indeed,
from
<span class="name">wasInformedBy(a2,a1)</span>, we know that there exists <span class="name">e1</span> such that <span class="name">e1</span> was generated by <span class="name">a1</span>
and used by <span class="name">a2</span>. Likewise, from <span class="name">wasInformedBy(a3,a2)</span>, we know that there exists <span class="name">e2</span> such that <span class="name">e2</span> was generated by <span class="name">a2</span>
and used by <span class="name">a3</span>. The following illustration
shows a counterexample to transitivity. The
horizontal axis represents the event line. We see that <span class="name">e1</span> was generated after <span class="name">e2</span> was used. Furthermore, the illustration also shows that
-<span class="name">a3</span> completes before <span class="name">a1</span>. So it is impossible for <span class="name">a3</span> to have used an entity generated by <span class="name">a1</span>. This is illustrated in <a href="#counterexample-wasInformedBy">Figure 1</a>.</p>
+<span class="name">a3</span> completes before <span class="name">a1</span><span class="delete">.</span><span class="insert"> started.</span> So <span class="insert">in this example (with no other
+ information) </span>it is impossible for <span class="name">a3</span> to have used an entity generated by <span class="name">a1</span>. This is illustrated in <a href="#counterexample-wasInformedBy">Figure <span class="delete">1</span><span class="insert">2</span></a>.</p>
<div style="text-align: center;">
<span class="figure">
<img src="images/constraints/informedByNonTransitive.png" alt="non transitivity of wasInformedBy">
<br>
-<span class="figcaption" id="counterexample-wasInformedBy">Figure 1<sup><a class="internalDFN" href="#counterexample-wasInformedBy"><span class="diamond"> ◊:</span></a></sup> Counter-example for transitivity of wasInformedBy</span>
+<span class="figcaption" id="counterexample-wasInformedBy">Figure <span class="delete">1</span><span class="insert">2</span><sup><a class="internalDFN" href="#counterexample-wasInformedBy"><span class="diamond"> ◊:</span></a></sup> Counter-example for transitivity of wasInformedBy</span>
</span>
</div>
</div>
@@ -1563,15 +1717,15 @@
<p id="entity-generation-invalidation-inference_text">
-From an entity, we can infer <span class="delete">that</span><span class="insert">the</span> existence of
+From an <span class="delete">entity,</span><span class="insert">entity statement,</span> we can infer <span class="delete">that</span><span class="insert">the</span> existence of
generation and invalidation events.
</p>
<div class="inference" id="entity-generation-invalidation-inference"><div class="ruleTitle"><a class="internalDFN" href="#entity-generation-invalidation-inference">Inference 7 (entity-generation-invalidation-inference)</a></div>
<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">_id2</span>, <span class="name">_a2</span>, and <span class="name">_t2</span> such that
- <span class="name"><span class="delete">wasGeneratedBy(_id1;e,_a1,_t1,[])</span><span class="delete"> and </span><span class="delete">wasInvalidatedBy(_id2;e,_a2,_t2,[])</span><span class="insert">wasGeneratedBy(_id1; e,_a1,_t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasInvalidatedBy(_id2; e,_a2,_t2,[])</span></span>.
+<span class="name"><span class="delete">_id1</span><span class="insert">_gen</span></span>, <span class="name">_a1</span>, <span class="name">_t1</span>,
+<span class="name"><span class="delete">_id2</span><span class="insert">_inv</span></span>, <span class="name">_a2</span>, and <span class="name">_t2</span> such that
+ <span class="name"><span class="delete">wasGeneratedBy(_id1;e,_a1,_t1,[])</span><span class="delete"> and </span><span class="delete">wasInvalidatedBy(_id2;e,_a2,_t2,[])</span><span class="insert">wasGeneratedBy(_gen; e,_a1,_t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasInvalidatedBy(_inv; e,_a2,_t2,[])</span></span>.
</p></div>
@@ -1585,9 +1739,9 @@
</p>
<div class="inference" id="activity-start-end-inference"><div class="ruleTitle"><a class="internalDFN" href="#activity-start-end-inference">Inference 8 (activity-start-end-inference)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name">activity(a,t1,t2,_attrs)</span> <span class="conditional">THEN</span> there exist <span class="name">_id1</span>, <span class="name">_e1</span>, <span class="name">_id2</span>,
+<span class="conditional">IF</span> <span class="name">activity(a,t1,t2,_attrs)</span> <span class="conditional">THEN</span> there exist <span class="name"><span class="delete">_id1</span><span class="insert">_start</span></span>, <span class="name">_e1</span>, <span class="name"><span class="delete">_id2</span><span class="insert">_end</span></span>,
and <span class="name">_e2</span> such that
- <span class="name"><span class="delete">wasStartedBy(_id1;a,_e1,_a1,t1,[])</span><span class="delete"> and </span><span class="delete">wasEndedBy(_id2;a,_e2,_a2,t2,[])</span><span class="insert">wasStartedBy(_id1; a,_e1,_a1,t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasEndedBy(_id2; a,_e2,_a2,t2,[])</span></span>.
+ <span class="name"><span class="delete">wasStartedBy(_id1;a,_e1,_a1,t1,[])</span><span class="delete"> and </span><span class="delete">wasEndedBy(_id2;a,_e2,_a2,t2,[])</span><span class="insert">wasStartedBy(_start; a,_e1,_a1,t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasEndedBy(_end; a,_e2,_a2,t2,[])</span></span>.
</p></div>
@@ -1637,6 +1791,7 @@
<div class="inference" id="derivation-generation-use-inference"><div class="ruleTitle"><a class="internalDFN" href="#derivation-generation-use-inference">Inference 11 <span class="delete">(derivation-generation-use)</span><span class="insert">(derivation-generation-use-inference)</span></a></div>
<p>
+
</p><p>
<span class="conditional">IF</span> <span class="name"><span class="delete">wasDerivedFrom(_id;e2,e1,a,id2,id1,_attrs)</span><span class="insert">wasDerivedFrom(_id; e2,e1,a,gen2,use1,_attrs)</span></span>,
<span class="conditional">THEN</span> there exists <span class="name">_t1</span> and <span class="name">_t2</span> such that <span class="name"><span class="delete">used(id1;a,e1,_t1,[])</span><span class="delete"> and </span><span class="delete">wasGeneratedBy(id2;e2,a,_t2,[])</span><span class="delete"> hold.</span><span class="insert">used(use1; a,e1,_t1,[])</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasGeneratedBy(gen2; e2,a,_t2,[])</span></span><span class="insert">.</span>
@@ -1675,27 +1830,24 @@
Indeed,
</span><span class="name"><span class="insert">e1</span></span><span class="insert"> may be used multiple times by
</span><span class="name"><span class="insert">a</span></span><span class="insert">, usage </span><span class="name"><span class="insert">use</span></span><span class="insert">
-may</span> not <span class="delete">hold.</span><span class="insert">be involved in the derivation</span> <span class="delete">Informally, from </span><span class="delete">wasDerivedFrom(id;e2,e1,-,-,-,attrs)</span><span class="delete"> and </span><span class="delete">used(use;a,e1,_t1,attrs1)</span><span class="delete">, one cannot derive </span><span class="delete">wasGeneratedBy(gen;e2,a,_t2,attrs2)</span><span class="delete"> because entity </span><span class="delete">e1</span><span class="insert">(for instance, it</span> may <span class="insert">well have taken place after
-the generation of </span><span expanclass="name"><span class="insert">e2</span></span><span class="insert">).</span></p>
-
-
-<p><span class="insert">Derivation is not defined to </span>be<span class="delete"> used by many activities, whereas at most
-one activity could generate the entity </span><span class="delete">e2</span><span class="delete">.
-Even if </span><span class="delete">e2</span><span class="delete"> is used by some activity</span><span class="insert">
-transitive either. Applications may define specializations of this relation</span> that<span class="delete">
+may</span> not <span class="delete">hold.</span><span class="insert">be involved in the derivation</span> <span class="delete">Informally, from </span><span class="delete">wasDerivedFrom(id;e2,e1,-,-,-,attrs)</span><span class="delete"> and </span><span class="delete">used(use;a,e1,_t1,attrs1)</span><span class="delete">, one cannot derive </span><span class="delete">wasGeneratedBy(gen;e2,a,_t2,attrs2)</span><span class="delete"> because entity </span><span class="delete">e1</span><span class="insert">(for instance, it</span> may <span class="delete">be used by many activities, whereas at most
+one activity could generate the entity </span><span class="insert">well have taken place after
+the generation of </span><span expanclass="name">e2</span><span class="delete">.
+Even if </span><span class="delete">e2</span><span class="delete"> is used by some activity that
later generates </span><span class="delete">e1</span><span class="delete"> is generated, it is not
safe to assume that </span><span class="delete">e2</span><span class="delete"> was derived from
</span><span class="delete">e1</span><span class="delete">. Derivation is not defined to be
-transitive either, following similar reasoning as for </span><span class="delete">wasInformedBy</span><span class="delete">.</span><span class="insert"> are transitive.</span> </p>
+transitive either, following similar reasoning as for </span><span class="delete">wasInformedBy</span><span class="delete">. </span><span class="insert">).</span></p>
- </div>
+ </div>
<hr>
<p id="specific-derivation-inference_text">A derivation
specifying activity, generation and use events is a special case of
- a derivation that leaves these unspecified. (The converse is not
- the case).</p>
+ a derivation that leaves these unspecified. <span class="delete">(The</span><span class="insert">The</span> converse is not
+ the <span class="delete">case).</span><span class="insert">case because the activity parameter of derivations is
+ non-expandable in </span><a class="rule-ref" href="#optional-placeholders"><span><span class="insert">Definition 4 (optional-placeholders)</span></span></a><span class="insert">. </span></p>
<div class="inference" id="specific-derivation-inference"><div class="ruleTitle"><a class="internalDFN" href="#specific-derivation-inference">Inference 13 (specific-derivation-inference)</a></div>
<p><span class="conditional">IF</span> <span class="name"><span class="delete">wasDerivedFrom(id;e2,e1,_act,_gen,_use,attrs)</span><span class="delete">
@@ -1711,31 +1863,45 @@
<div class="inference" id="revision-is-alternate-inference"><div class="ruleTitle"><a class="internalDFN" href="#revision-is-alternate-inference">Inference 14 <span class="delete">(revision-is-alternate)</span><span class="insert">(revision-is-alternate-inference)</span></a></div>
<p>
- <span class="conditional">IF</span> <span class="name"><span class="delete">wasDerivedFrom(_id;e2,e1,[prov:type='prov:Revision'])</span><span class="insert">wasDerivedFrom(_id; e2,e1,[prov:type='prov:Revision'])</span></span>
- holds, <span class="conditional">THEN</span> <span class="name">alternateOf(e2,e1)</span> holds.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasDerivedFrom(_id;e2,e1,[prov:type='prov:Revision'])</span><span class="delete">
+ holds,</span><span class="insert">wasDerivedFrom(_id; e2,e1,_a,_g,_u,[prov:type='prov:Revision'])</span></span><span class="insert">,</span> <span class="conditional">THEN</span> <span class="name">alternateOf(e2,e1)</span><span class="delete"> holds.</span><span class="insert">. The activity </span><span class="name"><span class="insert">_a</span></span><span class="insert">,
+ generation </span><span class="name"><span class="insert">_g</span></span><span class="insert">,
+ or use </span><span class="name"><span class="insert">_u</span></span><span class="insert"> may be the placeholder </span><span class="name"><span class="insert">-</span></span><span class="insert">.</span>
</p>
</div>
+
+
+
+
+
+<div class="remark"><span class="insert">
+ There is no inference stating that </span><span class="name"><span class="insert">wasDerivedFrom</span></span><span class="insert"> is
+ transitive.
+ </span></div>
</div>
<div id="agents" class="section">
<h3><span class="secno">4.4 </span>Agents</h3>
-<p id="attribution-inference_text"> Attribution identifies an agent as responsible for an entity. An
-agent can only be responsible for an entity if it was associated with
+<p id="attribution-inference_text"> Attribution <span class="delete">identifies</span><span class="insert">is the ascribing of</span> an <span class="delete">agent as responsible for</span><span class="insert">entity to</span> an <span class="delete">entity.</span><span class="insert">agent.</span> An
+<span class="insert">entity can only be ascribed to an </span>agent <span class="delete">can only be responsible for an entity </span>if <span class="delete">it</span><span class="insert">the agent</span> was associated with
an activity that generated the entity. If the activity, generation
+
and association events are not explicit in the instance, they can
be inferred.</p>
<div class="inference" id="attribution-inference"><div class="ruleTitle"><a class="internalDFN" href="#attribution-inference">Inference 15 (attribution-inference)</a></div>
<p>
<span class="conditional">IF</span>
-<span class="name"><span class="delete">wasAttributedTo(_att;e,ag,_attrs)</span><span class="insert">wasAttributedTo(_att; e,ag,_attrs)</span></span> holds for some identifiers
-<span class="name">e</span> and <span class="name">ag</span>,
+<span class="name"><span class="delete">wasAttributedTo(_att;e,ag,_attrs)</span><span class="delete"> holds for some identifiers
+</span><span class="delete">e</span><span class="delete"> and </span><span class="delete">ag</span><span class="delete">,
+</span><span class="insert">wasAttributedTo(_att; e,ag,_attrs)</span></span>
+
<span class="conditional">THEN</span> there exist
<span class="name">a</span>,
<span class="name">_t</span>,
@@ -1772,7 +1938,8 @@
the same, and one, both, or neither can be the placeholder <span class="name">-</span>
indicating that there is no plan, because the existential variables
<span class="name">_pl1</span> and <span class="name">_pl2</span> can be replaced with constant identifiers or
- placeholders <span class="name">-</span> independently.
+ placeholders <span class="name">-</span> <span class="delete">independently.</span><span class="insert">independently, as explained
+ in the definition of </span><a href="#dfn-merging" class="internalDFN"><span class="insert">merging</span></a><span class="insert">.</span>
</div>
<hr>
@@ -1786,42 +1953,43 @@
<p>
</p><ol>
<li>
- <span class="conditional">IF</span> <span class="name"><span class="delete">wasGeneratedBy(id;e,a,t,attrs)</span><span class="insert">wasGeneratedBy(id; e,a,t,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasGeneratedBy(id;e,a,t,attrs)</span><span class="insert">wasGeneratedBy(id; e,a,_t,attrs)</span></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"><span class="delete">used(id;a,e,t,attrs)</span><span class="insert">used(id; a,e,t,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, e, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">used(id;a,e,t,attrs)</span><span class="insert">used(id; a,e,_t,attrs)</span></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"><span class="delete">wasInformedBy(id;a2,a1,attrs)</span><span class="insert">wasInformedBy(id; a2,a1,attrs)</span></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"><span class="delete">wasStartedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasStartedBy(id; a2,e,a1,t,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasStartedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasStartedBy(id; a2,e,a1,_t,attrs)</span></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"><span class="delete">wasEndedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasEndedBy(id; a2,e,a1,t,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasEndedBy(id;a2,e,a1,t,attrs)</span><span class="insert">wasEndedBy(id; a2,e,_a1,_t,attrs)</span></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"><span class="delete">wasInvalidatedBy(id;e,a,t,attrs)</span><span class="insert">wasInvalidatedBy(id; e,a,t,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasInvalidatedBy(id;e,a,t,attrs)</span><span class="insert">wasInvalidatedBy(id; e,a,_t,attrs)</span></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>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAttributedTo(id; e,ag,attr)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, ag, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAttributedTo(id; e,ag,attrs)</span></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"><span class="delete">wasAssociatedWith(id;a,ag,pl,attrs)</span><span class="insert">wasAssociatedWith(id; a,ag,pl,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, ag, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">wasAssociatedWith(id;a,ag,pl,attrs)</span><span class="insert">wasAssociatedWith(id; a,ag,_pl,attrs)</span></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"><span class="delete">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span><span class="insert">actedOnBehalfOf(id; ag2,ag1,a,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; ag2, ag1, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name"><span class="delete">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span><span class="insert">actedOnBehalfOf(id; ag2,ag1,_a,attrs)</span></span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; ag2, ag1, attrs)</span>.
</li>
</ol>
</div>
<div class="remark">
- Note that the inferences above use the same identifier for the more
- specific relationship and the influence relationship.
+ <span class="delete">Note that the</span><span class="insert">The</span> inferences above <span class="insert">permit the </span>use <span class="delete">the </span><span class="insert">of </span>same identifier for <span class="delete">the</span><span class="insert">an
+ influence relationship and a</span> more
+ specific<span class="delete"> relationship and the influence</span> relationship.
</div>
</div>
@@ -1911,9 +2079,9 @@
<div class="inference" id="specialization-attributes-inference"><div class="ruleTitle"><a class="internalDFN" href="#specialization-attributes-inference">Inference 23 <span class="delete">(specialization-attributes)</span><span class="insert">(specialization-attributes-inference)</span></a></div>
<p>
-<span class="conditional">IF</span> <span class="name">entity(e1, attrs)</span> holds for some
- attributes <span class="name">attrs</span> and <span class="name">specializationOf(e2,e1)</span> holds, <span class="conditional">THEN </span>
- <span class="name">entity(e2, attrs)</span> also holds.</p>
+<span class="conditional">IF</span> <span class="name">entity(e1, attrs)</span><span class="delete"> holds for some
+ attributes </span><span class="delete">attrs</span> and <span class="name">specializationOf(e2,e1)</span><span class="delete"> holds,</span><span class="insert">,</span> <span class="conditional">THEN </span>
+ <span class="name">entity(e2, attrs)</span><span class="delete"> also holds.</span><span class="insert">.</span></p>
</div>
@@ -1961,7 +2129,7 @@
<li> <em>event ordering constraints</em> that say that it
should be possible to arrange the
events (generation, usage, invalidation, start, end) described in a
- PROV instance into a preorder that corresponds to a sensible
+ PROV instance into a <a href="#dfn-preorder" class="internalDFN">preorder</a> that corresponds to a sensible
"history" (for example, an entity should not be generated after it
is used); and
</li>
@@ -1983,24 +2151,25 @@
existential variables, we need to be more careful to combine
partial information that might be present in multiple compatible
statements, due to inferences. Uniqueness constraints are
- enforced through <a>merging</a> pairs of statements subject to
+ enforced through <a href="#dfn-merging" class="internalDFN">merging</a> pairs of statements subject to
equalities. For example, suppose we have two activity statements
<span class="name"><span class="delete">activity(a,2011-11-16T16:00:00,t1,[a=1])</span><span class="delete"> and </span><span class="delete">activity(a,t2,2011-11-16T18:00:00,[b=2])</span><span class="insert">activity(a,2011-11-16T16:00:00,_t1,[a=1])</span></span><span class="insert"> and </span><span class="name"><span class="insert">activity(a,_t2,2011-11-16T18:00:00,[b=2])</span></span><span class="insert">, with existential variables </span><span class="name"><span class="insert">_t1</span></span><span class="insert"> and </span><span class="name"><span class="insert">_t2</span></span>. The <a>merge</a> of
these two statements (describing the same activity <span class="name">a</span>) is <span class="name">activity(a,2011-11-16T16:00:00,2011-11-16T18:00:00,[a=1,b=2])</span>. </p>
- <p> Merging can be applied
+ <p> <dfn id="dfn-merging">Merging</dfn><span class="insert"> is an operation that</span> can be applied
to a pair of terms, or a pair of attribute lists.
The result of merging is either a substitution (mapping
- existentially quantified variables to terms) or a special symbol
- <span class="name">undefined</span> indicating that the merge
+ existentially quantified variables to terms) or <span class="delete">a special symbol
+ </span><span class="delete">undefined</span><span class="insert">failure,</span> indicating that the merge
cannot be performed. Merging of pairs of terms, attribute lists,
or statements is defined as follows.</p>
<ul>
<li> If <span class="name">t</span> and <span class="name">t'</span> are concrete identifiers or values
(including the placeholder <span class="name">-</span>), then
- their <a>merge</a> exists only if they are equal, otherwise merging
- is undefined. </li>
+ their <a>merge</a> exists only if they are equal, otherwise merging<span class="delete">
+ is undefined.</span><span class="insert">
+fails.</span> </li>
<li> If <span class="name">x</span> is an existential variable
and
<span class="name">t'</span> is any term (identifier, constant,
@@ -2015,7 +2184,9 @@
<span class="name">x'</span> is an existential variable, then their
merge is the same as the merge of <span class="name">x</span> and <span class="name">t</span>.</li>
<li> The <a>merge</a> of two attribute lists <span class="name">attrs1</span> and <span class="name">attrs2</span>
- is their union, considered as unordered lists, written <span class="name">attrs1 ∪ attrs2</span>. </li>
+ is their union, considered as <span class="delete">unordered lists,</span><span class="insert">sets of key-value pairs,</span> written <span class="name">attrs1 ∪ attrs2</span>. <span class="insert"> Duplicate keys with
+ different are
+ allowed, but equal key-value pairs are merged.</span></li>
</ul>
@@ -2044,12 +2215,13 @@
validation, then </span><span class="math"><span class="insert">I</span></span><span class="insert"> is invalid, as explained in </span><a href="#normalization-validity-equivalence"><span class="insert">Section 6</span></a><span class="insert">.
</span></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>
+ <span class="math">S</span> is applied to the instance <span class="math">I</span>, yielding result <span class="math"><span class="delete">I(S)</span><span class="insert">S(I)</span></span>.</li>
</ol>
-<p> In the common case that a particular field of a relation uniquely
- determines the other fields, we call the uniqueness constraint a
- <a>key constraint</a>. Key constraints are written as follows:
+<p> <span class="delete">In the common case </span><em><dfn id="dfn-key-constraints"><span class="insert">Key constraints</span></dfn></em><span class="insert"> are uniqueness constraints
+ </span>that <span class="insert">specify that </span>a particular <span class="insert">key </span>field of a relation uniquely
+ determines the other <span class="delete">fields, we call the uniqueness constraint a
+ </span><span class="delete">key constraint</span><span class="delete">.</span><span class="insert">parameters.</span> Key constraints are written as follows:
</p>
<div class="constraint-example" id="key-example"><div class="ruleTitle"><a class="internalDFN" href="#key-example">Constraint-example NNN (key-example)</a></div>
@@ -2088,8 +2260,9 @@
<p>
</p><hr>
- <p id="key-object_text"> We assume that the various identified objects of PROV have
- unique statements describing them within a PROV instance, through
+ <p id="key-object_text"><span class="delete"> We assume that the</span><span class="insert">The</span> various identified objects of PROV <em class="rfc2119" title="must"><span class="insert">must</span></em> have
+ unique statements describing them within a <span class="insert">valid </span>PROV <span class="delete">instance,</span><span class="insert">instance.
+ This is enforced</span> through
the following key constraints:
</p>
<div class="constraint" id="key-object"><div class="ruleTitle"><a class="internalDFN" href="#key-object">Constraint 25 (key-object)</a></div>
@@ -2134,11 +2307,13 @@
<li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name"><span class="delete">wasInvalidatedBy(id;e,a,t,attrs)</span><span class="insert">wasInvalidatedBy(id; e,a,t,attrs)</span></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">wasDerivedFrom(id;<span class="delete"> e2, e1, attrs)</span><span class="delete"> statement.
+ </span>
+ <span class="delete">The identifier field </span><span class="delete">id</span><span class="delete"> is a </span><span class="delete">KEY</span><span class="delete"> for
+ the </span><span class="delete">wasDerivedFrom(id; </span> 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"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAttributedTo(id; e,ag,attr)</span></span> statement.
@@ -2164,9 +2339,9 @@
<div id="unique-generation_text">
-<p>We assume that an entity has exactly one generation and
+<p><span class="delete">We assume that an</span><span class="insert">An</span> entity has exactly one generation and
invalidation event (either or both may, however, be left implicit).
- Note that together with the key constraints above, this implies that
+ <span class="delete">Note that together</span><span class="insert">Together</span> with the key constraints above, this implies that
<span class="name">e</span> is also a key for generation and
invalidation statements.
</p>
@@ -2175,8 +2350,8 @@
<div class="constraint" id="unique-generation"><div class="ruleTitle"><a class="internalDFN" href="#unique-generation">Constraint 27 (unique-generation)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name"><span class="delete">wasGeneratedBy(id1;e,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasGeneratedBy(id2;e,_a2,_t2,_attrs2)</span><span class="insert">wasGeneratedBy(id1; e,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasGeneratedBy(id2; e,_a2,_t2,_attrs2)</span></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"><span class="delete">wasGeneratedBy(id1;e,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasGeneratedBy(id2;e,_a2,_t2,_attrs2)</span><span class="insert">wasGeneratedBy(gen1; e,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasGeneratedBy(gen2; e,_a2,_t2,_attrs2)</span></span>,
+<span class="conditional">THEN</span> <span class="name"><span class="delete">id1</span><span class="insert">gen1</span></span> =<span class="delete">id2</span> <span class="name"><span class="insert">gen2</span></span>.</p>
</div>
<hr>
@@ -2185,21 +2360,38 @@
<div class="constraint" id="unique-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#unique-invalidation">Constraint 28 (unique-invalidation)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name"><span class="delete">wasInvalidatedBy(id1;e,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasInvalidatedBy(id2;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(id1; e,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasInvalidatedBy(id2; e,_a2,_t2,_attrs2)</span></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"><span class="delete">wasInvalidatedBy(id1;e,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasInvalidatedBy(id2;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv1; e,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasInvalidatedBy(inv2; e,_a2,_t2,_attrs2)</span></span>,
+<span class="conditional">THEN</span> <span class="name"><span class="delete">id1</span><span class="insert">inv1</span></span> =<span class="delete">id2</span> <span class="name"><span class="insert">inv2</span></span>.</p>
</div>
-<p> It follows from the above constraints that the generation and
-invalidation times of
-an entity are unique, if specified.
-</p><p>
-
-
-
-</p><hr>
+<div class="remark"> <p> It follows from the above <span class="insert">uniqueness and key
+ </span>constraints that the generation and
+ invalidation <span class="insert">activities and
+ </span>times of
+ an entity are unique, if specified.
+<span class="insert"> However, because we
+ apply the constraints by merging, it is possible for a valid PROV instance
+to contain multiple statements about the same identifiers.
+ </span></p><pre><span class="insert">wasGeneratedBy(id1; e,a,-,[prov:location="Paris"])
+wasGeneratedBy(-; e,-,-,[color="Red"])
+</span></pre><span class="insert">
+ When the uniqueness and key constraints are applied, the instance is
+ </span><a title="normal form" href="#dfn-normal-form" class="internalDFN"><span class="insert">normalized</span></a><span class="insert"> to the following form:
+ </span><pre><span class="insert">wasGeneratedBy(id1; e,a,_t,[prov:location="Paris",color="Red"])
+</span></pre><span class="insert">
+ where </span><span class="name"><span class="insert">_t</span></span><span class="insert"> is a new existential variable.
+ </span><p>
+
+
+
+</p>
+</div>
+
+
+<hr>
<p id="unique-wasStartedBy_text">
-We assume that an activity has exactly one start and
+<span class="delete">We assume that an</span><span class="insert">An</span> activity has exactly one start and
end event (either or both may, however, be left implicit). Again,
together with above key constraints these constraints imply that the
activity is a key for activity start and end statements.
@@ -2207,7 +2399,7 @@
<div class="constraint" id="unique-wasStartedBy"><div class="ruleTitle"><a class="internalDFN" href="#unique-wasStartedBy">Constraint 29 (unique-wasStartedBy)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name"><span class="delete">wasStartedBy(id1;a,_e1,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasStartedBy(id2;a,_e2,_a2,_t2,_attrs2)</span><span class="insert">wasStartedBy(id1; a,_e1,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasStartedBy(id2; a,_e2,_a2,_t2,_attrs2)</span></span>, <span class="conditional">THEN</span> <span class="name"><span class="delete">id</span><span class="insert">id1</span></span> =<span class="delete">id'</span> <span class="name"><span class="insert">id2</span></span>.</p>
+<span class="conditional">IF</span> <span class="name"><span class="delete">wasStartedBy(id1;a,_e1,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasStartedBy(id2;a,_e2,_a2,_t2,_attrs2)</span><span class="insert">wasStartedBy(start1; a,_e1,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasStartedBy(start2; a,_e2,_a2,_t2,_attrs2)</span></span>, <span class="conditional">THEN</span> <span class="name"><span class="delete">id</span><span class="insert">start1</span></span> =<span class="delete">id'</span> <span class="name"><span class="insert">start2</span></span>.</p>
</div>
<hr>
@@ -2215,7 +2407,7 @@
</p><div class="constraint" id="unique-wasEndedBy"><div class="ruleTitle"><a class="internalDFN" href="#unique-wasEndedBy">Constraint 30 (unique-wasEndedBy)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name"><span class="delete">wasEndedBy(id1;a,_e1,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasEndedBy(id2;a,_e2,_a2,_t2,_attrs2)</span><span class="insert">wasEndedBy(id1; a,_e1,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasEndedBy(id2; a,_e2,_a2,_t2,_attrs2)</span></span>, <span class="conditional">THEN</span> <span class="name"><span class="delete">id</span><span class="insert">id1</span></span> =<span class="delete">id'</span> <span class="name"><span class="insert">id2</span></span>.</p>
+<span class="conditional">IF</span> <span class="name"><span class="delete">wasEndedBy(id1;a,_e1,_a1,_t1,_attrs1)</span><span class="delete"> and </span><span class="delete">wasEndedBy(id2;a,_e2,_a2,_t2,_attrs2)</span><span class="insert">wasEndedBy(end1; a,_e1,_a1,_t1,_attrs1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasEndedBy(end2; a,_e2,_a2,_t2,_attrs2)</span></span>, <span class="conditional">THEN</span> <span class="name"><span class="delete">id</span><span class="insert">end1</span></span> =<span class="delete">id'</span> <span class="name"><span class="insert">end2</span></span>.</p>
</div>
@@ -2230,7 +2422,7 @@
<div class="constraint" id="unique-startTime"><div class="ruleTitle"><a class="internalDFN" href="#unique-startTime">Constraint 31 (unique-startTime)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name">activity(a,t,_t',_attrs)</span> and <span class="name"><span class="delete">wasStartedBy(id;a,_e1,_a1,t1,_attrs1)</span><span class="insert">wasStartedBy(id; a,_e1,_a1,t1,_attrs1)</span></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"><span class="delete">activity(a,t,_t',_attrs)</span><span class="delete"> and </span><span class="delete">wasStartedBy(id;a,_e1,_a1,t1,_attrs1)</span><span class="insert">activity(a2,t1,_t2,_attrs)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasStartedBy(_start; a2,_e,_a1,t,_attrs)</span></span>, <span class="conditional">THEN</span> <span class="name"><span class="insert">t1</span></span><span class="insert">=</span><span class="name">t<span class="delete">=</span><span class="delete">t1</span></span>.</p>
</div>
<hr>
@@ -2240,7 +2432,7 @@
<div class="constraint" id="unique-endTime"><div class="ruleTitle"><a class="internalDFN" href="#unique-endTime">Constraint 32 (unique-endTime)</a></div>
<p>
-<span class="conditional">IF</span> <span class="name">activity(a,_t,t',_attrs)</span> and <span class="name"><span class="delete">wasEndedBy(id;a,_e1,_a1,t1,_attrs1)</span><span class="insert">wasEndedBy(id; a,_e1,_a1,t1,_attrs1)</span></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"><span class="delete">activity(a,_t,t',_attrs)</span><span class="delete"> and </span><span class="delete">wasEndedBy(id;a,_e1,_a1,t1,_attrs1)</span><span class="insert">activity(a2,_t1,t2,_attrs)</span></span><span class="insert"> and </span><span class="name"><span class="insert">wasEndedBy(_end; a2,_e,_a1,t,_attrs1)</span></span>, <span class="conditional">THEN</span> <span class="name"><span class="delete">t'</span><span class="insert">t2</span></span> = <span class="name"><span class="delete">t1</span><span class="insert">t</span></span>.</p>
</div>
<p>
@@ -2278,9 +2470,9 @@
<p>Given that provenance consists of a description of past entities
and activities, <a href="#dfn-valid" class="internalDFN">valid</a> provenance instances <em class="rfc2119" title="must">must</em>
-satisfy <em>ordering constraints</em> between instantaneous events, which we introduce in
+satisfy <em>ordering constraints</em> between instantaneous events, which <span class="delete">we introduce</span><span class="insert">are introduced</span> in
this section. For instance, an entity can only be used after it was
-generated; hence, we say that an entity's <a title="entity generation
+generated; <span class="delete">hence, we say that</span><span class="insert">in other words,</span> an entity's <a title="entity generation
event" href="#dfn-generation-event" class="internalDFN">generation event</a> precedes any of this
entity's <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage events</a>. Should this
ordering constraint be violated, the associated generation and
@@ -2291,23 +2483,27 @@
<p>To allow for minimalistic clock assumptions, like Lamport
[<cite><a class="bibref" rel="biblioentry" href="#bib-CLOCK">CLOCK</a></cite>], PROV relies on a notion of relative ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous events</a>,
-without using physical clocks. This specification assumes that a preorder exists between <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous events</a>.
+without using physical clocks. This specification assumes that a <a href="#dfn-preorder" class="internalDFN">preorder</a> exists between <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous events</a>.
</p>
<p>Specifically, <dfn id="dfn-precedes">precedes</dfn> is a <a href="#dfn-preorder" class="internalDFN">preorder</a>
-between <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous events</a>. When
-we say <span class="name">e1</span> precedes <span class="name">e2</span>, this means that <span class="name">e1</span>
+between <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous events</a>. <span class="delete">When
+we say </span><span class="insert">A
+constraint of the form
+</span><span class="name">e1</span> precedes <span class="name">e2</span><span class="delete">, this</span> means that <span class="name">e1</span>
happened at the same time as or before <span class="name">e2</span>.
For symmetry, <dfn id="dfn-follows">follows</dfn> is defined as the
-inverse of <a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>; that is, when we say
-<span class="name">e1</span> follows <span class="name">e2</span>,
-this means that <span class="name">e1</span> happened at the same time
+inverse of <a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>; that is, <span class="delete">when we say
+</span><span class="insert">a constraint of
+the form
+</span><span class="name">e1</span> follows <span class="name">e2</span><span class="delete">,
+this</span> means that <span class="name">e1</span> happened at the same time
as or after <span class="name">e2</span>. Both relations are
<a href="#dfn-preorder" class="internalDFN">preorder</a>s, meaning that they are <a href="#dfn-reflexive" class="internalDFN">reflexive</a> and
<a href="#dfn-transitive" class="internalDFN">transitive</a>. Moreover, we sometimes consider <em>strict</em> forms of these
-orders: we say <span class="name">e1</span> strictly precedes <span class="name">e2</span> to indicate that <span class="name">e1</span>
-happened before <span class="name">e2</span>. This is a
+orders: we say <span class="name">e1</span> <dfn id="dfn-strictly-precedes">strictly precedes</dfn> <span class="name">e2</span> to indicate that <span class="name">e1</span>
+happened before <span class="name">e2</span><span class="delete">.</span><span class="insert">, but not at the same time.</span> This is a
<a href="#dfn-transitive" class="internalDFN">transitive</a> relation. </p>
@@ -2328,15 +2524,21 @@
<p> A typical ordering constraint is as follows.</p>
<div class="constraint-example" id="ordering-example"><div class="ruleTitle"><a class="internalDFN" href="#ordering-example">Constraint-example NNN (ordering-example)</a></div>
- <p><span class="conditional">IF</span> <span class="name">hyp<sub>1</sub></span> and ... and <span class="name">hyp<sub>n</sub></span> <span class="conditional">THEN</span> <span class="name">evt1</span> <a href="#dfn-precedes" class="internalDFN">precedes</a>/<a title="precedes" href="#dfn-precedes" class="internalDFN">strictly precedes</a> <span class="name">evt2</span>. </p></div>
+ <p><span class="conditional">IF</span> <span class="name">hyp<sub>1</sub></span> and ... and <span class="name">hyp<sub>n</sub></span> <span class="conditional">THEN</span> <span class="name">evt1</span> <a href="#dfn-precedes" class="internalDFN">precedes</a>/<a href="#dfn-strictly-precedes" class="internalDFN">strictly precedes</a> <span class="name">evt2</span>. </p></div>
<p>
The conclusion of an ordering constraint is either <a href="#dfn-precedes" class="internalDFN">precedes</a>
- or <a title="precedes" href="#dfn-precedes" class="internalDFN">strictly precedes</a>. To check ordering constraints, we
- generate all <a href="#dfn-precedes" class="internalDFN">precedes</a> and <a title="precedes" href="#dfn-precedes" class="internalDFN">strictly
- precedes</a>
- relationships arising from the ordering constraints to form a directed graph, with edges marked <a href="#dfn-precedes" class="internalDFN">precedes</a> or
- <a title="precedes" href="#dfn-precedes" class="internalDFN">strictly precedes</a>, and check that there is no cycle
- containing a <a title="precedes" href="#dfn-precedes" class="internalDFN">strictly precedes</a> edge.
+ or <a href="#dfn-strictly-precedes" class="internalDFN"><span class="insert">strictly precedes</span></a><span class="insert">. One way to check
+ ordering constraints is to
+ generate all </span><a href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a><span class="insert"> and </span><a title="precedes" href="#dfn-precedes" class="internalDFN">strictly
+ precedes</a><span class="delete">. To check</span><span class="insert">
+ relationships arising from the</span> ordering <span class="delete">constraints, we
+ generate all</span><span class="insert">constraints to form a directed graph, with edges marked</span> <a href="#dfn-precedes" class="internalDFN">precedes</a> <span class="delete">and </span><span class="insert">or
+ </span><a href="#dfn-strictly-precedes" class="internalDFN">strictly
+ precedes</a><span class="delete">
+ relationships arising from the ordering constraints to form</span><span class="insert">, and check that there is no cycle
+ containing</span> a <span class="delete">directed graph, with edges marked </span><span class="delete">precedes</span><span class="delete"> or
+ </span><span class="delete">strictly precedes</span><span class="delete">, and check that there is no cycle
+ containing a </span><a href="#dfn-strictly-precedes" class="internalDFN">strictly precedes</a> edge.
</p>
@@ -2347,17 +2549,20 @@
<h4><span class="secno">5.2.1 </span>Activity constraints</h4>
<p>
-In this section we discuss constraints from the perspective of
+<span class="delete">In this</span><span class="insert">This</span> section <span class="delete">we discuss</span><span class="insert">specifies ordering</span> constraints from the perspective of
the <a href="#lifetime" class="internalDFN">lifetime</a> of an activity. An activity starts, then during
-its lifetime uses, generates or invalidates entities, and communicates with or starts
+its lifetime <span class="delete">uses, generates</span><span class="insert">can use, generate</span> or invalidates entities, <span class="delete">and communicates</span><span class="insert">communicate
+ with, start, or end
other
-activities, and finally ends. The following constraints amount to
+activities, or be associated</span> with<span class="delete"> or starts
+other
+activities,</span><span class="insert"> agents,</span> and finally<span class="insert"> it</span> ends. The following constraints amount to
checking that all of the events associated with an activity take place
within the activity's lifetime, and the start and end events mark the
start and endpoints of its lifetime.
</p>
-<p><a href="#ordering-activity">Figure 2</a> summarizes the ordering
+<p><a href="#ordering-activity">Figure <span class="delete">2</span><span class="insert">3</span></a> summarizes the ordering
constraints on activities in a
graphical manner. For this and subsequent figures, an event time line points to the
right. Activities are represented by rectangles, whereas entities are
@@ -2380,7 +2585,7 @@
<span class="figure" id="ordering-activity">
<img src="images/constraints/ordering-activity.png" alt="constraints between events">
<br>
-<span class="figcaption" id="ordering-activity-fig">Figure 2<sup><a class="internalDFN" href="#ordering-activity-fig"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering constraints for activities</span>
+<span class="figcaption" id="ordering-activity-fig">Figure <span class="delete">2</span><span class="insert">3</span><sup><a class="internalDFN" href="#ordering-activity-fig"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering constraints for activities</span>
</span>
</div>
@@ -2393,7 +2598,7 @@
The existence of an activity implies that the <a href="#dfn-start-event" class="internalDFN">activity start
event</a> always <a href="#dfn-precedes" class="internalDFN">precedes</a> the corresponding <a href="#dfn-end-event" class="internalDFN">activity end
event</a>. This is illustrated by
-<a href="#ordering-activity">Figure 2</a>
+<a href="#ordering-activity">Figure <span class="delete">2</span><span class="insert">3</span></a>
(a) and expressed by <a class="rule-ref" href="#start-precedes-end"><span>Constraint 34 (start-precedes-end)</span></a>.</p>
<div class="constraint" id="start-precedes-end"><div class="ruleTitle"><a class="internalDFN" href="#start-precedes-end">Constraint 34 (start-precedes-end)</a></div>
@@ -2412,7 +2617,7 @@
</p><hr>
<p id="usage-within-activity_text">A usage implies ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">events</a>, since the <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage event</a> had to occur during the associated activity. This is
-illustrated by <a href="#ordering-activity">Figure 2</a> (b) and expressed by <a class="rule-ref" href="#usage-within-activity"><span>Constraint 35 (usage-within-activity)</span></a>.</p>
+illustrated by <a href="#ordering-activity">Figure <span class="delete">2</span><span class="insert">3</span></a> (b) and expressed by <a class="rule-ref" href="#usage-within-activity"><span>Constraint 35 (usage-within-activity)</span></a>.</p>
<div class="constraint" id="usage-within-activity"><div class="ruleTitle"><a class="internalDFN" href="#usage-within-activity">Constraint 35 (usage-within-activity)</a></div>
<ol>
@@ -2445,7 +2650,7 @@
<p id="generation-within-activity_text">A generation implies ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">events</a>, since the <a title="entity generation event" href="#dfn-generation-event" class="internalDFN">generation event</a> had to occur during the associated activity. This is
-illustrated by <a href="#ordering-activity">Figure 2</a> (c) and expressed by <a class="rule-ref" href="#generation-within-activity"><span>Constraint 36 (generation-within-activity)</span></a>.</p>
+illustrated by <a href="#ordering-activity">Figure <span class="delete">2</span><span class="insert">3</span></a> (c) and expressed by <a class="rule-ref" href="#generation-within-activity"><span>Constraint 36 (generation-within-activity)</span></a>.</p>
<div class="constraint" id="generation-within-activity"><div class="ruleTitle"><a class="internalDFN" href="#generation-within-activity">Constraint 36 (generation-within-activity)</a></div>
<ol>
@@ -2483,7 +2688,7 @@
implies that the start event of <span class="name">a1</span> cannot
follow the end event of <span class="name">a2</span>. This is
illustrated by
-<a href="#ordering-activity">Figure 2</a>
+<a href="#ordering-activity">Figure <span class="delete">2</span><span class="insert">3</span></a>
(d) and expressed by <a class="rule-ref" href="#wasInformedBy-ordering"><span>Constraint 37 (wasInformedBy-ordering)</span></a>.</p>
<div class="constraint" id="wasInformedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasInformedBy-ordering">Constraint 37 (wasInformedBy-ordering)</a></div>
@@ -2517,8 +2722,8 @@
can be used, <span class="delete">revised, or </span>other entities can be derived from them, and
finally they<span class="delete"> may</span><span class="insert">
can</span> 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>.
+illustrated graphically in <a href="#ordering-entity">Figure <span class="delete">3</span><span class="insert">4</span></a> and
+<a href="#ordering-entity-trigger">Figure <span class="delete">4</span><span class="insert">5</span></a>.
</p>
@@ -2527,7 +2732,7 @@
<span class="figure" id="ordering-entity">
<img src="images/constraints/ordering-entity.png" alt="ordering constraints for entities">
<br>
-<span class="figcaption" id="ordering-entity-fig">Figure 3<sup><a class="internalDFN" href="#ordering-entity-fig"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering constraints for entities</span></span>
+<span class="figcaption" id="ordering-entity-fig">Figure <span class="delete">3</span><span class="insert">4</span><sup><a class="internalDFN" href="#ordering-entity-fig"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering constraints for entities</span></span>
</div>
<p>
@@ -2536,8 +2741,8 @@
<p id="generation-precedes-invalidation_text">
Generation of an entity precedes its invalidation. (This
-follows from other constraints if the entity is used, but we state it
-explicitly to cover the case of an entity that is generated and
+follows from other constraints if the entity is used, but <span class="delete">we state </span>it<span class="insert"> is stated</span>
+explicitly<span class="insert"> here</span> to cover the case of an entity that is generated and
invalidated without being used.)</p>
<div class="constraint" id="generation-precedes-invalidation"><div class="ruleTitle"><a class="internalDFN" href="#generation-precedes-invalidation">Constraint 38 (generation-precedes-invalidation)</a></div>
@@ -2561,7 +2766,7 @@
<p id="generation-precedes-usage_text">
A usage and a generation for a given entity implies ordering of <a title="instantaneous event" href="#dfn-event" class="internalDFN">events</a>, since the <a title="entity generation
event" href="#dfn-generation-event" class="internalDFN">generation event</a> had to precede the <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage event</a>. This is
-illustrated by <a href="#ordering-entity">Figure 3</a>(a) and expressed by <a class="rule-ref" href="#generation-precedes-usage"><span>Constraint 39 (generation-precedes-usage)</span></a>.</p>
+illustrated by <a href="#ordering-entity">Figure <span class="delete">3</span><span class="insert">4</span></a>(a) and expressed by <a class="rule-ref" href="#generation-precedes-usage"><span>Constraint 39 (generation-precedes-usage)</span></a>.</p>
<div class="constraint" id="generation-precedes-usage"><div class="ruleTitle"><a class="internalDFN" href="#generation-precedes-usage">Constraint 39 (generation-precedes-usage)</a></div>
<p> <span class="conditional">IF</span>
@@ -2605,7 +2810,7 @@
First, we consider derivations, where the activity and usage are known. In that case, the <a title="entity usage event" href="#dfn-usage-event" class="internalDFN">usage</a> of <span class="name">e1</span> has to precede the <a title="entity generation
event" href="#dfn-generation-event" class="internalDFN">generation</a> of <span class="name">e2</span>.
This is
-illustrated by <a href="#ordering-entity-fig">Figure 3</a> (b) and expressed by <a class="rule-ref" href="#derivation-usage-generation-ordering"><span>Constraint 41 (derivation-usage-generation-ordering)</span></a>.</p>
+illustrated by <a href="#ordering-entity-fig">Figure <span class="delete">3</span><span class="insert">4</span></a> (b) and expressed by <a class="rule-ref" href="#derivation-usage-generation-ordering"><span>Constraint 41 (derivation-usage-generation-ordering)</span></a>.</p>
<div class="constraint" id="derivation-usage-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#derivation-usage-generation-ordering">Constraint 41 (derivation-usage-generation-ordering)</a></div>
@@ -2614,7 +2819,7 @@
<span class="name"><span class="delete">wasDerivedFrom(_d;_e2,_e1,_a,gen2,use1,_attrs)</span><span class="insert">wasDerivedFrom(_d; _e2,_e1,_a,gen2,use1,_attrs)</span></span>
<span class="conditional">THEN</span>
<span class="name">use1</span>
-<a title="precedes" href="#dfn-precedes" class="internalDFN">strictly precedes</a>
+<a title="precedes" href="#dfn-precedes" class="internalDFN"><span class="delete">strictly </span>precedes</a>
<span class="name">gen2</span>.
</p>
</div>
@@ -2624,7 +2829,7 @@
<p id="derivation-generation-generation-ordering_text">
When the activity, generation or usage is unknown, a similar constraint exists, except that the constraint refers to its
generation event, as
-illustrated by <a href="#ordering-entity-fig">Figure 3</a> (c) and expressed by <a class="rule-ref" href="#derivation-generation-generation-ordering"><span>Constraint 42 (derivation-generation-generation-ordering)</span></a>.</p>
+illustrated by <a href="#ordering-entity-fig">Figure <span class="delete">3</span><span class="insert">4</span></a> (c) and expressed by <a class="rule-ref" href="#derivation-generation-generation-ordering"><span>Constraint 42 (derivation-generation-generation-ordering)</span></a>.</p>
<div class="constraint" id="derivation-generation-generation-ordering"><div class="ruleTitle"><a class="internalDFN" href="#derivation-generation-generation-ordering">Constraint 42 (derivation-generation-generation-ordering)</a></div>
<p>
@@ -2633,29 +2838,39 @@
and
</span><span class="delete">wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1)</span><span class="delete">
and
-</span><span class="delete">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span><span class="insert">wasDerivedFrom(_d; e2,e1,attrs)</span></span><span class="insert">
+</span><span class="delete">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span><span class="insert">wasDerivedFrom(_d; e2,e1,-,-,-,attrs)</span></span><span class="insert">
and
</span><span class="name"><span class="insert">wasGeneratedBy(gen1; e1,_a1,_t1,_attrs1)</span></span><span class="insert">
and
</span><span class="name"><span class="insert">wasGeneratedBy(gen2; e2,_a2,_t2,_attrs2)</span></span>
<span class="conditional">THEN</span>
<span class="name">gen1</span>
-<a title="precedes" href="#dfn-precedes" class="internalDFN">strictly precedes</a>
+<a href="#dfn-strictly-precedes" class="internalDFN">strictly precedes</a>
<span class="name">gen2</span>.
</p>
</div>
-<p>Note that event ordering is between generations of <span class="name">e1</span>
+<div class="remark">
+ <p><span class="delete">Note that</span><span class="insert">This constraint, similar to constraint 38, requires the derived
+ entity to be generated strictly following the generation of the
+ original entity. This follows from the [</span><cite><a class="bibref" rel="biblioentry" href="#bib-PROV-DM"><span class="insert">PROV-DM</span></a></cite><span class="insert">] definition of
+ derivation: </span><em><span class="insert">A derivation is a transformation of an entity into
+ another, an update of an entity resulting in a new one, or the
+ construction of a new entity based on a pre-existing entity</span></em><span class="insert">, thus
+ the derived entity must be newer than the original entity.</span></p>
+ <p><span class="insert">The</span> event ordering is between generations of <span class="name">e1</span>
and <span class="name">e2</span>, as opposed to derivation where usage is known,
which implies ordering between the usage of <span class="name">e1</span> and
generation of <span class="name">e2</span>. </p>
+
+</div>
<hr>
<p id="wasStartedBy-ordering_text">
The entity that triggered the start of an activity must exist before the activity starts.
This is
-illustrated by <a href="#ordering-entity-trigger">Figure 4</a>(a) and expressed by <a class="rule-ref" href="#wasStartedBy-ordering"><span>Constraint 43 (wasStartedBy-ordering)</span></a>.</p>
+illustrated by <a href="#ordering-entity-trigger">Figure <span class="delete">4</span><span class="insert">5</span></a>(a) and expressed by <a class="rule-ref" href="#wasStartedBy-ordering"><span>Constraint 43 (wasStartedBy-ordering)</span></a>.</p>
<div class="constraint" id="wasStartedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasStartedBy-ordering">Constraint 43 (wasStartedBy-ordering)</a></div>
@@ -2673,7 +2888,7 @@
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasStartedBy(start;_a,e,_a1,_t1,_attrs1)</span><span class="insert">wasStartedBy(start; _a,e,_a1,_t1,_attrs1)</span></span>
and
-<span class="name"><span class="delete">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span></span>
+<span class="name"><span class="delete">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; e,_a3,_t3,_attrs3)</span></span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>
@@ -2687,7 +2902,7 @@
<p id="wasEndedBy-ordering_text"> Similarly, the entity that triggered
the end of an activity must exist before the activity ends, as
illustrated by
-<a href="#ordering-entity-trigger">Figure 4</a>(b).</p>
+<a href="#ordering-entity-trigger">Figure <span class="delete">4</span><span class="insert">5</span></a>(b).</p>
<div class="constraint" id="wasEndedBy-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasEndedBy-ordering">Constraint 44 (wasEndedBy-ordering)</a></div>
@@ -2705,7 +2920,7 @@
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasEndedBy(end;_a,e,_a1,_t1,_attrs1)</span><span class="insert">wasEndedBy(end; _a,e,_a1,_t1,_attrs1)</span></span>
and
-<span class="name"><span class="delete">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span></span>
+<span class="name"><span class="delete">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; e,_a3,_t3,_attrs3)</span></span>
<span class="conditional">THEN</span>
<span class="name">end</span>
<a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>
@@ -2718,7 +2933,7 @@
<span class="figure" id="ordering-entity-trigger">
<img src="images/constraints/ordering-entity-trigger.png" alt="ordering constraints for trigger entities">
<br>
-<span class="figcaption" id="ordering-entity-trigger-fig">Figure 4<sup><a class="internalDFN" href="#ordering-entity-trigger-fig"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering constraints for trigger entities</span>
+<span class="figcaption" id="ordering-entity-trigger-fig">Figure <span class="delete">4</span><span class="insert">5</span><sup><a class="internalDFN" href="#ordering-entity-trigger-fig"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering constraints for trigger entities</span>
</span>
</div>
@@ -2772,13 +2987,13 @@
</span><span class="insert">delegation.
</span></p>
- <p>Further constraints associated with agents appear in <a href="#ordering-agents">Figure 5</a> and are discussed below.</p>
+ <p>Further constraints associated with agents appear in <a href="#ordering-agents">Figure <span class="delete">5</span><span class="insert">6</span></a> and are discussed below.</p>
<div style="text-align: center;">
<span class="figure" id="ordering-agents-fig">
<img src="images/constraints/ordering-agents.png" alt="ordering constraints for agents">
<br>
-<span class="figcaption" id="ordering-agents">Figure 5<sup><a class="internalDFN" href="#ordering-agents"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering
+<span class="figcaption" id="ordering-agents">Figure <span class="delete">5</span><span class="insert">6</span><sup><a class="internalDFN" href="#ordering-agents"><span class="diamond"> ◊:</span></a></sup> Summary of <a title="instantaneous event" href="#dfn-event" class="internalDFN">instantaneous event</a> ordering
constraints for agents</span>
</span>
</div>
@@ -2786,13 +3001,24 @@
<hr>
-<p id="wasAssociatedWith-ordering_text">An activity that was associated with an agent must have some overlap with the agent. The agent may be generated, or may only become associated with the activity, after the activity start: so, the agent is required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start.
+<p id="wasAssociatedWith-ordering_text">An activity that was
+associated with an agent must have some overlap with the agent. <span class="delete">The </span><span class="insert">Ihe
+</span>agent <em class="rfc2119" title="must"><span class="insert">must</span></em><span class="insert"> have been generated (or started), or </span><em class="rfc2119" title="must"><span class="insert">must</span></em><span class="insert"> have become
+associated with the activity, after the activity start: so, the agent </span><em class="rfc2119" title="must"><span class="insert">must</span></em><span class="insert"> exist before the activity end. Likewise, the agent </span>may be <span class="delete">generated,</span><span class="insert">destructed (or ended),</span> or may <span class="delete">only become associated</span><span class="insert">terminate its association</span> with the activity, <span class="insert">before the activity end: hence, the agent invalidation (or end) is required to happen </span>after the activity <span class="delete">start: so, the agent</span><span class="insert">start.
+This</span> is <span class="delete">required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start.
This is
-illustrated by <a href="#ordering-agents">Figure 5</a> (a) and expressed by <a class="rule-ref" href="#wasAssociatedWith-ordering"><span>Constraint 47 (wasAssociatedWith-ordering)</span></a>.</p>
+</span>illustrated by <a href="#ordering-agents">Figure <span class="delete">5</span><span class="insert">6</span></a> (a) and expressed by <a class="rule-ref" href="#wasAssociatedWith-ordering"><span>Constraint 47 (wasAssociatedWith-ordering)</span></a>.</p>
+
+
+
+
<div class="constraint" id="wasAssociatedWith-ordering"><div class="ruleTitle"><a class="internalDFN" href="#wasAssociatedWith-ordering">Constraint 47 (wasAssociatedWith-ordering)</a></div>
- <ol> <li>
+ <p><span class="insert">
+In the following inferences, </span><span class="name"><span class="insert">_pl</span></span> <em class="rfc2119" title="may"><span class="insert">may</span></em><span class="insert"> be
+ </span><span class="name"><span class="insert">-</span></span><span class="insert">.
+ </span></p><ol> <li>
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasAssociatedWith(_assoc;a,ag,_pl,_attrs)</span><span class="insert">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span></span>
and
@@ -2807,11 +3033,33 @@
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasAssociatedWith(_assoc;a,ag,_pl,_attrs)</span><span class="insert">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span></span>
and
-<span class="name"><span class="delete">wasGeneratedBy(gen;ag,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen; ag,_a1,_t1,_attrs1)</span></span>
+<span class="name"><span class="delete">wasGeneratedBy(gen;ag,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen; ag,_a3,_t3,_attrs3)</span></span>
and
-<span class="name"><span class="delete">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span><span class="insert">wasEndedBy(end; a,_e2,_a2,_t2,_attrs2)</span></span>
+<span class="name"><span class="delete">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span><span class="insert">wasEndedBy(end; a,_e4,_a4,_t4,_attrs4)</span></span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
+<a title="precedes" href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a>
+<span class="name"><span class="insert">end</span></span><span class="insert">.
+ </span></li><li>
+ <span class="conditional"><span class="insert">IF</span></span>
+<span class="name"><span class="insert">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasStartedBy(start; a,_e5,_a5,_t5,_attrs5)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasEndedBy(end1; ag,_e6,_a6,_t6,_attrs6)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">start</span></span>
+<a title="precedes" href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a>
+<span class="name"><span class="insert">end1</span></span><span class="insert">.
+ </span></li><li>
+ <span class="conditional"><span class="insert">IF</span></span>
+<span class="name"><span class="insert">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasStartedBy(start1; ag,_e7,_a7,_t7,_attrs7)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasEndedBy(end; a,_e8,_a8,_t8,_attrs8)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">start1</span></span>
<a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>
<span class="name">end</span>.
</li>
@@ -2824,10 +3072,10 @@
</p><hr>
<p id="wasAttributedTo-ordering_text">An entity that was attributed to an agent must have some overlap
-with the agent. The agent is required to exist before the entity
+with the agent. The agent <span class="delete">is required to</span><em class="rfc2119" title="must"><span class="insert">must</span></em> exist before the entity
invalidation. Likewise, the entity generation must precede the agent destruction.
This is
-illustrated by <a href="#ordering-agents">Figure 5</a> (b) and expressed by <a class="rule-ref" href="#wasAttributedTo-ordering"><span>Constraint 48 (wasAttributedTo-ordering)</span></a>.</p>
+illustrated by <a href="#ordering-agents">Figure <span class="delete">5</span><span class="insert">6</span></a> (b) and expressed by <a class="rule-ref" href="#wasAttributedTo-ordering"><span>Constraint 48 (wasAttributedTo-ordering)</span></a>.</p>
@@ -2837,22 +3085,44 @@
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasAttributedTo(_at;e,ag,_attrs)</span><span class="insert">wasAttributedTo(_at; e,ag,_attrs)</span></span>
and
-<span class="name"><span class="delete">wasGeneratedBy(gen;e,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen2; e,_a2,_t2,_attrs2)</span></span>
+<span class="name"><span class="delete">wasGeneratedBy(gen;e,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span></span>
and
-<span class="name"><span class="delete">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv1; ag,_a1,_t1,_attrs1)</span></span>
+<span class="name"><span class="delete">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; ag,_a2,_t2,_attrs2)</span></span>
<span class="conditional">THEN</span>
-<span class="name"><span class="delete">gen</span><span class="insert">gen1</span></span>
+<span class="name">gen</span>
<a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>
-<span class="name"><span class="delete">inv</span><span class="insert">inv2</span></span>.
+<span class="name">inv</span>.
</li><li>
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasAttributedTo(_at;e,ag,_attrs)</span><span class="insert">wasAttributedTo(_at; e,ag,_attrs)</span></span>
and
-<span class="name"><span class="delete">wasGeneratedBy(gen;ag,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen; ag,_a1,_t1,_attrs1)</span></span>
+<span class="name"><span class="delete">wasGeneratedBy(gen;ag,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen; ag,_a3,_t3,_attrs3)</span></span>
and
-<span class="name"><span class="delete">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span></span>
+<span class="name"><span class="delete">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span><span class="insert">wasInvalidatedBy(inv; e,_a4,_t4,_attrs4)</span></span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
+<a title="precedes" href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a>
+<span class="name"><span class="insert">inv</span></span><span class="insert">.
+ </span></li><li>
+ <span class="conditional"><span class="insert">IF</span></span>
+<span class="name"><span class="insert">wasAttributedTo(_at; e,ag,_attrs)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasGeneratedBy(gen; e,_a5,_t5,_attrs5)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasEndedBy(end; ag,_e6,_a6,_t6,_attrs6)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">gen</span></span>
+<a title="precedes" href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a>
+<span class="name"><span class="insert">end</span></span><span class="insert">.
+ </span></li><li>
+ <span class="conditional"><span class="insert">IF</span></span>
+<span class="name"><span class="insert">wasAttributedTo(_at; e,ag,_attrs)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasStartedBy(start; ag,_e7,_a7,_t7,_attrs7) </span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasInvalidatedBy(inv; e,_a8,_t8,_attrs8)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">start</span></span>
<a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>
<span class="name">inv</span>.
</li>
@@ -2866,7 +3136,9 @@
<div class="constraint" id="actedOnBehalfOf-ordering"><div class="ruleTitle"><a class="internalDFN" href="#actedOnBehalfOf-ordering">Constraint 49 (actedOnBehalfOf-ordering)</a></div>
-<p> <span class="conditional">IF</span>
+
+ <ol> <li>
+ <span class="conditional">IF</span>
<span class="name"><span class="delete">actedOnBehalfOf(_del;ag2,ag1,_a,_attrs)</span><span class="insert">actedOnBehalfOf(_del; ag2,ag1,_a,_attrs)</span></span>
and
<span class="name"><span class="delete">wasGeneratedBy(gen;ag1,_a1,_t1,_attrs1)</span><span class="insert">wasGeneratedBy(gen; ag1,_a1,_t1,_attrs1)</span></span>
@@ -2876,7 +3148,22 @@
<span class="name">gen</span>
<a title="precedes" href="#dfn-precedes" class="internalDFN">precedes</a>
<span class="name">inv</span>.
-</p>
+
+
+ </li><li>
+ <span class="conditional"><span class="insert">IF</span></span>
+<span class="name"><span class="insert">actedOnBehalfOf(_del; ag2,ag1,_a,_attrs)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasStartedBy(start; ag1,_e3,_a3,_t3,_attrs3)</span></span><span class="insert">
+and
+</span><span class="name"><span class="insert">wasEndedBy(end; ag2,_e4,_a4,_t4,_attrs4)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">start</span></span>
+<a title="precedes" href="#dfn-precedes" class="internalDFN"><span class="insert">precedes</span></a>
+<span class="name"><span class="insert">end</span></span><span class="insert">.
+ </span></li>
+ </ol>
+
</div>
</div>
@@ -2895,7 +3182,7 @@
<p><span class="conditional">IF</span> <span class="name">hyp<sub>1</sub></span> and ... and <span class="name">hyp<sub>n</sub></span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
</div>
-<p> To check an impossibility constraint on instance <span class="math">I</span>, we check whether there is
+<p> <span class="delete">To check</span><span class="insert">Checking</span> an impossibility constraint on instance <span class="math">I</span><span class="delete">, we check</span><span class="insert"> means checking</span> whether there is
any way of matching the pattern <span class="name">hyp<sub>1</sub></span>, ..., <span class="name">hyp<sub>n</sub></span>. If there
is, then checking the constraint on <span class="math">I</span> fails (which implies that
<span class="math">I</span> is invalid).
@@ -2962,9 +3249,24 @@
</div>
<div class="remark">
- Since <span class="name">wasInfluencedBy</span> is a superproperty of many other
+ <p>Since <span class="name">wasInfluencedBy</span> is a superproperty of many other
properties, it is excluded from the set of properties whose
- identifiers are required to be pairwise disjoint.
+ identifiers are required to be pairwise disjoint.<span class="insert"> The following
+ example illustrates this observation:
+ </span></p><pre><span class="insert">wasInfluencedBy(id;e2,e1)
+wasDerivedFrom(id;e2,e1)
+</span></pre><span class="insert">
+ This satisfies the disjointness constraint.
+ </span><p></p>
+ <p><span class="insert">There is, however, no
+ constraint requiring that every influence relationship is
+ accompanied by a more specific relationship having the same
+ identifier. The following valid example illustrates this observation:
+ </span></p><pre><span class="insert">wasInfluencedBy(id; e2,e1)
+</span></pre><span class="insert">
+ This is valid; there is no inferrable information about what kind
+ of influence relates </span><span class="name"><span class="insert">e2</span></span><span class="insert"> and </span><span class="name"><span class="insert">e1</span></span><span class="insert">, other than its identity.
+ </span><p></p>
</div>
<p id="impossible-object-property-overlap_text"> Identifiers of entities,
@@ -2972,8 +3274,8 @@
</p>
<div class="constraint" id="impossible-object-property-overlap"><div class="ruleTitle"><a class="internalDFN" href="#impossible-object-property-overlap">Constraint <span class="delete">53</span><span class="insert">52</span> (impossible-object-property-overlap)</a></div>
<p>
-For each <span class="name"><span class="delete">r</span><span class="insert">p</span></span> in <span class="name">entity</span>, <span class="name">activity</span>
- or <span class="name">agent</span> and for each <span class="name"><span class="delete">s</span><span class="insert">r</span></span> in {
+For each <span class="name"><span class="delete">r</span><span class="insert">p</span></span> in <span class="insert">{</span><span class="name">entity</span>, <span class="name">activity</span>
+ or <span class="name">agent</span><span class="insert">}</span> and for each <span class="name"><span class="delete">s</span><span class="insert">r</span></span> in {
<span class="name">used</span>,
<span class="name">wasGeneratedBy</span>,
<span class="name">wasInvalidatedBy</span>,
@@ -3000,8 +3302,8 @@
<h3><span class="secno">5.4 </span>Type Constraints</h3>
<p id="typing_text">The following rule establishes types denoted by identifiers from their use within expressions.
-For this, the function <span class="name">typeOf</span> gives the set of types denoted by an identifier.
-For example, <span class="name">typeOf(e)</span> returns the set of types associated with identifier <span class="name">e</span>. The function <span class="name">typeOf</span> is not a term of PROV, but a construct introduced to validate PROV statements.
+<span class="delete">For this, the</span><span class="insert">The</span> function <span class="name">typeOf</span> gives the set of types denoted by an identifier.
+<span class="delete">For example,</span><span class="insert">That is,</span> <span class="name">typeOf(e)</span> returns the set of types associated with identifier <span class="name">e</span>. The function <span class="name">typeOf</span> is not a term of PROV, but a construct introduced to validate PROV statements.
</p>
@@ -3009,7 +3311,13 @@
<p>
For any identifier <span class="name">id</span>, <span class="name">typeOf(id)</span> is a subset of {<span class="name">'entity'</span>, <span class="name">'activity'</span>, <span class="name">'agent'</span>, <span class="name">'prov:Collection'</span>, <span class="name">'prov:EmptyCollection'</span>}.
-For identifiers that do not have a type, <span class="name">typeOf</span> gives the empty set.
+For identifiers that do not have a type, <span class="name">typeOf</span> gives the empty set.<span class="insert">
+ Identifiers can have more than one type, because of subtyping
+ (e.g. </span><span class="name"><span class="insert">'prov:EmptyCollection'</span></span><span class="insert"> is a subtype of </span><span class="name"><span class="insert">'prov:Collection'</span></span><span class="insert">) or because certain types are not
+ disjoint (such as </span><span class="name"><span class="insert">'agent'</span></span><span class="insert"> and </span><span class="name"><span class="insert">'entity'</span></span><span class="insert">). The set of types
+ does not reflect all of the distinctions among objects, only those
+ relevant for checking validity. In particular, subtypes such as
+ </span><span class="name"><span class="insert">'plan'</span></span><span class="insert"> are omitted.</span>
</p>
<p>To check if a PROV instance satisfies type constraints, one obtains the types of identifiers by application of
@@ -3024,7 +3332,7 @@
<div class="constraint" id="typing"><div class="ruleTitle"><a class="internalDFN" href="#typing">Constraint <span class="delete">54</span><span class="insert">53</span> (typing)</a></div>
-<ul>
+<ol>
<li>
<span class="conditional">IF</span>
<span class="name"><span class="delete">wasGeneratedBy(gen;e,a,t,attrs)</span><span class="insert">wasGeneratedBy(gen; e,a,t,attrs)</span></span>
@@ -3106,24 +3414,43 @@
<span class="conditional">THEN</span>
<span class="name">'entity' ∈ typeOf(e2)</span> AND
<span class="name">'entity' ∈ typeOf(e1)</span> AND
-<span class="name">'activity' ∈ typeOf(a)</span>.
+<span class="name">'activity' ∈ typeOf(a)</span><span class="insert">.
+
+</span></li><li>
+<span class="conditional"><span class="insert">IF</span></span>
+ <span class="name"><span class="insert">wasDerivedFrom(id; e2, e1, -, -, -, attrs)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">'entity' ∈ typeOf(e2)</span></span><span class="insert"> AND
+</span><span class="name"><span class="insert">'entity' ∈ typeOf(e1)</span></span><span class="insert"> AND
+</span><span class="name"><span class="insert">'activity' ∈ typeOf(a)</span></span><span class="insert">.
+
+</span></li><li>
+<span class="conditional"><span class="insert">IF</span></span>
+ <span class="name"><span class="insert">wasAttributedTo(id; e,ag,attr)</span></span>
+<span class="conditional"><span class="insert">THEN</span></span>
+<span class="name"><span class="insert">'entity' ∈ typeOf(e)</span></span><span class="insert"> AND
+</span><span class="name"><span class="insert">'agent' ∈ typeOf(ag)</span></span>.
</li><li>
<span class="conditional">IF</span>
- <span class="name"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAttributedTo(id; e,ag,attr)</span></span>
+ <span class="name"><span class="delete">wasAttributedTo(id;e,ag,attr)</span><span class="insert">wasAssociatedWith(id; a,ag,pl,attrs)</span></span>
<span class="conditional">THEN</span>
-<span class="name">'entity' ∈ typeOf(e)</span> AND
-<span class="name">'agent' ∈ typeOf(ag)</span>.
+<span class="name"><span class="insert">'activity' ∈ typeOf(a)</span></span><span class="insert"> AND
+</span><span class="name"><span class="insert">'agent' ∈ typeOf(ag)</span></span><span class="insert"> AND
+</span><span class="name">'entity' ∈ <span class="delete">typeOf(e)</span><span class="delete"> AND
+</span><span class="delete">'agent' ∈ typeOf(ag)</span><span class="insert">typeOf(pl)</span></span>.
+
+
</li><li>
<span class="conditional">IF</span>
- <span class="name"><span class="delete">wasAssociatedWith(id;a,ag,pl,attrs)</span><span class="insert">wasAssociatedWith(id; a,ag,pl,attrs)</span></span>
+ <span class="name"><span class="delete">wasAssociatedWith(id;a,ag,pl,attrs)</span><span class="insert">wasAssociatedWith(id; a,ag,-,attrs)</span></span>
<span class="conditional">THEN</span>
<span class="name">'activity' ∈ typeOf(a)</span> AND
-<span class="name">'agent' ∈ typeOf(ag)</span> AND
-<span class="name">'entity' ∈ typeOf(pl)</span>.
+<span class="name">'agent' ∈ typeOf(ag)<span class="delete"> AND
+</span><span class="delete">'entity' ∈ typeOf(pl)</span></span>.
@@ -3180,9 +3507,10 @@
<span class="name">entity(c,[prov:type='prov:EmptyCollection'])</span>
<span class="conditional">THEN</span>
<span class="name">'entity' ∈ typeOf(c)</span> AND
-<span class="name">'prov:EmptyCollection' ∈ typeOf(c)</span>.
-
-</li></ul>
+<span class="name"><span class="insert">'prov:Collection' ∈ typeOf(c)</span></span><span class="insert">AND
+</span><span class="name">'prov:EmptyCollection' ∈ typeOf(c)</span>.
+
+</li></ol>
</div>
@@ -3201,13 +3529,13 @@
</div>
<div class="remark">
<span class="delete">Note that there</span><span class="insert">There</span> 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 <em class="rfc2119" title="may">may</em> assert both <span class="name">entity(a1)</span> and <span class="name">agent(a1)</span> in a valid PROV instance.
-
- <span class="insert">
+ <span class="delete">Therefore, users </span><span class="insert">For example, one can assert both </span><span class="name"><span class="insert">entity(a1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">agent(a1)</span></span><span class="insert"> 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.
-
+ agents, and one can assert both </span><span class="name"><span class="insert">activity(a1)</span></span><span class="insert"> and </span><span class="name"><span class="insert">agent(a1)</span></span><span class="insert"> in a valid PROV instance.
+ However, one should keep in mind that some specific types of agents </span>may<span class="delete"> assert</span><span class="insert"> not be suitable as activities.
+ For example, asserting statements such as </span><span class="name"><span class="insert">agent(Bob, [type=prov:Person])</span></span><span class="insert"> and </span><span class="name"><span class="insert">activity(Bob)</span></span><span class="insert"> is discouraged. In these cases, disjointness can be ensured by explicitly asserting the agent as</span> both <span class="delete">entity(a1)</span><span class="delete"> and </span><span class="delete">agent(a1)</span><span class="delete"> in a valid PROV instance.
+
+ </span><span class="insert">agent and entity, and applying </span><a class="rule-ref" href="#entity-activity-disjoint"><span><span class="insert">Constraint 54 (entity-activity-disjoint)</span></span></a><span class="insert">.
</span></div>
@@ -3255,9 +3583,10 @@
</span></div>
<p> We define the <dfn id="dfn-normal-form">normal form</dfn> of a PROV instance as the set
-of provenance statements resulting from merging to resolve all
-uniqueness constraints in the instance and applying all possible
-inference rules to this set. </p>
+of provenance statements resulting from <span class="delete">merging to resolve</span><span class="insert">applying</span> all
+<span class="insert"> definitions,
+ inferences, and </span>uniqueness <span class="delete">constraints in the instance and applying all possible
+inference rules to this set. </span><span class="insert">constraints.</span></p>
@@ -3269,7 +3598,7 @@
</li>
<li>
Apply all inferences to <span class="math">I<sub>1</sub></span> by adding the conclusion of each inference
- whose hypotheses are satisfied and whose entire conclusions do not
+ whose hypotheses are satisfied and whose entire <span class="delete">conclusions do</span><span class="insert">conclusion does</span> not
already hold (again, possibly introducing fresh existential
variables), yielding an instance <span class="math">I<sub>2</sub></span>.
</li>
@@ -3306,9 +3635,9 @@
validity:</p>
<ol>
- <li>Normalize the instance, obtaining normalized instance <span class="math">I'</span>. If
+ <li>Normalize the <span class="delete">instance,</span><span class="insert">instance #</span><i><span class="insert">#,</span> obtaining normalized instance <span class="math">I'</span>. If
normalization fails, then <span class="math">I</span> is not <a href="#dfn-valid" class="internalDFN">valid</a>.
- </li>
+ </i></li><i>
<li>Apply all event ordering constraints to <span class="math">I'</span> to build a graph <span class="math">G</span> whose nodes
are event identifiers and edges
are labeled by "precedes"
@@ -3317,17 +3646,24 @@
"strictly precedes" edge. If so, then <span class="math">I</span> is not <a href="#dfn-valid" class="internalDFN">valid</a>.
</li>
<li>
- If no
- such cycle exists, and none of the impossibility constraints <a href="#impossibility-constraints">(section 5.3)</a> and type constraints <a href="#type-constraints">(section 5.4)</a> are
- violated, then <span class="math">I</span> is <a href="#dfn-valid" class="internalDFN">valid</a>.
- </li>
- </ol>
+ <span class="insert">Apply the type constraints </span><a href="#type-constraints"><span class="insert">(section
+ 5.3)</span></a><span class="insert"> to determine whether there are any violations of
+ disjointness. </span>If <span class="delete">no
+ such cycle exists, and</span><span class="insert">so, then </span><span class="math"><span class="insert">I</span></span><span class="insert"> is not </span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a><span class="insert">.
+ </span></li><li><span class="insert">
+ Check that</span> none of the impossibility constraints <a href="#impossibility-constraints">(section <span class="delete">5.3)</span><span class="insert">5.4)</span></a> <span class="delete">and type constraints </span><span class="delete">(section 5.4)</span> are
+ <span class="insert">violated. If any are </span>violated, then <span class="math">I</span> is<span class="insert">
+ not</span> <a href="#dfn-valid" class="internalDFN">valid</a>.
+ <span class="insert"> Otherwise, #</span><i><span class="insert"># is </span><a href="#dfn-valid" class="internalDFN"><span class="insert">valid</span></a>
+ </i></li>
+ <i>
+ </i></i></ol><i><i>
<p>A normal form of a PROV instance <span class="delete">may</span><span class="insert">does</span> not exist when a uniqueness constraint fails due to merging failure. </p>
- <p>Two PROV instances are <dfn id="dfn-equivalent">equivalent</dfn> if they have the
-isomorphic normal forms (that is, after applying all possible inference
+ <p>Two PROV instances are <dfn id="dfn-equivalent">equivalent</dfn> if they have <span class="delete">the
+</span>isomorphic normal forms (that is, after applying all possible inference
rules, the two instances produce the same set of PROV statements,
up to reordering of statements and attributes within attribute lists,
and renaming of existential variables).
@@ -3337,22 +3673,27 @@
<li>
The order of provenance statements is irrelevant to the meaning of
a PROV instance. That is, a
- PROV instance is equivalent to any other instance obtained by
- permuting its statements.
+ PROV instance is equivalent to any other instance obtained by<span class="delete">
+ permuting</span><span class="insert">
+reordering</span> its statements.
</li>
<li>The order of attribute-value pairs in attribute lists is
irrelevant to the meaning of a PROV statement. That is, a PROV
statement carrying attributes is equivalent to any other statement
- obtained by permuting attribute-value pairs.
+ obtained by <span class="delete">permuting</span><span class="insert">reordering</span> attribute-value<span class="insert"> pairs and eliminating
+ duplicate</span> pairs.
</li>
<li>The particular choices of names of existential variables are irrelevant to the meaning
- of an instance; that is, the names can be permuted without changing
- the meaning. (Replacing two different names with equal names does
- change the meaning.)</li>
+ of an instance; that is, the names can be <span class="delete">permuted</span><span class="insert">renamed</span> without changing
+ the <span class="delete">meaning.</span><span class="insert">meaning, as long as different names are always replaced with
+ different names.</span> (Replacing two different names with equal <span class="delete">names</span><span class="insert">names,
+ however, can
+ change the meaning, so</span> does<span class="delete">
+ change the meaning.)</span><span class="insert"> not preserve equivalence.)</span></li>
<li>
Applying inference rules, definitions, and uniqueness constraints preserves equivalence. That is, a <a>PROV
instance</a> is equivalent to the instance obtained by applying any
- inference rule or definition, or by <a>merging</a> two statements to
+ inference rule or definition, or by <a href="#dfn-merging" class="internalDFN">merging</a> two statements to
enforce a uniqueness constraint.
</li>
<li>Equivalence is <a href="#dfn-reflexive" class="internalDFN">reflexive</a>, <a href="#dfn-symmetric" class="internalDFN">symmetric</a>, and <a href="#dfn-transitive" class="internalDFN">transitive</a>.</li>
@@ -3366,7 +3707,7 @@
<div id="bundle-constraints" class="section">
-<h3><span class="secno">6.1 </span>Bundles</h3>
+<h3><span class="delete">6.1 </span>Bundles</h3>
<p>The definitions, inferences, and constraints, and
@@ -3415,26 +3756,26 @@
</div>
-</div>
-
-
-
-
-
-
-
-
-
-
-<div class="appendix section" id="acknowledgements">
- <h2><span class="secno">A. </span>Acknowledgements</h2>
+</i></i></div><i><i>
+
+
+
+
+
+
+
+
+
+
+<div class="appendix section">
+ <span class="delete">A. </span><h2 id="acknowledgements">Acknowledgements</h2>
<p>
WG membership to be listed here.
</p>
</div>
-<div class="glossary section" id="glossary">
- <h2><span class="secno">B. </span>Glossary</h2>
+<div class="glossary section">
+ <span class="delete">B. </span><h2 id="glossary">Glossary</h2>
<ul>
<li> <dfn id="dfn-antisymmetric">antisymmetric</dfn>: A relation <span class="math">R</span> over <span class="math">X</span> is <a href="#dfn-antisymmetric" class="internalDFN">antisymmetric</a> if
@@ -3469,7 +3810,7 @@
<div class="appendix informative section" id="termination">
- <h2><span class="secno">C. </span>Termination of normalization</h2><p><em><span class="insert">This section is non-normative.</span></em></p>
+ <h2><span class="delete">C. </span>Termination of normalization</h2><p><em><span class="insert">This section is non-normative.</span></em></p>
<div class="note">TODO: give proof that normalization terminates and
produces unique normal forms.
</div>
@@ -3492,16 +3833,16 @@
-<div id="references" class="appendix section"><h2><span class="secno">D. </span>References</h2><div id="normative-references" class="section"><h3><span class="secno">D.1 </span>Normative references</h3><dl class="bibliography"><span class="delete">[PROV-N]</span><dt id="bib-RDF"><span class="insert">[RDF]</span></dt><dd><span class="delete">Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes </span><span class="insert">Graham Klyne and Jeremy J. Carroll (eds.) </span><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/"><cite><span class="delete">PROV-N: The Provenance Notation</span><span class="insert">Resource Description Framework (RDF): Concepts and Abstract Syntax</span></cite></a>. <span class="delete">2011, Working Draft.</span><span class="insert">2004, W3C Recommendation.</span> URL: <span class="delete">http://www.w3.org/TR/prov-n/</span><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210//"><span class="insert">http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/</span></a>
+</i></i><div id="references" class="appendix section"><h2><span class="secno"><span class="delete">D.</span><span class="insert">A.</span> </span>References</h2><div id="normative-references" class="section"><h3><span class="secno"><span class="delete">D.1</span><span class="insert">A.1</span> </span>Normative references</h3><dl class="bibliography"><dt id="bib-PROV-DM"><span class="insert">[PROV-DM]</span></dt><dd><span class="insert">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 </span><a href="http://www.w3.org/TR/prov-dm/"><cite><span class="insert">PROV-DM: The PROV Data Model</span></cite></a><span class="insert">. 2012, Working Draft. URL: </span><a href="http://www.w3.org/TR/prov-dm/"><span class="insert">http://www.w3.org/TR/prov-dm/</span></a>
+</dd><dt id="bib-PROV-N">[PROV-N]</dt><dd>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>
+</dd><dt id="bib-RDF"><span class="insert">[RDF]</span></dt><dd><span class="insert">Graham Klyne and Jeremy J. Carroll (eds.) </span><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/"><cite><span class="insert">Resource Description Framework (RDF): Concepts and Abstract Syntax</span></cite></a><span class="insert">. 2004, W3C Recommendation. URL: </span><a href="http://www.w3.org/TR/2004/REC-rdf-concepts-20040210//"><span class="insert">http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/</span></a>
</dd><dt id="bib-RFC2119">[RFC2119]</dt><dd>S. Bradner. <a href="http://www.ietf.org/rfc/rfc2119.txt"><cite>Key words for use in RFCs to Indicate Requirement Levels.</cite></a> March 1997. Internet RFC 2119. URL: <a href="http://www.ietf.org/rfc/rfc2119.txt">http://www.ietf.org/rfc/rfc2119.txt</a>
-</dd></dl></div><div id="informative-references" class="section"><h3><span class="secno">D.2 </span>Informative references</h3><dl class="bibliography"><dt id="bib-CHR">[CHR]</dt><dd>Thom Frühwirth <a href="http://constraint-handling-rules.org/"><cite>Constraint Handling Rules</cite></a>. Cambridge University Press URL: <a href="http://constraint-handling-rules.org/">http://constraint-handling-rules.org/</a>
+</dd></dl></div><div id="informative-references" class="section"><h3><span class="secno"><span class="delete">D.2</span><span class="insert">A.2</span> </span>Informative references</h3><dl class="bibliography"><dt id="bib-CHR">[CHR]</dt><dd>Thom Frühwirth <a href="http://constraint-handling-rules.org/"><cite>Constraint Handling Rules</cite></a>. Cambridge University Press URL: <a href="http://constraint-handling-rules.org/">http://constraint-handling-rules.org/</a>
</dd><dt id="bib-CLOCK">[CLOCK]</dt><dd>Lamport, L. <a href="http://research.microsoft.com/users/lamport/pubs/time-clocks.pdf"><cite>Time, clocks, and the ordering of events in a distributed system</cite></a>. Communications of the ACM 21 (7): 558–565. 1978. URL: <a href="http://research.microsoft.com/users/lamport/pubs/time-clocks.pdf">http://research.microsoft.com/users/lamport/pubs/time-clocks.pdf</a> DOI: doi:10.1145/359545.359563.
</dd><dt id="bib-DBCONSTRAINTS">[DBCONSTRAINTS]</dt><dd> Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, and Lucian Popa <a href="http://dx.doi.org/10.1016/j.tcs.2004.10.033"><cite>Data exchange: Semantics and query answering</cite></a>. Theoretical computer science 336(1):89-124 Elsevier URL: <a href="http://dx.doi.org/10.1016/j.tcs.2004.10.033">http://dx.doi.org/10.1016/j.tcs.2004.10.033</a>
</dd><dt id="bib-Logic">[Logic]</dt><dd>W. E. Johnson<a href="http://www.ditext.com/johnson/intro-3.html"><cite>Logic: Part III</cite></a>.1924. URL: <a href="http://www.ditext.com/johnson/intro-3.html">http://www.ditext.com/johnson/intro-3.html</a>
-</dd><dt id="bib-PROV-DM">[PROV-DM]</dt><dd>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>
-</dd><dt id="bib-PROV-N"><span class="insert">[PROV-N]</span></dt><dd><span class="insert">Luc Moreau and Paolo Missier (eds.), James Cheney, Stian Soiland-Reyes </span><a href="http://www.w3.org/TR/prov-n/"><cite><span class="insert">PROV-N: The Provenance Notation</span></cite></a><span class="insert">. 2011, Working Draft. URL: </span><a href="http://www.w3.org/TR/prov-n/"><span class="insert">http://www.w3.org/TR/prov-n/</span></a>
-</dd><dt id="bib-PROV-O"><span class="insert">[PROV-O]</span></dt><dd><span class="insert">Timothy Lebo, Satya Sahoo and Deborah McGuinness (eds.) Khalid Belhajjame, James Cheney, David Corsar, Daniel Garijo, Stian Soiland-Reyes, and Stephan Zednik </span><a href="http://www.w3.org/TR/prov-o/"><cite><span class="insert">Provenance Formal Model</span></cite></a><span class="insert">. 2011, Working Draft. URL: </span><a href="http://www.w3.org/TR/prov-o/"><span class="insert">http://www.w3.org/TR/prov-o/</span></a>
-</dd><dt id="bib-PROV-SEM">[PROV-SEM]</dt><dd>James Cheney <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman"><cite>Formal Semantics Strawman</cite></a>. 2011, Work in progress. URL: <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman">http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman
-<span class="delete">[RDF]</span><span class="delete">Graham Klyne and Jeremy J. Carroll (eds.) </span><span class="delete">Resource Description Framework (RDF): Concepts and Abstract Syntax</span><span class="delete">. 2004, W3C Recommendation. URL: </span><span class="delete">http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/</span></a>
-</dd></dl></div></div></body></html>
-
+</dd><span class="delete">[PROV-DM]</span><dt id="bib-PROV-O"><span class="insert">[PROV-O]</span></dt><dd><span class="delete">Luc Moreau and Paolo Missier</span><span class="insert">Timothy Lebo, Satya Sahoo and Deborah McGuinness</span> (eds.) Khalid Belhajjame, <span class="delete">Reza B'Far, </span>James Cheney, <span class="delete">Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes </span><span class="insert">David Corsar, Daniel Garijo, Stian Soiland-Reyes, and Stephan Zednik </span><a href="http://www.w3.org/TR/prov-o/"><cite><span class="delete">PROV-DM: The PROV Data</span><span class="insert">Provenance Formal</span> Model</cite></a>. <span class="delete">2012,</span><span class="insert">2011,</span> Working Draft. URL: <span class="delete">http://www.w3.org/TR/prov-dm/</span><a href="http://www.w3.org/TR/prov-o/"><span class="insert">http://www.w3.org/TR/prov-o/</span></a>
+</dd><dt id="bib-PROV-SEM">[PROV-SEM]</dt><dd>James Cheney <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman"><cite>Formal Semantics Strawman</cite></a>. 2011, Work in progress. URL: <a href="http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman">http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman</a>
+</dd><span class="delete">[RDF]</span><span class="delete">Graham Klyne and Jeremy J. Carroll (eds.) </span><span class="delete">Resource Description Framework (RDF): Concepts and Abstract Syntax</span><span class="delete">. 2004, W3C Recommendation. URL: </span><span class="delete">http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/</span>
+</dl></div></div></body></html>
+