--- a/model/prov-constraints.html Tue Jul 10 14:40:04 2012 +0100
+++ b/model/prov-constraints.html Mon Jul 16 20:09:12 2012 +0100
@@ -42,6 +42,28 @@
//console.log( "rule for " + myid + " " + mycount);
});
+
+ $('.constraint-example,.definition-example,.inference-example').each(function(index) {
+
+ var myid=$(this).attr('id');
+ var mycount='NNN';
+
+ if (myid==undefined) {
+ myid='rule_' + mycount;
+ $(this).attr('id',myid);
+ }
+
+ var myClass=$(this).attr('class');
+
+ var myTitle=capitaliseFirstLetter(myClass) + ' ' + mycount + ' (' + myid + ')';
+
+ $(this).attr('data-count', mycount)
+ .attr('data-title',myTitle).prepend($('<div>').addClass('ruleTitle')
+ .append($('<a>').addClass('internalDFN').attr('href','#'+myid).append(myTitle)));
+
+ //console.log( "rule for " + myid + " " + mycount);
+
+ });
}
function capitaliseFirstLetter(string)
@@ -134,10 +156,15 @@
};
var extraReferences = {
+ "CHR":
+ "AUTHOR "+
+ "<a href=\"???\"><cite>TITLE</cite></a>."+
+ " PUBLISHER "+
+ " URL: <a href=\"???\">URL</a>",
"CLOCK":
"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. "+
+ " 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.",
"CSP":
@@ -145,7 +172,12 @@
"<a href=\"http://www.usingcsp.com/cspbook.pdf\"><cite>Communicating Sequential Processes</cite></a>."+
"Prentice-Hall. 1985"+
"URL: <a href=\"http://www.usingcsp.com/cspbook.pdf\">http://www.usingcsp.com/cspbook.pdf</a>",
- "Logic":
+ "DBCONSTRAINTS":
+ " AUTHOR "+
+ " <a href=\"???\"><cite>TITLE</cite></a>."+
+ " PUBLISHER"+
+ " URL: <a href=\"???\">URL</a>",
+ "Logic":
"W. E. Johnson"+
"<a href=\"http://www.ditext.com/johnson/intro-3.html\"><cite>Logic: Part III</cite></a>."+
"1924. "+
@@ -288,12 +320,15 @@
<p> This document introduces <i>inferences</i> and <i>definitions</i>
- that are allowed on provenance statements and <i>validity
- constraints</i> that PROV instances should satisfy. These inferences
- and constraints are useful for readers who develop applications that
- generate provenance or reason over provenance. They can also be
- used to <i>normalize</i> PROV instances to a form that can easily be
- compared.</p> </section>
+ that are allowed on provenance statements and <i>constraints</i>
+ that PROV instances MUST satisfy in order to be considered
+ <i>valid</i>. These inferences and constraints are useful for
+ readers who develop applications that generate provenance or reason
+ over provenance. They can also be used to <i>normalize</i> PROV
+ instances to forms that can easily be compared in order to determine
+ whether two PROV instances are equivalent.</p>
+
+</section>
<section id="sotd">
<h4>PROV Family of Specifications</h4>
@@ -319,15 +354,10 @@
should focus on PROV-DM and PROV-CONSTRAINTS. PROV-O, PROV-N, PROV-XML offer examples of mapping to RDF, text, and XML, respectively.</li>
</ul>
-<h4>First Public Working Draft</h4>
-<div class='note'> Revise for 2PWD</div>
-
- <p>This is the first public release of the PROV-CONSTRAINTS
-document. Following feedback, the Working Group has decided to
-reorganize the PROV-DM document substantially, separating the data model,
-from its constraints, and the notation used to illustrate it. The
-PROV-CONSTRAINTS release is synchronized with the release of the PROV-DM, PROV-O,
-PROV-PRIMER, and PROV-N documents.
+<h4>Second Public Working Draft</h4>
+<div class='note'>Revise</div>
+ <p>This is a draft of the second public release of the PROV-CONSTRAINTS
+document.
</p>
</section>
@@ -362,37 +392,23 @@
<h3>Purpose of this document</h3>
-<p> PROV-DM is a conceptual data model for provenance, which is realizable
-using different serializations such as PROV-N, PROV-O, or PROV-XML.
-The PROV-DM specification [[PROV-DM]] does not impose any requirements
-upon sets of PROV
-statements (or <a>instances</a>) to be valid, that is, to correspond to a consistent
-history of objects and interactions to which logical reasoning can be safely applied. </p>
+<p> PROV-DM is a conceptual data model for provenance, which is
+realizable using different serializations such as PROV-N, PROV-O, or
+PROV-XML. The PROV-DM specification [[PROV-DM]] imposes few
+requirements upon sets of PROV statements (or <a>instances</a>). By
+default, PROV instances need not be valid, that is, they may not
+correspond to a consistent history of objects and interactions to
+which logical reasoning can be safely applied. </p>
-<p> This document specifies <em>inferences</em> over PROV instances that
-applications MAY employ, including definitions of some provenance
-statements in terms of others, and also defines a class of <em>valid</em>
-PROV instances by specifying <em>constraints</em> that valid PROV instances must
-satisfy. Applications SHOULD produce valid provenance and
-MAY reject provenance that is not <em>valid</em>. <a href="#compliance"
-class="sectionRef"></a>
-summarizes the requirements for compliance with this document, which
-are specified in detail in the rest of the document.
-</p>
-
-<p> This specification lists inferences and definitions together in
-one section (<a href="#inferences" class="sectionRef"></a>), and introduces two kinds of
-constraints (<a href="#constraints" class="sectionRef"></a>):
-<em>uniqueness constraints</em> that prescribe properties of PROV
-instances that can be checked directly by inspecting the syntax, and
-<em>event ordering</em> constraints that require that the records in a
-PROV <a>instance</a> are consistent with a sensible ordering of events
-relating the activities, entities and agents involved. Next,
-notions of <a>validity</a>, <a>equivalence</a> and <a>normalization</a> are defined (<a href="#equivalence"
-class="sectionRef"></a>).
-In <a
- href="#bundle-constraints" class="sectionRef"></a> we
-discuss how constraints interact with bundles. </p>
+<p> This document specifies <em>inferences</em> over PROV instances
+that applications MAY employ, including <em>definitions</em> of some
+provenance statements in terms of others, and also defines a class of
+<em>valid</em> PROV instances by specifying <em>constraints</em> that
+valid PROV instances must satisfy. Applications SHOULD produce valid
+provenance and MAY reject provenance that is not valid. Applications
+SHOULD also use definitions, inferences and constraints to normalize
+PROV instances in order to determine whether two such instances convey
+the same information.
<p>To summarize: compliant applications use definitions,
@@ -405,6 +421,43 @@
of the semantics of PROV statements, which justifies the inferences
and constraints, can be found in the formal semantics [[PROV-SEM]].
</p>
+
+<section>
+<h4>Structure of this document</h4>
+
+<p><a href="#rationale">Section 2</a> gives a brief rationale
+for the definitions, inferences and constraints.
+</p>
+<p>
+<a
+ href="#compliance">Section 3</a> summarizes the
+requirements for compliance with this document, which are specified in
+detail in the rest of the document. </p>
+
+<p> <a href="#inferences">Section 4</a> presents inferences and
+definitions. Definitions allow replacing shorthand notation in PROV-N
+with more explicit and complete statements; inferences allow adding
+new facts representing implicit knowledge about the structure of
+provenance. </p>
+
+<p><a href="#constraints">Section 5</a> presents two kinds of constraints,
+<em>uniqueness</em> constraints that prescribe properties of PROV
+instances that can be checked directly by inspecting the syntax, and
+<em>event ordering</em> constraints that require that the records in a
+PROV <a>instance</a> are consistent with a sensible ordering of events
+relating the activities, entities and agents involved.
+</p>
+
+<p><a href="#equivalence">Section 6</a> defines the notions of
+of <a>validity</a>, <a>equivalence</a> and <a>normalization</a>.
+</p>
+
+<p><a href="#bundle-constraints">Section 7</a> discusses how the
+preceding concepts are applied in a PROV instance with multiple
+bundles. </p>
+
+</section>
+
</section>
<section id="audience">
<h3> Audience </h3>
@@ -413,34 +466,40 @@
and users who wish to create, process, share or integrate provenance
records on the (Semantic) Web. Not all PROV-compliant applications
need to perform inferences or check validity when processing provenance.
-However, applications that create or transform provenance should
+However, applications that create or transform provenance SHOULD
attempt to produce valid provenance, to make it more useful to other
applications by ruling out nonsensical or inconsistent information.
</p>
-<p>This document assumes familiarity with [[PROV-DM]].
+<p>This document assumes familiarity with [[PROV-DM]] and employs the
+[[PROV-N]] notation.
</p>
+
+</section>
+</section>
+
<section id='rationale' class="informative">
<h3>Rationale</h3>
-<div class="note"> The following motivating discussion copied from
- sec. 8 in a prior version; not sure where it fits best.</div>
-
<p> In this section we give a high-level rationale that provides some
further background for the constraints. </p>
-
+
+<section>
+<h4>Entities, Activities and Agents</h4>
<p>
-From a provenance viewpoint, it is important to identify
-a partial state of something, i.e. something with some aspects that
-have been fixed, so that it becomes possible to express its provenance
-(i.e. what caused the thing with these specific aspects).
+One of the central challenges in representing provenance information
+is how to deal with change. Real-world objects, information objects
+and Web resources change over time, and the characteristics that make
+them identifiable in a given situation are sometimes subject to change
+as well. To avoid over-reliance on assumptions that identifying
+characteristics do not change, PROV allows for things to be described
+in different ways, with different descriptions of their partial
+state.
</p>
<p>
An <dfn>entity</dfn> is a thing one wants to provide provenance for
and whose situation in the world is described by some fixed
-attributes. An entity has a <dfn
-id="dfn-characterization-interval">characterization interval</dfn>,
-or <dfn id="lifetime">lifetime</dfn>,
+attributes. An entity has a <dfn id="lifetime">lifetime</dfn>,
defined as the period
between its <a title="entity generation event">generation event</a>
and its <a title="entity invalidation event">invalidation event</a>.
@@ -470,28 +529,28 @@
different entities.
</p>
-Further considerations:
-<ul>
-<li>In order to describe the provenance of something during an interval over which
- relevant attributes of the thing are not fixed, it is required to
- create multiple entities, each with its own identifier, <a
- title="characterization interval">characterization interval</a>, and
- fixed attributes, and express
- dependencies between the various entities using events.
- For example, if we want to describe the provenance of several
- versions of a document, involving attributes such as authorship that
- change over time, we need different entities for the versions linked
- by appropriate generation, usage, revision, and invalidation events.
-</li>
+<p>
+In order to describe the provenance of something during an interval
+ over which relevant attributes of the thing are not fixed, a PROV
+ instance would describe multiple entities, each with its own
+ identifier, <a>lifetime</a>, and fixed attributes, and express dependencies between
+ the various entities using events. For example, if we want to
+ describe the provenance of several versions of a document, involving
+ attributes such as authorship that change over time, we need
+ different entities for the versions linked by appropriate
+ generation, usage, revision, and invalidation events.
+</p>
-<li>There is no assumption that the set of attributes is complete, nor
-that the attributes are independent or orthogonal of each other.</li>
-<li>There is no assumption that the attributes of an entity uniquely
-identify it. Two different entities that present the same aspects of
-possibly different things can have the same attributes; this leads to
-ambiguity, which is mitigated through the use of identifiers.</li> </ul>
+<p>There is no assumption that the set of attributes listed in an
+<span class="name">entity</span> statement is complete, nor
+that the attributes are independent or orthogonal of each
+other. Similarly, there is no assumption that the attributes of an
+entity uniquely identify it. Two different entities that present the
+same aspects of possibly different things can have the same
+attributes; this leads to ambiguity, which is mitigated through the
+use of identifiers.</p>
-<p>An activity is delimited by its <a title="activity start event">start</a> and its <a title="activity end event">end</a> events; hence, it occurs over
+<p>An <a>activity</a> is delimited by its <a title="activity start event">start</a> and its <a title="activity end event">end</a> events; hence, it occurs over
an interval delimited by two <a title="instantaneous event">instantaneous
events</a>. However, an activity record 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">start</a> event and its <a title="activity end event">end</a> event.
@@ -499,37 +558,37 @@
-<p>Further considerations:</p>
-<ul>
-<li>An activity is not an entity.
-Indeed, an entity exists in full at
-any point in its lifetime, persists during this
-interval, and preserves the characteristics that makes it
-identifiable. 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 distinction is similar to the distinction between
-'continuant' and 'occurrent' in logic [[Logic]].</li>
-</ul>
-
-<p> Although time is critical, we should also recognize that
-provenance can be used 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 records
-are combined by different systems, we may not be able to align the
-times involved to a single global timeline. Hence, PROV-DM is
-designed to minimize assumptions about time. </p>
+<p>An activity is not necessarily an entity. Indeed, an entity exists in full at
+any point in its lifetime, persists during this interval, and
+preserves the characteristics that makes it identifiable. 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
+distinction is similar to the distinction between 'continuant' and
+'occurrent' in logic [[Logic]].</p>
-<h4>Types of Events</h4>
-<p>Five kinds of <a title="instantaneous event">instantaneous events</a> are used
-for the PROV-DM data model. The <strong>activity start</strong> and
-<strong>activity end</strong> events delimit the beginning and the end
-of activities, respectively. The <strong>entity usage</strong>,
+</section>
+<section>
+<h4>Events</h4>
+
+<p> Although time is important for provenance, provenance can be used
+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 records are combined by
+different systems, we 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>
+
+<p>Five kinds of <a title="instantaneous event">instantaneous
+events</a> are used in PROV-DM. The <strong>activity start</strong>
+and <strong>activity end</strong> events delimit the beginning and the
+end of activities, respectively. The <strong>entity usage</strong>,
<strong>entity generation</strong>, and <strong>entity
invalidation</strong> events apply to entities, and the generation and
-invalidation events delimit the <a title="characterization interval">characterization interval</a> of
-an entity. More specifically:
+invalidation events delimit the <a>lifetime</a> of an entity. More
+specifically:
</p>
@@ -554,46 +613,41 @@
</section>
</section>
-</section>
-
<section id="compliance">
<h2>Compliance with this document</h2>
-<div class="note">
-TODO: Add collection and account constraint sections to the compliance
- list as appropriate.
- </div>
+<p>
For the purpose of compliance, the normative sections of this document
are <a href="#compliance"
class="sectionRef"></a>, <a href="#inferences"
+class="sectionRef"></a>, <a href="#constraints"
class="sectionRef"></a>, <a href="#equivalence"
-class="sectionRef"></a>, and <a href="#constraints"
-class="sectionRef"></a>.
+class="sectionRef"></a>, and <a
+ href="#bundle-constraints" class="sectionRef"></a>.
To be compliant:
<ol><li>When processing provenance, an
application MAY apply the inferences and definitions in <a
href="#inferences" class='sectionRef'></a>.</li>
- <li>When determining whether two PROV instances are
- <a>equivalent</a>, an application MUST determine whether their
- normal forms are equal, as specified in <a href="#equivalence" class="sectionRef"></a>.
- <li>When determining whether a PROV instance is <a>valid</a>, an
+ <li>When determining whether a PROV instance is <a>valid</a>, an
application MUST check that all of the
constraints of <a href="#constraints" class="sectionRef"></a> are
satisfied on the <a>normal form</a> of the instance.</li>
- <li> When producing provenance meant for other applications to
- use, the application SHOULD produce <a>valid</a> provenance. </li>
+ <li> When producing provenance meant for other applications to
+ use, the application SHOULD produce <a>valid</a> provenance, as specified in <a href="#equivalence" class="sectionRef"></a>. </li>
+ <li>When determining whether two PROV instances are
+ <a>equivalent</a>, an application MUST determine whether their
+ normal forms are equal, as specified in <a href="#equivalence" class="sectionRef"></a>.
+ <li>For PROV instances containing multiple <a>bundle</a>s, the
+inferences, definitions, constraints and inferences
+SHOULD be applied to each bundle independently, for the purpose of
+ checking validity or equivalence, as specified in <a
+ href="#bundle-constraints" class="sectionRef"></a>. </li>
</ol>
- <div class="note">
- Should we specify a way for PROV instances to say whether they
- are meant to be validated or not? Seems outside the scope of this
- document, may require changes to PROV-N. Proposal: Point out that
- this can be done already by describing bundles; more details in
- best practices.
- </div>
+</p>
+
+ <p>
-<p>
-
-<div class="note">Table: work in progress. Done up to constraint 25.</div>
+<div class="note">Table: work in progress; do after constraints are done.</div>
<div id="prov-dm-constraints-fig" style="text-align: left;">
<table class="thinborder" style="margin-left: auto; margin-right: auto;">
@@ -640,10 +694,7 @@
<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
<tr class="component6-color"><td class="provType"><a>Collection</a></td><td> </td><td rowspan="6"><a href="#component6">Component 6: Collections</a></td></tr>
-<tr class="component6-color"><td class="provType"><a>Dictionary</a></td><td> </td></tr>
<tr class="component6-color"><td class="provType"><a title="empty dictionary">EmptyDictionary</a></td><td> </a></td></tr>
-<tr class="component6-color"><td><a>Insertion</a></td><td> </td></tr>
-<tr class="component6-color"><td><a>Removal</a></td><td> </td></tr>
<tr class="component6-color"><td><a>Membership</a></td><td> </td></tr>
</table>
</div>
@@ -669,7 +720,7 @@
</p>
<p> Inferences have the following general form:</p>
-<div class='inference' id='inference-example'>
+<div class='inference-example' id='inference-example'>
<p>
<span class='conditional'>IF</span> <span class="name">hyp_1</span> and ... and
<span class="name">hyp_k</span> <span class='conditional'>THEN</span>
@@ -686,14 +737,10 @@
identifiers might later be found to be equal to known identifiers;
they play a similar role in PROV constraints to existential variables in logic.
</p>
-<div class='note'>
- TODO: Make sure conjunctive reading of conclusion is clear. Discuss
- connection to TGDs.
- </div>
<p> Definitions have the following general form:</p>
-<div class='definition' id='definition-example'>
+<div class='definition-example' id='definition-example'>
<p>
<span class="name">defined_exp</span> holds <span class='conditional'>IF AND ONLY IF </span>
there exists <span class="name">a_1</span>,..., <span
@@ -713,27 +760,85 @@
its definition.
</p>
+<p> Definitions and inferences can be viewed as logical formulas;
+ similar formalisms are often used in rule-based reasoning [[CHR]]
+ and in databases [[DBCONSTRAINTS]]. In particular, the identifiers
+ <span class="name">a_1</span> ... <span class="name">a_n</span>
+ should be viewed as existentially quantified variables, meaning that
+ through subsequent reasoning steps they may turn out to be equal to
+ other identifiers that are already known, or to other existentially
+ 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.
+ </p>
+
+<section>
+ <h4>Optional Identifiers and Attributes</h4>
+
+ <p>Many PROV relation statements have an identifier,
+ identifting a link between two or more related objects. This
+ identifier is optional and can be omitted in [[PROV-N]] notation.
+ For the purpose of inference and validity checking, it is convenient
+ to generate dummy identifiers (i.e. existentially quantified
+ variables) denoting the missing identifiers.
+ </p>
+ <div class="definition" id="optional-identifiers">
+ <p>
+ <span class="name">r(a_1,...,a_n) </span> holds <span class="conditional">IF AND ONLY IF</span>
+ there exists <span class="name">id</span> such that <span class="name">r(id;a_1,...,a_n)</span> holds.</p>
+ </div>
+
+ <p>Likewise, many PROV expressions allow for an optional attribute
+ list. If it is omitted, this is the same as specifying an empty
+ attribute list:</p>
+ <div class="definition" id="optional-attributes">
+ <p>
+ <span class="name">r(a_1,...,a_n)</span> holds and does not contain an explicit attribute
+ list <span class="conditional">IF AND ONLY IF</span> <span
+ class="name">r(a_1,...,a_n,[])</span> holds.</p>
+ <p>
+ Similarly, <span class="name">r(id;a_1,...,a_n)</span> holds and does not contain an explicit attribute
+ list <span class="conditional">IF AND ONLY IF</span> <span class="name">r(id;a_1,...,a_n,[])</span> holds.</p>
+ </div>
+
+ <p>We assume from now on that all optional identifiers have been
+ filled in and all explicit attributes have been removed, generating
+ <span class='name'>attribute</span> statements. Finally, many PROV
+ expressions have other optional arguments or short forms that can be
+ used if none of the optional arguments is present. These are
+ handled by specific rules listed below. </p> </section>
+
<section>
<h3>Component 1: Entities and Activities</h3>
+
+
-<p>Communication between activities is <a title="definition">defined</a> in terms
-as the existence of an underlying entity generated by one activity and used by the
-other.</p>
+<p>Communication between activities is <a
+ title="definition">defined</a> as the existence of an underlying
+entity generated by one activity and used by the other.</p>
- <div class="note">Explicitly list existentially quantified vars in constraints</div>
+ <div class="note">Where do the attributes of the wasInformedBy
+ relation go? The definition is essentially saying they don't
+ matter. If this is what we mean, then the id and attributes are
+ irrelevant to the meaning/validity.</div>
<div class='definition' id='wasInformedBy-definition'>
<p>
Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
-<span class="name">wasInformedBy(-;a2,a1)</span>
+<span class="name">wasInformedBy(_id;a2,a1,_attrs)</span>
holds <span class='conditional'>IF AND ONLY IF</span>
- there is an entity with some identifier <span class="name">e</span>,
-such that <span class="name">wasGeneratedBy(-;e,a1,-,)</span> and <span class="name">used(-;a2,e,-)</span> hold.</p>
+ there exists <span class="name">e</span>, <span class="name">_id1</span>, <span class="name">_t1</span>, <span class="name">_attrs1</span>, <span class="name">_id2</span>, <span class="name">_t2</span>, <span class="name">_attrs2</span>,
+such that <span class="name">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span> and <span class="name">used(_id2;a2,e,_t2,_attrs2)</span> hold.</p>
</div>
+<div class="note"> We don't give counterexamples to other
+ non-inferences. Suggest dropping this one.</div>
+
<p>The relationship <span class="name">wasInformedBy</span> is not
<a>transitive</a>. Indeed, consider the following statements.</p>
<pre class="codeexample">
@@ -770,15 +875,11 @@
<span class='conditional'>IF</span> <span
class="name">activity(a,t1,t2,_attrs)</span> <span
class="conditional">THEN</span> <span
- class="name">wasStartedBy(-;a,-,-,t1)</span> and <span class="name">wasEndedBy(-;a,-,-,t2)</span>.
+ class="name">wasStartedBy(_id1;a,_e1,t1,_attrs1)</span> and <span class="name">wasEndedBy(_id2;a,_e2,t2,_attrs2)</span>.
</div>
-<hr>
-<div class="note"> James: The following definitions seem circular;
- prune?
-<br>
-Luc: there was something wrong. I have replaced the definitions by inferences.</div>
+<hr />
<p id='wasStartedBy-inference_text'>Start of <span class="name">a</span> by trigger <span class="name">e1</span> and starter activity <span
@@ -788,9 +889,9 @@
<div class='inference' id='wasStartedBy-inference'>
<p><span class='conditional'>IF</span>
- <span class="name">wasStartedBy(_id;a,e1,a1,_t1,_attrs1)</span>,
+ <span class="name">wasStartedBy(_id;a,e1,a1,_t,_attrs)</span>,
<span class='conditional'>THEN</span>
- <span class="name">wasGeneratedBy(-;e1,a1,-,-)</span>.</p>
+ <span class="name">wasGeneratedBy(_gen;e1,a1,_t1,_attrs1)</span>.</p>
</div>
<p>
@@ -805,9 +906,9 @@
<div class='inference' id='wasEndedBy-inference'>
<p><span class='conditional'>IF</span>
- <span class="name">wasEndedBy(_id;a,e1,a1,_t1,_attrs1)</span>,
+ <span class="name">wasEndedBy(_id;a,e1,a1,_t,_attrs)</span>,
<span class='conditional'>THEN</span>
- <span class="name">wasGeneratedBy(-;e1,a1,-,-)</span>.</p>
+ <span class="name">wasGeneratedBy(_gen;e1,a1,_t1,_attrs1)</span>.</p>
</div>
@@ -827,37 +928,49 @@
<div class='inference' id='derivation-generation-use'>
<p>
<ol>
-<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(_id;e2,e1,a,id2,_id1,_attrs)</span>, <span class='conditional'>THEN</span> <span class="name">wasGeneratedBy(id2;e2,a,-)</span>
-<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(_id;e2,e1,a,_id2,id1,_attrs)</span>, <span class='conditional'>THEN</span> <span class="name">used(id1;a,e1,-)</span>
+<li><span class='conditional'>IF</span> <span
+ class="name">wasDerivedFrom(_id;e2,e1,a,id2,_id1,_attrs)</span>,
+ <span class='conditional'>THEN</span> there exist <span
+ class="name">_t2</span> and <span class="name">_attrs2</span>
+ such that <span class="name">wasGeneratedBy(id2;e2,a,_t2,_attrs2)</span>
+<li><span class='conditional'>IF</span> <span
+ class="name">wasDerivedFrom(_id;e2,e1,a,_id2,id1,_attrs)</span>,
+ <span class='conditional'>THEN</span> there exist <span
+ class="name">_t1</span> and <span class="name">_attrs1</span>
+ such that <span class="name">used(id1;a,e1,_t1,_attrs1)</span>
</ol>
</div>
<p>
<hr>
-<p id='derivation-use_text'>Derivations with an explicit activity and no usage admit the following inference: </p>
+<p id='derivation-use_text'>Derivations with an explicit activity and
+no specified generation and usage admit the following inference: </p>
<div class="note">
Luc: Here we really mean, no usage, no generation specified. What notation do we use?
</div>
<div class='inference' id='derivation-use'>
<p>
-<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(_id;e2,e1,a, -, -,_attrs)</span> and <span class="name">wasGeneratedBy(_id2;e2,a,_t2,_attrs2)</span> hold, <span
-class='conditional'>THEN</span> <span class="name">used(-;a,e1,-)</span> also holds.
+<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(_id;e2,e1,a,gen,use,_attrs)</span> and <span class="name">wasGeneratedBy(gen;e2,a,_t2,_attrs2)</span> hold, <span
+class='conditional'>THEN</span> there exist <span
+ class="name">_t1</span> and <span class="name">_attrs1</span> such
+ that <span class="name">used(use;a,e1,_t1,_attrs1)</span> also holds.
</div>
-<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity in a given account
+<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity
(see <a class="rule-text" href="#unique-generation"><span>TBD</span></a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
</p>
-<p>The converse inference does not hold.
-From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(a,e1,-)</span>, one cannot
-derive <span class="name">wasGeneratedBy(e2,a,-)</span> because
- identifier <span class="name">e1</span> may be used by many
- activities, whereas at most one activity could generate the entity
- <span class="name">e2</span>. Even if <span
-class="name">e2</span> is used by some activity that later generates <span class="name">e1</span>
-is generated, it is not safe to assume that <span
-class="name">e2</span> was derived from <span class="name">e1</span>.
-Derivation is not defined to be transitive either, following similar
- reasoning as for <span class="name">wasInformedBy</span>. </p>
+<p>The converse inference does not hold. Informally, from <span
+class="name">wasDerivedFrom(e2,e1)</span> and <span
+class="name">used(a,e1,-)</span>, one cannot derive <span
+class="name">wasGeneratedBy(e2,a,-)</span> because identifier <span
+class="name">e1</span> may be used by many activities, whereas at most
+one activity could generate the entity <span class="name">e2</span>.
+Even if <span class="name">e2</span> is used by some activity that
+later generates <span class="name">e1</span> is generated, it is not
+safe to assume that <span class="name">e2</span> was derived from
+<span class="name">e1</span>. Derivation is not defined to be
+transitive either, following similar reasoning as for <span
+class="name">wasInformedBy</span>. </p>
@@ -866,12 +979,16 @@
linked by a revision are also alternates.</p>
<div class='inference' id='revision-is-alternate'>
-Given two identifiers <span class="name">e1</span> and <span class="name">e2</span> identifying two entities,
-<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(-,e2,e1,[prov:type='prov:Revision'])</span> holds, <span class='conditional'>THEN</span> the following
-holds:
-<pre>
-alternateOf(e2,e1)
-</pre>
+<p><span class='conditional'>IF</span> <span
+ class="name">wasDerivedFrom(_id;e2,e1,[prov:type='prov:Revision'])</span>
+ holds, <span class='conditional'>THEN</span> <span
+ class="name">alternateOf(e2,e1)</span> holds.
+</p>
+<p><span class='conditional'>IF</span> <span
+ class="name">wasDerivedFrom(_id;e2,e1,_act,_gen,_use,[prov:type='prov:Revision'])</span>
+ holds, <span class='conditional'>THEN</span> <span
+ class="name">alternateOf(e2,e1)</span> holds.
+</p>
</div>
@@ -920,73 +1037,55 @@
<div class='inference' id='inference-attribution'>
<p>
<span class='conditional'>IF</span>
-<span class="name">wasAttributedTo(-;e,ag)</span> holds for some identifiers
+<span class="name">wasAttributedTo(_att;e,ag,_attrs)</span> holds for some identifiers
<span class="name">e</span> and <span class="name">ag</span>,
-<span class='conditional'>THEN</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
+<span class='conditional'>THEN</span> there exist
+ <span class="name">a</span>,
+ <span class="name">_t</span>,
+ <span class="name">_t1</span>,
+ <span class="name">_t2</span>,
+ <span class="name">_gen</span>,
+<span class="name">_assoc</span>,
+ <span class="name">_pl</span>,
+ <span class="name">_attrs1</span>,
+ <span class="name">_attrs2</span>,
+ <span class="name">_attrs3</span>,
+ such that the following statements hold:
<pre>
-activity(a,-,-)
-wasGeneratedBy(-;e,a,-)
-wasAssociatedWith(-;a,ag,-)
+activity(a,_t1,_t2,_attrs1)
+wasGeneratedBy(_gen;e,a,_t,_attrs2)
+wasAssociatedWith(_assoc;a,ag,_pl,_attrs3)
</pre>
</p>
</div>
-
-<p> Delegation relates agents where one agent acts on behalf of
+<hr />
+<p id='inference-delegation_text'> Delegation relates agents where one agent acts on behalf of
another, in the context of some activity. The supervising agent
delegates some responsibility for part of the activity to the
subordinate agent, while retaining some responsibility for the overall
activity. </p>
-
-
<div class="note">
- @@TODO: Could this be an inference? Does it imply that
- a1 is associated with all activities a2 is associated with?
+ @@TODO: Do we want both of these inferences?
</div>
-<!-- DELETE
- <hr>
-
-<p id='inference-trace_text'>A trace allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
-
-<p>A trace can be inferred from existing statements, or can be asserted stating that a dependency path exists without its individual steps being expressed. This is captured
-by the following inferences:
-
-<div class='inference' id='inference-trace'>
+<div class='inference' id='inference-delegation'>
<p>
-Given two identifiers <span class="name">e2</span> and <span class="name">e1</span> for entities,
-the following statements hold:</p>
-<ol>
-<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
-class="name">u1</span>, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
-<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also
-holds.</li>
-<li><span class='conditional'>IF</span> <span
-class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span
-class='conditional'>THEN</span> <span
-class="name">tracedTo(e2,ag1)</span> also holds.
-</li>
-<li>
-<span class='conditional'>IF</span> <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(-;e2,a,-,gAttr)</span>, and <span
-class="name">actedOnBehalfOf(ag2,ag1,a,rAttr)</span> hold, for some <span class="name">a</span>, <span class="name">ag2</span>, <span class="name">ag1</span>, <span class="name">aAttr</span>, <span class="name">gAttr</span>, and <span class="name">rAttr</span>, <span
-class='conditional'>THEN</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-
-<li><span class='conditional'>IF</span> <span
-class="name">wasGeneratedBy(e2,a,gAttr)</span> and <span
-class="name">wasStartedBy(a,e1,sAttr)</span> hold, for some <span
-class="name">a</span>, <span class="name">gAttr</span> , <span
-class="name">sAttr</span> then <span
-class="name">tracedTo(e2,e1)</span> holds.</li>
-<li><span class='conditional'>IF</span> <span class="name">tracedTo(e2,e)</span> and <span class="name">tracedTo(e,e1)</span> hold for some <span class="name">e</span>, <span
-class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
-</ol>
+<span class='conditional'>IF</span>
+<span class="name">wasAssociatedWith(_id1;a, ag1, _pl1, _attrs1)</span>
+ and <span class="name">actedOnBehalfOf(_id;ag1, ag2, a, _attrs)</span>,
+<span class='conditional'>THEN</span> there exist <span
+ class="name">_id2</span>, <span class="name">_pl2</span>, and <span class="name">_attrs2</span> such that <span class="name">wasAssociatedWith(_id2;a, ag2, _pl2, _attrs2)</span>.
+</p>
+<p>
+<span class='conditional'>IF</span>
+<span class="name">wasAssociatedWith(_id2;a, ag1, _pl2, _attrs2)</span>
+ and <span class="name">actedOnBehalfOf(_id;ag1, ag2, a, _attrs)</span>,
+<span class='conditional'>THEN</span> there exist <span
+ class="name">_id1</span>, <span class="name">_pl1</span>, and <span class="name">_attrs1</span> such that <span class="name">wasAssociatedWith(_id1;a, ag1, _pl1, _attrs1)</span>.
+</p>
</div>
-<p>We note that <a class="rule-text"
-href="#inference-trace"><span>TBD</span></a> does not
-allow us to infer anything about the attributes of the related
-entities, agents or events.
-</p>
--->
+
</section>
@@ -1023,8 +1122,8 @@
<hr>
-<p id="specialization-irreflexive_text">Similarly, specialization is a <a>strict</a> partial order: it is <a>irreflexive</a>,
- <a>antisymmetric</a> and
+<p id="specialization-irreflexive_text">Similarly, specialization is a
+ <a>strict partial order</a>: it is <a>irreflexive</a> and
<a>transitive</a>.</p>
<div class='inference' id="specialization-irreflexive">
@@ -1072,10 +1171,18 @@
</div>
- <div class="note">TODO: Possible inferences about attributes,
- generation, invalidation?
+ <div class="note">Confirm inferences about attributes,
+ generation, invalidation? See below. What about shared attributes
+ of overlapping entities?
</div>
+<div class="inference" id="specialization-attributes">
+ <p>
+ For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>entity(e1, [a=x])</span> holds for some
+ attribute <span class='name'>a</span> with value <span class='name'>x </span> and <span class='name'>specializationOf(e2,e1)</span> holds <span class='conditional'>THEN </span>
+ <span class='name'>entity(e2, [a=x])</span> also holds.</p>
+ </div>
+
</section>
@@ -1137,7 +1244,7 @@
constraint template(s)
</div>
- <section id="structural-constraints">
+ <section id="uniqueness-constraints">
<h3>Uniqueness Constraints</h3>
<div class="note"> More explanation about constraints. Non-examples
@@ -1342,15 +1449,20 @@
<p>Specifically, <dfn id="dfn-precedes">precedes</dfn> is a partial
order between <a title="instantaneous event">instantaneous events</a>. When we say
<span class="name">e1</span> precedes <span class="name">e2</span>,
-this means that either the two events are equal or <span
-class="name">e1</span> happened before <span class="name">e2</span>.
+this 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">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 after <span
-class="name">e2</span>. Both relations are <a>strict</a> partial orders, meaning
-that they are <a>irreflexive</a>, <a>transitive</a>, and <a>antisymmetric</a>.</p>
+class="name">e1</span> happened at the same time as or after <span
+class="name">e2</span>. Both relations are <a>preorder</a>s, meaning
+that they are <a>reflexive</a> and <a>transitive</a>. Moreover, we
+consider strict 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 <a>transitive</a> relation. </p>
<p>PROV-DM also allows for time observations to be inserted in
@@ -1794,6 +1906,25 @@
</figure>
</div>
+<hr />
+<p id="specialization-generation_text">
+If an entity specalizes another, then its generation must follow the
+specialized entity's generation.
+</p>
+<div class="constraint" id="specialization-generation">
+ <p>
+<span class="conditional">IF</span> <span class="name">specializationOf(e2,e1)</span> and <span class="name">wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span> THEN <span class="name">gen1</span> precedes-or-equals <span class="name">gen2</span>.
+<p/p>
+</div>
+<hr />
+<p id="specialization-generation_text">
+Similarly, if an entity specalizes another, then its invalidation must follow the
+specialized entity's invalidation.
+</p><div class="constraint" id="specialization-invalidation">
+ <p>
+IF <span class="name">specializationOf(e2,e1)</span> and <span class="name">wasInvalidatedBy(inv1;e1,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(inv2;e2,_a2,_t2,_attrs2)</span> THEN <span class="name">inv2</span> <a>precedes-or-equals</a> <span class="name">inv1</span>.
+</p>
+ </div>
</section>
@@ -2086,17 +2217,11 @@
<h2>Glossary</h2>
<ul>
<li> <dfn>antisymmetric</dfn>: A relation R over X is <a>antisymmetric</a> if
- for any elements x, y of X, if x R y and y R x then x = y.
- Alternatively, for a <a>strict</a> partial order anti-symmetry
- means that for any elements x, y of X, it is impossible that
- both x R
- y and y R x hold.</li>
+ for any elements x, y of X, if x R y and y R x then x = y.</li>
<li> <dfn>reflexive</dfn>: A relation R over X is <a>reflexive</a> if
for any element x of X, we have x R x.</li>
- <li><dfn>strict</dfn>: Partial orders are often defined in one
- of two standard forms: a weak form, like ≤, which is <a>reflexive</a>, and a <a>strict</a> form, like < that
- is <a>irreflexive</a>. The meanings of certain terms, such as
- <a>antisymmetric</a>, differe slightly depending on strictness.
+ <li><dfn>strict</dfn>: The strict form of a partial order or
+ preorder is the relation formed by excluding reflexive steps.
<li> <dfn>symmetric</dfn>: A relation R over X is <a>symmetric</a> if
for any elements x, y of X, if x R y then y R x.</li>
<li> <dfn>transitive</dfn>: A relation R over X is <a>transitive</a> if