--- a/model/prov-constraints.html Tue Feb 19 16:27:16 2013 +0100
+++ b/model/prov-constraints.html Tue Feb 19 15:30:34 2013 +0000
@@ -816,13 +816,13 @@
consistent history of objects and their interactions that is safe to
use for the purpose of logical reasoning and other kinds of analysis.
Valid PROV instances satisfy
-certain <a>definitions</a>, <a>inferences</a>, and
-<a>constraints</a>. These definitions, inferences, and constraints
+certain <a title="definition">definitions</a>, <a title="inference">inferences</a>, and
+<a title="constraint">constraints</a>. These definitions, inferences, and constraints
provide a measure of consistency checking for provenance and reasoning
over provenance. They can also be used to <a title="normal
form">normalize</a> PROV instances to forms that can easily be
compared in order to determine whether two PROV instances are
-<a>equivalent</a>. Validity and equivalence are also defined for PROV
+<a title="equivalence">equivalent</a>. Validity and equivalence are also defined for PROV
bundles (that is, named instances) and documents (that is, a toplevel
instance together with zero or more bundles).</p>
<p>The <a href="http://www.w3.org/TR/2012/WD-prov-overview-20130312/">PROV Document Overview</a> describes the overall state of PROV, and should be read before other PROV documents.</p>
@@ -899,9 +899,9 @@
<p>The PROV Data Model, PROV-DM, is a conceptual data model for provenance, which is
realizable using different representations such as PROV-N and PROV-O.
-A PROV <a>instance</a> is a set of PROV statements.
-A PROV <a>document</a> is an instance
-together with zero or more <a>bundles</a>, or named instances. For
+A <a>PROV instance</a> is a set of PROV statements.
+A <a>PROV document</a> is an instance
+together with zero or more <a title="bundle">bundles</a>, or named instances. For
example, a PROV document could be a .provn document, the result
of a query, a triple store containing PROV statements in RDF, etc.
The
@@ -990,9 +990,9 @@
<p><a href="#constraints">Section 6</a> presents four kinds of constraints,
<em>uniqueness</em> constraints that prescribe that certain statements
-must be unique within PROV <a>instances</a>,
+must be unique within <a title="PROV instance">PROV instances</a>,
<em>event ordering</em> constraints that require that the records in a
-PROV <a>instance</a> are consistent with a sensible ordering of events
+<a>PROV instance</a> are consistent with a sensible ordering of events
relating the activities, entities and agents involved,
<em>impossibility</em> constraints that forbid certain patterns of
statements in valid PROV instances, and <em>type</em> constraints that
@@ -1000,7 +1000,7 @@
</p>
<p><a href="#normalization-validity-equivalence">Section 7</a> defines the notions
-of <a>validity</a>, <a>equivalence</a> and <a>normalization</a>.
+of <a title="valid">validity</a>, <a>equivalence</a> and <a title="normal form">normalization</a>.
</p>
@@ -1097,7 +1097,7 @@
attributes; this leads to potential ambiguity, which is mitigated through the
use of identifiers.</p>
-<p>An <a>activity</a>'s lifetime is delimited by its <a title="activity start
+<p>An activity's lifetime is delimited by its <a title="activity start
event">start</a> and its <a title="activity end event">end</a>
events. It occurs over
an interval delimited by two <a title="instantaneous event">instantaneous
@@ -1485,7 +1485,7 @@
<p>
For the purpose of constraint checking, we view PROV statements
(possibly involving existential variables) as
- <dfn>formulas</dfn>. An instance is analogous to a "theory" in
+ <dfn id="formula">formulas</dfn>. An instance is analogous to a "theory" in
logic, that is, a set of formulas all thought to describe the same
situation. The set can also be thought of a single, large formula:
the conjunction of all of the atomic formulas.
@@ -2236,7 +2236,7 @@
<dfn>variables</dfn> denoting the unknown values.
Generally, identifiers occurring in constraints and inferences are
variables. Variables that are generated during inferences and
- appear inside an instance are often called <dfn>existential
+ appear inside an instance are often called <dfn title="existential variable">existential
variables</dfn>, because they are implicitly existentially quantified.
</p>
@@ -2291,7 +2291,7 @@
statements in <span class="math">I</span>.
</p>
- <p> <dfn>Unification</dfn> is an operation that can be applied
+ <p> <dfn id="unification">Unification</dfn> is an operation that can be applied
to a pair of terms.
The result of unification is either a <dfn>unifier</dfn>, that is, a substitution <span class="math">S</span> such that <span class="math">S(t)
= S(t')</span>, or failure, indicating
@@ -2347,8 +2347,7 @@
This section describes <a title="definition">definitions</a> and <a title="inference">inferences</a> that MAY be used on
provenance data, and that preserve <a>equivalence</a> on <a>valid</a>
PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef"></a>).
-A <dfn
- id="definition">definition</dfn> is a rule that can be applied to
+A <dfn>definition</dfn> is a rule that can be applied to
PROV instances to replace defined statements with other statements. An <dfn id="inference">inference</dfn> is a rule that can be applied
to PROV instances to add new PROV statements. A definition states that a
provenance statement is equivalent to some other statements, whereas
@@ -3462,7 +3461,7 @@
</li>
<li>If unification fails, then the constraint
is unsatisfiable, so application of the constraint to <span class="math">I</span>
- fails. If this failure occurs during <a>normalization</a> prior to
+ fails. If this failure occurs during <a title="normal form">normalization</a> prior to
validation, then <span class="math">I</span> is invalid, as explained in <a href="#normalization-validity-equivalence">Section 6</a>.
</li>
<li>If unification succeeds with a substitution <span class="math">S</span>, then
@@ -5032,9 +5031,9 @@
<p>Because of the potential interaction among definitions, inferences, and
constraints, the above algorithm is iterative. Nevertheless,
- all of our constraints fall into a class of <a>tuple-generating
- dependencies</a> and <a>equality-generating dependencies</a> that
- satisfy a termination condition called <a>weak acyclicity</a> that
+ all of our constraints fall into a class of <em>tuple-generating
+ dependencies</em> and <em>equality-generating dependencies</em> that
+ satisfy a termination condition called <em>weak acyclicity</em> that
has been studied in the context of relational databases
[[DBCONSTRAINTS]]. Therefore, the above algorithm terminates, independently
of the order in which inferences and constraints are applied.
@@ -5076,7 +5075,7 @@
-<p> Two <a>valid</a> PROV instances are <dfn>equivalent</dfn> if they
+<p> Two <a>valid</a> PROV instances are <dfn id="equivalence">equivalent</dfn> if they
have <a>isomorphic</a> 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,
@@ -5143,8 +5142,8 @@
the resulting notions of normalization, validity and equivalence,
work on a single PROV instance. In this
section, we describe how to deal with general PROV
-documents, possibly including multiple named bundles as well as a
-toplevel instance. Briefly, each bundle is
+documents, possibly including multiple named <dfn id="bundle">bundles</a> as well as a
+<dfn>toplevel instance</dfn>. Briefly, each bundle is
handled independently; there is no interaction between bundles from
the perspective of applying definitions, inferences, or constraints,
computing normal forms, or checking validity or equivalence.</p>