--- a/semantics/constraints.pl Sat Feb 23 16:53:17 2013 -0700
+++ b/semantics/constraints.pl Sun Feb 24 14:42:47 2013 +0000
@@ -183,7 +183,7 @@
decl('Constraint', 22, 'key-object',
rules([key(id,entity(id,attrs)),
- key(id,activity(id,t1,t2,attrs)),
+ key(id,activity(id,t_1,t_2,attrs)),
key(id,agent(id,attrs))])).
decl('Constraint', 23, 'key-properties',
@@ -193,7 +193,7 @@
key(id,wasStartedBy(id, a_2,e,a_1,t,attrs) ),
key(id,wasEndedBy(id, a_2,e,a_1,t,attrs) ),
key(id,wasInvalidatedBy(id, e,a,t,attrs) ),
- key(id,wasDerivedFrom(id, e_2, e_1, a, g2, u1, attrs) ),
+ key(id,wasDerivedFrom(id, e_2, e_1, a, g_2, u_1, attrs) ),
key(id,wasAttributedTo(id, e,ag,attr) ),
key(id,wasAssociatedWith(id, a,ag,pl,attrs) ),
key(id,actedOnBehalfOf(id, ag_2,ag_1,a,attrs) ),
@@ -258,7 +258,7 @@
[ wasEndedBy(end_1, a,e_1,a_1,t_1,attrs_1) ,
wasEndedBy(end_2, a,e_2,a_2,t_2,attrs_2) ],
[],
- [ preceq(end_1, end2)])).
+ [ preceq(end_1, end_2)])).
decl('Constraint', 33, 'usage-within-activity',
rules([rule(
@@ -437,6 +437,66 @@
wasEndedBy(end_2, ag_2,e_2,a_2,t_2,attrs_2) ],
[ preceq(start_1, end_2)])])).
+decl('Constraint',50,'typing',
+ rules([rule([e,attrs],
+ [entity(e,attrs)],
+ [typeOf(e,entity)]),
+ rule([ag,attrs],
+ [agent(ag,attrs)],
+ [typeOf(ag,agent)]),
+ rule([a,t_1,t_2,attrs],
+ [activity(a,t_1,t_2,attrs)],
+ [typeOf(a,activity)]),
+ rule([u,a,e,t,attrs],
+ [used(u,a,e,t,attrs)],
+ [typeOf(a,activity),typeOf(e,entity)]),
+ rule([g,a,e,t,attrs],
+ [wasGeneratedBy(g,e,a,t,attrs)],
+ [typeOf(a,activity),typeOf(e,entity)]),
+ rule([inf,a_2,a_1,t,attrs],
+ [wasInformedBy(inf,a_2,a_1,t,attrs)],
+ [typeOf(a_1,activity),typeOf(a_2,activity)]),
+ rule([start,a_2,e,a_1,t,attrs],
+ [wasStartedBy(start,a_2,e,a_1,t,attrs)],
+ [typeOf(a_1,activity),typeOf(a_2,activity),typeOf(e,entity)]),
+ rule([end,a_2,e,a_1,t,attrs],
+ [wasEndedBy(end,a_2,e,a_1,t,attrs)],
+ [typeOf(a_1,activity),typeOf(a_2,activity),typeOf(e,entity)]),
+ rule([inv,a,e,t,attrs],
+ [wasInvalidatedBy(inv,e,a,t,attrs)],
+ [typeOf(a,activity),typeOf(e,entity)]),
+ rule([id,e_2,e_1,a,g_2,u_1,attrs],
+ [notNull(a),notNull(g_2),notNull(u_1),wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)],
+ [typeOf(e_2,entity),typeOf(e_1,activity),typeOf(a,activity)]),
+ rule([id,e_2,e_1,attrs],
+ [wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)],
+ [typeOf(e_2,entity),typeOf(e_1,activity)]),
+ rule([id,e,ag,attrs],
+ [wasAttributedTo(id,e,ag,attrs)],
+ [typeOf(e,entity),typeOf(ag,agent)]),
+ rule([id, a,ag,pl,attrs],
+ [notNull(pl),wasAssociatedWith(id, a,ag,pl,attrs)],
+ [typeOf(a,activity),typeOf(ag,agent),typeOf(pl,entity)]),
+ rule([id, a,ag,attrs],
+ [wasAssociatedWith(id, a,ag,-,attrs)],
+ [typeOf(a,activity),typeOf(ag,agent)]),
+ rule([id, ag_2,ag_1,a,attrs],
+ [actedOnBehalfOf(id, ag_2,ag_1,a,attrs)],
+ [typeOf(ag_2,agent),typeOf(ag_1,agent),typeOf(a,activity)]),
+ rule([e_2,e_1],
+ [alternateOf(e_2, e_1)],
+ [typeOf(e_2,entity),typeOf(e_1,entity)]),
+ rule([e_2,e_1],
+ [ specializationOf(e_2, e_1)],
+ [typeOf(e_2,entity),typeOf(e_1,entity)]),
+ rule([c,e],
+ [hadMember(c,e)],
+ [typeOf(c,'prov:Collection'),typeOf(e,entity)]),
+ rule([c],
+ [entity(c,['prov:type'='prov:emptyCollection'])],
+ [typeOf(c,entity),typeOf(c,'prov:Collection'),typeOf(c,'prov:EmptyCollection')])
+ ])).
+
decl('Constraint',51,'impossible-unspecified-derivation-generation-use',
rules([rule([id,e_1,e_2,g,attrs],
@@ -499,7 +559,6 @@
emit(X,Y,Z) :- atom(X),atom_concat(Y,X,Z).
emit(X,Y,Z) :- number(X),number_codes(X,Xc),atom_codes(X2,Xc),atom_concat(Y,X2,Z).
-
emitComment(A,_) --> {atom(A)}, emit(A).
emitComment([X|Xs],T) --> emitComments([X|Xs],T).
emitComment(math(A),latex) --> emit('$'),emit(A),emit('$').
@@ -518,7 +577,7 @@
latexPred(T = U) --> emit(T), emit(' = '), emit(U),!.
-latexPred(typeOf(T,U)) --> emit(U), emit(' \\in typeOf('), emit(T), emit(')'),!.
+latexPred(typeOf(T,U)) --> emit('typeOf('),emit(T),emit(','),emit(U),emit(')'),!.
latexPred(preceq(T,U)) --> emit(T), emit(' \\preceq '), emit(U),!.
latexPred(prec(T,U)) --> emit(T), emit(' \\prec '), emit(U),!.
latexPred(A) --> {atom(A)},emit(A).
@@ -674,7 +733,9 @@
emit('</span>').
htmlRules(comment(Comment,Rules)) -->
- emitComment(Comment,html),
+ emit('<p>'),
+ emitComment(Comment,html),
+ emit('</p>'),
htmlRules(Rules).
htmlRules(rules(L)) -->
emit('<ol>'),
@@ -727,8 +788,9 @@
emit('$').
htmlLatexRules(comment(Comment,Rules)) -->
+ emit('<p>'),
emitComment(Comment,latex),
- emit('<br />'),
+ emit('</p>'),
htmlLatexRules(Rules).
htmlLatexRules(rules(L)) -->
emit('<ol>'),
--- a/semantics/prov-sem.html Sat Feb 23 16:53:17 2013 -0700
+++ b/semantics/prov-sem.html Sun Feb 24 14:42:47 2013 +0000
@@ -79,6 +79,32 @@
+.theorem {
+ padding: 1em;
+ margin: 1em 0em 0em;
+ border: 1px solid #888;
+ background: #fff;
+}
+
+.proof {
+ padding: 1em;
+ margin: 1em 0em 0em;
+ border: 1px solid #888;
+ background: #FFFFFF;
+}
+.proof::before {
+ content: "Proof";
+ display: block;
+ width: 150px;
+ margin: -1.5em 0 0.5em 0;
+ font-weight: bold;
+ border: 1px solid #000;
+ background: #fff;
+ padding: 3px 1em;
+}
+
+
+
/* .inference[id]::before { */
/* content: "Inference: " attr(id); */
/* width: 380px; /\* How can we compute the length of "Constraint: " attr(id) *\/ */
@@ -544,8 +570,8 @@
</style>
- <script src="http://dev.w3.org/2009/dap/ReSpec.js/js/respec.js" class="remove"></script>
-<!-- <script src="http://www.w3.org/Tools/respec/respec-w3c-common" class="remove" async></script> -->
+<!-- <script src="http://dev.w3.org/2009/dap/ReSpec.js/js/respec.js" class="remove"></script> -->
+ <script src="http://www.w3.org/Tools/respec/respec-w3c-common" class="remove" async></script>
<script src="http://www.w3.org/2007/OWL/toggles.js" class="remove"></script>
<script src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.1/jquery.min.js" class="remove"></script>
@@ -571,7 +597,7 @@
function updateRules() {
var count=1;
- $('.constraint,.definition,.inference,.formalism').each(function(index) {
+ $('.constraint,.definition,.inference,.formalism,.theorem').each(function(index) {
var myid=$(this).attr('id');
var mycount=$(this).attr('number');
@@ -930,34 +956,43 @@
</p>
-<p> This document ... TODO </p>
+<p> This document presents a model-theoretic semantics for the PROV
+data model (called the <dfn>reference semantics</dfn>), viewing
+PROV-DM statements as atomic formulas in the sense of first-order
+logic, and viewing the constraints and inferences specified in
+PROV-CONSTRAINTS as a first-order theory. It is shown that the
+first-order theory is sound with respect to the semantics; that any
+<em>valid</em> PROV instance corresponds to a <em>satisfiable</em>
+theory, and furthermore that any valid instance has a reference model.
+This information may be useful to researchers or users of PROV to
+understand the intended meaning and use of PROV for modeling
+information about the actual history, derivation or evolution of Web
+resources. It may also be useful for development of additional
+constraints or inferences for reasoning about PROV or integration of
+PROV with other Semantic Web vocabularies. It is <b>not</b> proposed
+as a canonical or required semantics of PROV and does not place any
+constraints on use of PROV.</p>
+
<p>The PROV Document Overview describes the overall state of PROV, and should be read before other PROV documents.</p>
</section>
<section id="sotd">
<h4>PROV Family of Documents</h4>
This document is part of the PROV family of documents, a set of documents defining various aspects that are necessary to achieve the vision of inter-operable
-interchange of provenance information in heterogeneous environments such as the Web. These documents are:
+interchange of provenance information in heterogeneous environments such as the Web. These documents are listed below. Please consult the [[PROV-OVERVIEW]] for a guide to reading these documents.
<ul>
-<li> <a href="http://www.w3.org/TR/2012/WD-prov-overview-20121211/">PROV-OVERVIEW</a> (Note), an overview of the PROV family of documents [[PROV-OVERVIEW]];</li>
-<li> <a href="http://www.w3.org/TR/2012/WD-prov-primer-20121211/">PROV-PRIMER</a> (Note), a primer for the PROV data model [[PROV-PRIMER]];</li>
-<li> <a href="http://www.w3.org/TR/2012/CR-prov-o-20121211/">PROV-O</a> (Recommendation), the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF [[PROV-O]];</li>
-<li> <a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/">PROV-DM</a> (Recommendation), the PROV data model for provenance [[PROV-DM]];</li>
-<li> <a href="http://www.w3.org/TR/2012/CR-prov-n-20121211/">PROV-N</a> (Recommendation), a notation for provenance aimed at human consumption [[PROV-N]];</li>
-<li> <a
-href="http://www.w3.org/TR/2012/CR-prov-constraints-20121211/">PROV-CONSTRAINTS</a>
-(Recommendation), a set of constraints applying to the PROV data model;</li>
-<li> <a href="http://www.w3.org/TR/2012/WD-prov-aq-20120619/">PROV-AQ</a> (Note), the mechanisms for accessing and querying provenance [[PROV-AQ]]; </li>
-<li> <a href="http://www.w3.org/TR/2012/WD-prov-xml-20121211/">PROV-XML</a> (Note), an XML schema for the PROV data model [[PROV-XML]].</li>
-
-</ul>
-<h4>How to read the PROV Family of Documents</h4>
-<ul>
-<li>The primer is the entry point to PROV offering an introduction to the provenance model.</li>
-<li>The Linked Data and Semantic Web community should focus on PROV-O defining PROV classes and properties specified in an OWL2 ontology. For further details, PROV-DM and PROV-CONSTRAINTS specify the constraints applicable to the data model, and its interpretation. </li>
-<li>Developers seeking to retrieve or publish provenance should focus on PROV-AQ.</li>
-<li>Readers seeking to implement other PROV serializations
-should focus on PROV-DM and PROV-CONSTRAINTS. PROV-O and PROV-N offer examples of mapping to RDF and text, respectively.</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-overview-20130312/">PROV-OVERVIEW</a> (To be published as Note), an overview of the PROV family of documents [[PROV-OVERVIEW]];</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-primer-20130312/">PROV-PRIMER</a> (To be published as Note), a primer for the PROV data model [[PROV-PRIMER]];</li>
+<li> <a href="http://www.w3.org/TR/2013/PR-prov-o-20130312/">PROV-O</a> (Proposed Recommendation), the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF [[!PROV-O]];</li>
+<li> <a href="http://www.w3.org/TR/2013/PR-prov-dm-20130312/">PROV-DM</a> (Proposed Recommendation), the PROV data model for provenance [[!PROV-DM]];</li>
+<li> <a href="http://www.w3.org/TR/2013/PR-prov-n-20130312/">PROV-N</a> (Proposed Recommendation), a notation for provenance aimed at human consumption [[!PROV-N]];</li>
+<li> <a href="http://www.w3.org/TR/2013/PR-prov-constraints-20130312/">PROV-CONSTRAINTS</a> (Proposed Recommendation), a set of constraints applying to the PROV data model (this document);</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-xml-20130312/">PROV-XML</a> (To be published as Note), an XML schema for the PROV data model [[PROV-XML]];</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-aq-20130312/">PROV-AQ</a> (To be published as Note), the mechanisms for accessing and querying provenance [[PROV-AQ]]; </li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-dictionary-20130312/">PROV-DICTIONARY</a> (To be published as Note) introduces a specific type of collection, consisting of key-entity pairs [[PROV-DICTIONARY]];</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-dc-20130312/">PROV-DC</a> (To be published as Note) provides a mapping between PROV and Dublic Core Terms [[PROV-DC]];</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-sem-20130312/">PROV-SEM</a> (To be published as Note), a declarative specification in terms of first-order logic of the PROV data model [[PROV-SEM]];</li>
+<li> <a href="http://www.w3.org/TR/2013/WD-prov-links-20130312/">PROV-LINKS</a> (To be published as Note) introduces a mechanism to link across bundles [[PROV-LINKS]].</li>
</ul>
</section>
@@ -972,7 +1007,13 @@
Provenance is a record that describes the people, institutions, entities, and activities involved in producing, influencing, or delivering a piece of data or a thing.
This document complements
the PROV-DM specification [[PROV-DM]] that defines a data model for
- provenance on the Web. This document defines a form of validation for provenance. </p>
+ provenance on the Web, and the PROV-CONSTRAINTS specification
+[[PROV-CONSTRAINTS]] that
+specifies definitions, inferences, and constraints that can be used to
+reason about, or determine the validity, of PROV documents. It
+provides a reference formal semantics of PROV, providing a formal
+counterpart to the informal descriptions and motivations given
+elsewhere in PROV specifications.</p>
@@ -996,12 +1037,68 @@
<h3>Purpose of this document</h3>
</section>
-
-<section>
-<h4>Structure of this document</h4>
-<p>
+<p>The PROV-DM and PROV-CONSTRAINTS give motivating examples that
+provide an intuition about the meaning of the constructs. For some
+concepts, such as use, start, end, generation/invaludation, and
+derivation, the meaning is either obvious or implementation-dependent.
+However, during the development of PROV, the importance of additional
+concepts became evident, but the intuitive meaning or correct use of
+these concepts were not clear. For example, the $alternateOf$ and
+$specializationOf$ relations are used in PROV to relate different
+entities that present aspects of "the same thing".
+Over time the working group came to a
+consensus about these concepts and how they are to be used, but this
+understanding is based on abstract notions that are not explicit in
+PROV documents; instead, some of their properties are captured
+formally through certain constraints and inferences, while others are
+not captured in PROV specifications at all.
</p>
+<p>The purpose of this document is to present the working group's
+consensus view of the semantics of PROV, using tools from mathematical
+logic, principally model theory (though our use of these tools is not
+deep). This information may be useful to users for understanding the
+intent behind certain features of PROV, to researchers investigating
+richer forms of reasoning over provenance, or to future efforts
+building upon PROV. It is intended as an exploration of a <b>reference</b>
+semantics for PROV, not a definitive specification of the <b>only</b>
+semantics of PROV. </p>
+
+<p> Nevertheless, the reference semantics does have appealing
+properties. Specifically, it provides a declarative counterpart to
+the operational definition of validity taken in PROV-CONSTRAINTS. In
+the specification, validity is defined via a normalization process
+followed by constraint checking on the normal form. This approach is
+to keep the specification closer to implementations, although other
+implementations are possible and allowed. In addition to providing a
+reference semantics, this document shows that the operational
+presentation of PROV validity checking is equivalent to the
+declarative presentation adopted here, and any other algorithm for
+deciding satisfiability of first-order theories could also be used for
+PROV.</p>
+
+<section> <h4>Structure of this document</h4> <p>
+
+</p>
+
+<ul>
+ <li><a href="#basics">Section 2</a> summarizes the basic concepts
+ from mathematical logic used in the semantics, recapitulates how
+ PROV statements can be viewed as atomic formulas, and introduces
+ some auxiliary formulas.</li>
+ <li><a href="#structures">Section 3</a> presents the mathematical
+ structures used for situations that PROV statements can
+ describe.</li>
+ <li><a href="#semantics">Section 4</a> defines the semantics of PROV
+ statements and auxiliary formulas, indicating when a given formula
+ is satisfied in a structure.</li>
+ <li><a href="#theory">Section 5</a> presents the inferences and
+ constraints from PROV-CONSTRAINTS as first-order formulas, and gives
+ brief justifications for their soundness.</li>
+ <li><a href="#completeness">Section 6</a> relates the PROV notion of
+ validity to the logical notion of consistency. A PROV instance is
+ valid if and only if its corresponding first-order theory is
+ satisfiable. </li>
</section>
@@ -1009,14 +1106,28 @@
<h3> Audience </h3>
-<p>This document assumes familiarity with [[PROV-DM]] and employs the
-[[PROV-N]] notation.
+<p>This document assumes familiarity with [[PROV-DM]] and
+ [[PROV-CONSTRAINTS]] and employs (a
+ simplified form of)
+[[PROV-N]] notation. In particular it assumes familiarity with the concepts
+ from logic, and the relationship between PROV statements and
+ instances and first-order formulas and theories, respectively,
+ presented in <a href="http://www.w3.org/TR/2013/PR-prov-constraints-20130312/#overview">Section 2.5</a> of PROV-CONSTRAINTS.
</p>
-</section>
-</section>
-
-
+ <p>This document may be useful to users of PROV who have a formal
+ background and are interested in the rationale for some of the
+ constructs of PROV; for resaerchers investigating extensions of PROV
+ or alternative approaches to reasoning about PROV; or for future
+ efforts on provenance standardization. </p>
+
+ </section>
+
+ </section>
+
+
+ <!--
+
<section id="overview">
<h2> Overview </h2>
@@ -1046,6 +1157,7 @@
<p>One goal of the semantics is to link the procedural specification of validity and equivalence with traditional notions of logical consistency and equivalence of theories, for example in first-order logic. A first-order axiomatization that corresponds to the formal constraints and is sound for reasoning about the models described below is in progress at the end of the document.
</p>
</section>
+-->
<section id="basics">
<h2> Basics </h2>
@@ -1053,24 +1165,24 @@
-<p>I will use syntax for PROV-DM records (which I will usually call
-formulas) as described in the Candidate Recommendation of PROV-DM (<a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211"> PROV-DM CR</a>).
-</p>
-<p>A PROV-DM instance, or set of atomic formulas $\phi_1$...$\phi_n$, is interpreted as a conjunction, that is, the overall instance is considered to hold in a given structure if each atomic formula in it holds.</p>
-
-<p>The rest of the document will discuss the structures and define when an atomic assertion holds in a given world.
-</p>
+
+<section>
<h3> Identifiers </h3>
<p>A lowercase symbol $x,y,...$ on its own denotes an identifier. Identifiers may or may not be URIs. I view identifiers as being like variables in logic (or blank nodes in RDF): just because we have two different identifiers $x$ and $y$ doesn't tell us that they denote different things, since we could discover that they are actually the same later. We write $Identifiers$ for the set of identifiers of interest in a given situation (typically, the set of identifiers present in the PROV instance of interest).
</p>
+</section>
+
+<section>
<h3> Times and Intervals </h3>
<p>We assume a linearly ordered set $(Times,\leq)$ of time instants. For convenience we assume the order is total or linear order, corresponding to a linear timeline; however, PROV does not assume that time is linear and events could be partially ordered and not necessarily reconciled to a single global clock.
</p>
<p>We also consider a set $Intervals$ of closed intervals of the form $\{t \mid t_1 \leq t \leq t_2\}$.
</p>
-
+</section>
+
+<section>
<h3> Attributes and Values </h3>
<p>We assume a set $Attributes$ of attribute labels and a set $Values$ of possible values of attributes.
@@ -1078,7 +1190,7 @@
</section>
<section id="formulas">
-<h2>Formulas </h2>
+<h2>Atomic Formulas</h2>
<p>The following atomic formulas correspond to the statements of PROV-DM. We assume that definitions 1-4 of PROV-CONSTRAINTS have been applied in order to expand all optional parameters; thus, we use uniform notation $r(id,a_1,\ldots,a_n)$ instead of the semicolon notation $r(id;a_1,\ldots,a_n)$.
</p>
@@ -1086,14 +1198,15 @@
</p>
$$
\begin{array}{rcl}
- formula &::=& element\_formula\\
+ atomic\_formula &{::=}& element\_formula\\
& | & relation\_formula\\
+ & | & auxiliary\_formula\\
element\_formula
- &::= &entity(id,attrs) \\
+ &{::=} &entity(id,attrs) \\
& |& activity(id,st,et,attrs)\\
& |& agent(id,attrs)\\
relation\_formula
- &::=& wasGeneratedBy(id,e,a,t,attrs)\\
+ &{::=}& wasGeneratedBy(id,e,a,t,attrs)\\
& |& used(id,e,a,t,attrs)\\
& |& wasInvalidatedBy(id,e,a,t,attrs)\\
& |& wasAssociatedWith(id,ag,act,pl,attrs)\\
@@ -1105,13 +1218,66 @@
& |& wasDerivedFrom(id,e_2,e_1,act,g,u,attrs)\\
& |& wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)\\
& |& alternateOf(e_1,e_2)\\
- & |& specializationOf(e_1,e_2)
+ & |& specializationOf(e_1,e_2)\\
+ auxiliary\_formula
+ &{::=}& x \prec y\\
+ & | & x \preceq y\\
+ & | & notNull(x)\\
+ & | & typeOf(x,ty)\\
+ ty &{::=}& entity \\
+&|& activity\\
+&|& agent\\
+&|& prov:collection\\
+&|& prov:EmptyCollection
\end{array}
$$
</section>
-<section id="models">
-<h2> World Models </h2>
+
+<section>
+<h3>First-Order Formulas</h3>
+
+<p>We also consider the usual connectives and quantifiers of
+first-order logic [[Logic]].
+$$
+\begin{array}{rcl}
+ formula &{::=}& atomic\_formula\\
+ &|& formula_1 \wedge formula_2\\
+ &|& formula_1 \vee formula_2\\
+&|& \neg~formula\\
+&|& \forall x. formula\\
+&|& \exists x. formula
+\end{array}
+$$
+
+
+</section>
+<section>
+<h3>Instances as Theories</h3>
+<p>A PROV-DM
+instance can be viewed as a set of atomic formulas
+$\phi_1$...$\phi_n$, often called a <em>theory</em>. A theory is
+viewed as a conjunction, that is, the overall instance is considered
+to hold in a given structure if each atomic formula in it holds.</p>
+</section>
+
+<section>
+<h3> Interpretations </h3>
+
+<p>We need to link identifiers to the objects they denote. We do this using a function which we shall call an <em>interpretation</em>.
+</p>
+<p>The mapping from identifiers to objects may <b>not</b> change over time. Thus, we consider interpretations as follows:
+An interpretation function $I : Identifiers \to Objects$ describing
+which object is the target of each identifier.
+</p>
+</section>
+
+
+</section>
+
+
+<section id="structures">
+<h2> Structures </h2>
<h3> Things </h3>
@@ -1276,14 +1442,6 @@
</p>
<p>The annotations [WF] refer to well-formedness constraints that correspond to typing constraints.
</p>
-<h3> Interpretations </h3>
-
-<p>We need to link identifiers to the objects they denote. We do this using a function which we shall call an <em>interpretation</em>.
-</p>
-<p>The mapping from identifiers to objects may <b>not</b> change over time. Thus, we consider interpretations as follows:
-</p>
-<div class="formalism"> An interpretation function $I : Identifiers \to Objects$ describing which object is the target of each identifier.
-</div>
<h3> Satisfaction </h3>
@@ -1634,8 +1792,682 @@
</section>
-<section id="formalizations">
-<h2> Formalizations of Inferences and Constraints </h2>
+<section id="theory">
+<h2> Inferences and Constraints </h2>
+
+<div class="inference" number="5" id="communication-generation-use-inference">$\begin{array}[t]{l}
+\forall id,a_2,a_1,attrs.~
+\\
+\qquad wasInformedBy(id,a_2,a_1,attrs)
+\\
+\quad\Rightarrow
+\exists e,gen,t_1,use,t_2.~wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge used(use,a_2,e,t_2,[])
+\end{array}$</div>
+<div class="inference" number="6" id="generation-use-communication-inference">$\begin{array}[t]{l}
+\forall gen,e,a_1,t_1,attrs_1,id_2,a_2,t_2,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(id_2,a_2,e,t_2,attrs_2)
+\\
+\quad\Rightarrow
+\exists id.~wasInformedBy(id,a_2,a_1,[])
+\end{array}$</div>
+<div class="inference" number="7" id="entity-generation-invalidation-inference">$\begin{array}[t]{l}
+\forall e,attrs.~
+\\
+\qquad entity(e,attrs)
+\\
+\quad\Rightarrow
+\exists gen,a_1,t_1,inv,a_2,t_2.~wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge wasInvalidatedBy(inv,e,a_2,t_2,[])
+\end{array}$</div>
+<div class="inference" number="8" id="activity-start-end-inference">$\begin{array}[t]{l}
+\forall a,t_1,t_2,attrs.~
+\\
+\qquad activity(a,t_1,t_2,attrs)
+\\
+\quad\Rightarrow
+\exists start,e_1,a_1,end,a_2,e_2.~wasStartedBy(start,a,e_1,a_1,t_1,[]) \wedge wasEndedBy(end,a,e_2,a_2,t_2,[])
+\end{array}$</div>
+<div class="inference" number="9" id="wasStartedBy-inference">$\begin{array}[t]{l}
+\forall id,a,e_1,a_1,t,attrs.~
+\\
+\qquad wasStartedBy(id,a,e_1,a_1,t,attrs)
+\\
+\quad\Rightarrow
+\exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])
+\end{array}$</div>
+<div class="inference" number="10" id="wasEndedBy-inference">$\begin{array}[t]{l}
+\forall id,a,e_1,a_1,t,attrs.~
+\\
+\qquad wasEndedBy(id,a,e_1,a_1,t,attrs)
+\\
+\quad\Rightarrow
+\exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])
+\end{array}$</div>
+<div class="inference" number="11" id="derivation-generation-use-inference"><p>In this inference, none of $a$,$gen_2$, or $use_1$ can be placeholders -.</p>$\begin{array}[t]{l}
+\forall id,e_2,e_1,a,gen_2,use_1,attrs.~
+\\
+\qquad notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(id,e_2,e_1,a,gen_2,use_1,attrs)
+\\
+\quad\Rightarrow
+\exists t_1,t_2.~used(use_1,a,e_1,t_1,[]) \wedge wasGeneratedBy(gen_2,e_2,a,t_2,[])
+\end{array}$</div>
+<div class="inference" number="12" id="revision-is-alternate-inference"><p>In this inference, any of $a$,$gen_2$, or $use_1$ can be placeholders -.</p>$\begin{array}[t]{l}
+\forall id,e_1,e_2,a,g,u.~
+\\
+\qquad wasDerivedFrom(id,e_2,e_1,a,g,u,.(prov:type = prov:Revision,[]))
+\\
+\quad\Rightarrow
+alternateOf(e_2,e_1)
+\end{array}$</div>
+<div class="inference" number="13" id="attribution-inference">$\begin{array}[t]{l}
+\forall att,e,ag,attrs.~
+\\
+\qquad wasAttributedTo(att,e,ag,attrs)
+\\
+\quad\Rightarrow
+\exists a,t,gen,assoc,pl.~wasGeneratedBy(gen,e,a,t,[]) \wedge wasAssociatedWith(assoc,a,ag,pl,[])
+\end{array}$</div>
+<div class="inference" number="14" id="delegation-inference">$\begin{array}[t]{l}
+\forall id,ag_1,ag_2,a,attrs.~
+\\
+\qquad actedOnBehalfOf(id,ag_1,ag_2,a,attrs)
+\\
+\quad\Rightarrow
+\exists id_1,pl_1,id_2,pl_2.~wasAssociatedWith(id_1,a,ag_1,pl_1,[]) \wedge wasAssociatedWith(id_2,a,ag_2,pl_2,[])
+\end{array}$</div>
+<div class="inference" number="15" id="influence-inference"><ol><li>$\begin{array}[t]{l}
+\forall id,e,a,t,attrs.~
+\\
+\qquad wasGeneratedBy(id,e,a,t,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,e,a,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a,e,t,attrs.~
+\\
+\qquad used(id,a,e,t,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,a,e,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a_2,a_1,attrs.~
+\\
+\qquad wasInformedBy(id,a_2,a_1,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,a_2,a_1,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a_2,e,a_1,t,attrs.~
+\\
+\qquad wasStartedBy(id,a_2,e,a_1,t,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,a_2,e,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a_2,e,a_1,t,attrs.~
+\\
+\qquad wasEndedBy(id,a_2,e,a_1,t,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,a_2,e,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e,a,t,attrs.~
+\\
+\qquad wasInvalidatedBy(id,e,a,t,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,e,a,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_2,e_1,a,g,u,attrs.~
+\\
+\qquad wasDerivedFrom(id,e_2,e_1,a,g,u,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,e_2,e_1,attrs)
+\end{array}$</li><li><p>In this rule, $a$,$g$, or $u$ may be placeholders -.</p>$\begin{array}[t]{l}
+\forall id,e,ag,attrs.~
+\\
+\qquad wasAttributedTo(id,e,ag,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,e,ag,attrs)
+\end{array}$</li><li><p>In this rule, $pl$ may be a placeholder -.</p>$\begin{array}[t]{l}
+\forall id,a,ag,pl,attrs.~
+\\
+\qquad wasAssociatedWith(id,a,ag,pl,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,a,ag,attrs)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,ag_2,ag_1,a,attrs.~
+\\
+\qquad actedOnBehalfOf(id,ag_2,ag_1,a,attrs)
+\\
+\quad\Rightarrow
+wasInfluencedBy(id,ag_2,ag_1,attrs)
+\end{array}$</li></ol></div>
+<div class="inference" number="16" id="alternate-reflexive">$\begin{array}[t]{l}
+\forall e.~
+\\
+\qquad entity(e)
+\\
+\quad\Rightarrow
+alternateOf(e,e)
+\end{array}$</div>
+<div class="inference" number="17" id="alternate-transitive">$\begin{array}[t]{l}
+\forall e_1,e_2,e_3.~
+\\
+\qquad alternateOf(e_1,e_2) \wedge alternateOf(e_2,e_3)
+\\
+\quad\Rightarrow
+alternateOf(e_1,e_3)
+\end{array}$</div>
+<div class="inference" number="18" id="alternate-symmetric">$\begin{array}[t]{l}
+\forall e_1,e_2.~
+\\
+\qquad alternateOf(e_1,e_2)
+\\
+\quad\Rightarrow
+alternateOf(e_2,e_1)
+\end{array}$</div>
+<div class="inference" number="19" id="specialization-transitive">$\begin{array}[t]{l}
+\forall e_1,e_2,e_3.~
+\\
+\qquad specializationOf(e_1,e_2) \wedge specializationOf(e_2,e_3)
+\\
+\quad\Rightarrow
+specializationOf(e_1,e_3)
+\end{array}$</div>
+<div class="inference" number="20" id="specialization-alternate-inference">$\begin{array}[t]{l}
+\forall e_1,e_2.~
+\\
+\qquad specializationOf(e_1,e_2)
+\\
+\quad\Rightarrow
+alternateOf(e_1,e_2)
+\end{array}$</div>
+<div class="inference" number="21" id="specialization-attributes-inference">$\begin{array}[t]{l}
+\forall e_1,attrs,e_2.~
+\\
+\qquad entity(e_1,attrs) \wedge specializationOf(e_2,e_1)
+\\
+\quad\Rightarrow
+entity(e_2,attrs)
+\end{array}$</div>
+<div class="constraint" number="22" id="key-object"><ol><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $entity(id,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $activity(id,t_1,t_2,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $agent(id,attrs)$ statement.</li></ol></div>
+<div class="constraint" number="23" id="key-properties"><ol><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasGeneratedBy(id,e,a,t,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $used(id,a,e,t,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasInformedBy(id,a_2,a_1,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasStartedBy(id,a_2,e,a_1,t,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasEndedBy(id,a_2,e,a_1,t,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasInvalidatedBy(id,e,a,t,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasAttributedTo(id,e,ag,attr)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasAssociatedWith(id,a,ag,pl,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $actedOnBehalfOf(id,ag_2,ag_1,a,attrs)$ statement.</li><li>The identifier field $id$ is a <span class="conditional">KEY</span> for the $wasInfluencedBy(id,o2,o1,attrs)$ statement.</li></ol></div>
+<div class="constraint" number="24" id="unique-generation">$\begin{array}[t]{l}
+\forall gen_1,gen_2,e,a,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen_1,e,a,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 = gen_2
+\end{array}$</div>
+<div class="constraint" number="25" id="unique-invalidation">$\begin{array}[t]{l}
+\forall inv_1,inv_2,e,a,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasInvalidatedBy(inv_1,e,a,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e,a,t_2,attrs_2)
+\\
+\quad\Rightarrow
+inv_1 = inv_2
+\end{array}$</div>
+<div class="constraint" number="26" id="unique-wasStartedBy">$\begin{array}[t]{l}
+\forall start_1,start_2,a,e_1,e_2,a_0,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasStartedBy(start_1,a,e_1,a_0,t_1,attrs_1) \wedge wasStartedBy(start_2,a,e_2,a_0,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 = start_2
+\end{array}$</div>
+<div class="constraint" number="27" id="unique-wasEndedBy">$\begin{array}[t]{l}
+\forall end_1,end_2,a,e_1,e_2,a_0,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasEndedBy(end_1,a,e_1,a_0,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_0,t_2,attrs_2)
+\\
+\quad\Rightarrow
+end_1 = end_2
+\end{array}$</div>
+<div class="constraint" number="28" id="unique-startTime">$\begin{array}[t]{l}
+\forall start,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1.~
+\\
+\qquad activity(a_2,t_1,t_2,attrs) \wedge wasStartedBy(start,a_2,e,a_1,t,attrs_1)
+\\
+\quad\Rightarrow
+t_1 = t
+\end{array}$</div>
+<div class="constraint" number="29" id="unique-endTime">$\begin{array}[t]{l}
+\forall end,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1.~
+\\
+\qquad activity(a_2,t_1,t_2,attrs) \wedge wasEndedBy(end,a_2,e,a_1,t,attrs_1)
+\\
+\quad\Rightarrow
+t_2 = t
+\end{array}$</div>
+<div class="constraint" number="30" id="start-precedes-end">$\begin{array}[t]{l}
+\forall start,end,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start \preceq end
+\end{array}$</div>
+<div class="constraint" number="31" id="start-start-ordering">$\begin{array}[t]{l}
+\forall start_1,start_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasStartedBy(start_2,a,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 \preceq start_2
+\end{array}$</div>
+<div class="constraint" number="32" id="end-end-ordering">$\begin{array}[t]{l}
+\forall end_1,end_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasEndedBy(end_1,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+end_1 \preceq end_2
+\end{array}$</div>
+<div class="constraint" number="33" id="usage-within-activity"><ol><li>$\begin{array}[t]{l}
+\forall start,use,a,e_1,e_2,a_1,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge used(use,a,e_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start \preceq use
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall use,end,a,e_1,e_2,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad used(use,a,e_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+use \preceq end
+\end{array}$</li></ol></div>
+<div class="constraint" number="34" id="generation-within-activity"><ol><li>$\begin{array}[t]{l}
+\forall start,gen,e_1,e_2,a,a_1,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen,e_2,a,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start \preceq gen
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall gen,end,e,e_1,a,a_1,t,t_1,attrs,attrs_1.~
+\\
+\qquad wasGeneratedBy(gen,e,a,t,attrs) \wedge wasEndedBy(end,a,e_1,a_1,t_1,attrs_1)
+\\
+\quad\Rightarrow
+gen \preceq end
+\end{array}$</li></ol></div>
+<div class="constraint" number="35" id="wasInformedBy-ordering">$\begin{array}[t]{l}
+\forall id,start,end,a_1,a_1',a_2,a_2',e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2.~
+\\
+\qquad wasInformedBy(id,a_2,a_1,attrs) \wedge wasStartedBy(start,a_1,e_1,a_1',t_1,attrs_1) \wedge wasEndedBy(end,a_2,e_2,a_2',t_2,attrs_2)
+\\
+\quad\Rightarrow
+start \preceq end
+\end{array}$</div>
+<div class="constraint" number="36" id="generation-precedes-invalidation">$\begin{array}[t]{l}
+\forall gen,inv,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen \preceq inv
+\end{array}$</div>
+<div class="constraint" number="37" id="generation-precedes-usage">$\begin{array}[t]{l}
+\forall gen,use,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(use,a_2,e,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen \preceq use
+\end{array}$</div>
+<div class="constraint" number="38" id="usage-precedes-invalidation">$\begin{array}[t]{l}
+\forall use,inv,a_1,a_2,e,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad used(use,a_1,e,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+use \preceq inv
+\end{array}$</div>
+<div class="constraint" number="39" id="generation-generation-ordering">$\begin{array}[t]{l}
+\forall gen_1,gen_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen_1,e,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 \preceq gen_2
+\end{array}$</div>
+<div class="constraint" number="40" id="invalidation-invalidation-ordering">$\begin{array}[t]{l}
+\forall inv_1,inv_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasInvalidatedBy(inv_1,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+inv_1 \preceq inv_2
+\end{array}$</div>
+<div class="constraint" number="41" id="derivation-usage-generation-ordering"><p>In this constraint$a$,$gen_2$, or $use_1$ must not be placeholders -.</p>$\begin{array}[t]{l}
+\forall d,e_1,e_2,a,gen_2,use_1,attrs.~
+\\
+\qquad notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(d,e_2,e_1,a,gen_2,use_1,attrs)
+\\
+\quad\Rightarrow
+use_1 \preceq gen_2
+\end{array}$</div>
+<div class="constraint" number="42" id="derivation-generation-generation-ordering"><p>In this constraint, any of $a$,$g$, or $u$ may be placeholders -.</p>$\begin{array}[t]{l}
+\forall d,gen_1,gen_2,e_1,e_2,a,a_1,a_2,g,u,t_1,t_2,attrs,attrs_1,attrs_2.~
+\\
+\qquad wasDerivedFrom(d,e_2,e_1,a,g,u,attrs) \wedge wasGeneratedBy(gen_1,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 \prec gen_2
+\end{array}$</div>
+<div class="constraint" number="43" id="wasStartedBy-ordering"><ol><li>$\begin{array}[t]{l}
+\forall gen,start,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasStartedBy(start,a,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen \preceq start
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall start,inv,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasStartedBy(start,a,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start \preceq inv
+\end{array}$</li></ol></div>
+<div class="constraint" number="44" id="wasEndedBy-ordering"><ol><li>$\begin{array}[t]{l}
+\forall gen,end,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen \preceq end
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall end,inv,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasEndedBy(end,a,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+end \preceq inv
+\end{array}$</li></ol></div>
+<div class="constraint" number="45" id="specialization-generation-ordering">$\begin{array}[t]{l}
+\forall gen_1,gen_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad specializationOf(e_2,e_1) \wedge wasGeneratedBy(gen_1,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 \preceq gen_2
+\end{array}$</div>
+<div class="constraint" number="46" id="specialization-invalidation-ordering">$\begin{array}[t]{l}
+\forall inv_1,inv_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad specializationOf(e_1,e_2) \wedge wasInvalidatedBy(inv_1,e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+inv_1 \preceq inv_2
+\end{array}$</div>
+<div class="constraint" number="47" id="wasAssociatedWith-ordering"><p>In the following inferences, $pl$ may be a placeholder -.</p><ol><li>$\begin{array}[t]{l}
+\forall assoc,start_1,inv_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,ag,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 \preceq inv_2
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall assoc,gen_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasGeneratedBy(gen_1,ag,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 \preceq end_2
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall assoc,start_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,ag,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 \preceq end_2
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall assoc,start_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~
+\\
+\qquad wasAssociatedWith(assoc,a,ag,pl,attrs) \wedge wasStartedBy(start_1,ag,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 \preceq end_2
+\end{array}$</li></ol></div>
+<div class="constraint" number="48" id="wasAttributedTo-ordering"><ol><li>$\begin{array}[t]{l}
+\forall att,gen_1,gen_2,e,a_1,a_2,t_1,t_2,ag,attrs,attrs_1,attrs_2.~
+\\
+\qquad wasAttributedTo(att,e,ag,attrs) \wedge wasGeneratedBy(gen_1,ag,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 \preceq gen_2
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall att,start_1,gen_2,e,e_1,a_1,a_2,ag,t_1,t_2,attrs,attrs_1,attrs_2.~
+\\
+\qquad wasAttributedTo(att,e,ag,attrs) \wedge wasStartedBy(start_1,ag,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 \preceq gen_2
+\end{array}$</li></ol></div>
+<div class="constraint" number="49" id="actedOnBehalfOf-ordering"><ol><li>$\begin{array}[t]{l}
+\forall del,gen_1,inv_2,ag_1,ag_2,a,a_1,a_2,t_1,t_2,attrs,attrs_1,attrs_2.~
+\\
+\qquad actedOnBehalfOf(del,ag_2,ag_1,a,attrs) \wedge wasGeneratedBy(gen_1,ag_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,ag_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+gen_1 \preceq inv_2
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall del,start_1,end_2,ag_1,ag_2,a,a_1,a_2,e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2.~
+\\
+\qquad actedOnBehalfOf(del,ag_2,ag_1,a,attrs) \wedge wasStartedBy(start_1,ag_1,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,ag_2,e_2,a_2,t_2,attrs_2)
+\\
+\quad\Rightarrow
+start_1 \preceq end_2
+\end{array}$</li></ol></div>
+<div class="constraint" number="50" id="typing"><ol><li>$\begin{array}[t]{l}
+\forall e,attrs.~
+\\
+\qquad entity(e,attrs)
+\\
+\quad\Rightarrow
+typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall ag,attrs.~
+\\
+\qquad agent(ag,attrs)
+\\
+\quad\Rightarrow
+typeOf(ag,agent)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall a,t_1,t_2,attrs.~
+\\
+\qquad activity(a,t_1,t_2,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall u,a,e,t,attrs.~
+\\
+\qquad used(u,a,e,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall g,a,e,t,attrs.~
+\\
+\qquad wasGeneratedBy(g,e,a,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall inf,a_2,a_1,t,attrs.~
+\\
+\qquad wasInformedBy(inf,a_2,a_1,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a_1,activity) \wedge typeOf(a_2,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall start,a_2,e,a_1,t,attrs.~
+\\
+\qquad wasStartedBy(start,a_2,e,a_1,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a_1,activity) \wedge typeOf(a_2,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall end,a_2,e,a_1,t,attrs.~
+\\
+\qquad wasEndedBy(end,a_2,e,a_1,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a_1,activity) \wedge typeOf(a_2,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall inv,a,e,t,attrs.~
+\\
+\qquad wasInvalidatedBy(inv,e,a,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_2,e_1,a,g_2,u_1,attrs.~
+\\
+\qquad notNull(a) \wedge notNull(g_2) \wedge notNull(u_1) \wedge wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,activity) \wedge typeOf(a,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_2,e_1,attrs.~
+\\
+\qquad wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e,ag,attrs.~
+\\
+\qquad wasAttributedTo(id,e,ag,attrs)
+\\
+\quad\Rightarrow
+typeOf(e,entity) \wedge typeOf(ag,agent)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a,ag,pl,attrs.~
+\\
+\qquad notNull(pl) \wedge wasAssociatedWith(id,a,ag,pl,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(ag,agent) \wedge typeOf(pl,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a,ag,attrs.~
+\\
+\qquad wasAssociatedWith(id,a,ag,-,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(ag,agent)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,ag_2,ag_1,a,attrs.~
+\\
+\qquad actedOnBehalfOf(id,ag_2,ag_1,a,attrs)
+\\
+\quad\Rightarrow
+typeOf(ag_2,agent) \wedge typeOf(ag_1,agent) \wedge typeOf(a,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall e_2,e_1.~
+\\
+\qquad alternateOf(e_2,e_1)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall e_2,e_1.~
+\\
+\qquad specializationOf(e_2,e_1)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall c,e.~
+\\
+\qquad hadMember(c,e)
+\\
+\quad\Rightarrow
+typeOf(c,prov:Collection) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall c.~
+\\
+\qquad entity(c,.(prov:type = prov:emptyCollection,[]))
+\\
+\quad\Rightarrow
+typeOf(c,entity) \wedge typeOf(c,prov:Collection) \wedge typeOf(c,prov:EmptyCollection)
+\end{array}$</li></ol></div>
+<div class="constraint" number="51" id="impossible-unspecified-derivation-generation-use"><ol><li>$\begin{array}[t]{l}
+\forall id,e_1,e_2,g,attrs.~
+\\
+\qquad notNull(g) \wedge wasDerivedFrom(id,e_2,e_1,-,g,-,attrs)
+\\
+\quad\Rightarrow
+False
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_1,e_2,u,attrs.~
+\\
+\qquad notNull(u) \wedge wasDerivedFrom(id,e_2,e_1,-,-,u,attrs)
+\\
+\quad\Rightarrow
+False
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_1,e_2,g,u,attrs.~
+\\
+\qquad notNull(g) \wedge notNull(u) \wedge wasDerivedFrom(id,e_2,e_1,-,g,u,attrs)
+\\
+\quad\Rightarrow
+False
+\end{array}$</li></ol></div>
+<div class="constraint" number="52" id="impossible-specialization-reflexive">$\begin{array}[t]{l}
+\forall e.~
+\\
+\qquad specializationOf(e,e)
+\\
+\quad\Rightarrow
+False
+\end{array}$</div>
+<div class="constraint" number="53" id="impossible-property-overlap"><p>For each $r$ and $s \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$ such that $r$ and $s$ are different relation names, the following constraint holds:</p>$\begin{array}[t]{l}
+\forall id,a_1,\ldots,a_m,b_1,\ldots,b_n.~
+\\
+\qquad r(id,a_1,\ldots,a_m) \wedge s(id,b_1,\ldots,b_n)
+\\
+\quad\Rightarrow
+False
+\end{array}$</div>
+<div class="constraint" number="54" id="impossible-object-property-overlap"><p>For each $p \in \{entity,activity,agent\}$ and each $r \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$, the following constraint holds:</p>$\begin{array}[t]{l}
+\forall id,a_1,\ldots,a_m,b_1,\ldots,b_n.~
+\\
+\qquad p(id,a_1,\ldots,a_m) \wedge r(id,b_1,\ldots,b_n)
+\\
+\quad\Rightarrow
+False
+\end{array}$</div>
+<div class="constraint" number="55" id="entity-activity-disjoint">$\begin{array}[t]{l}
+\forall id.~
+\\
+\qquad typeOf(id,entity) \wedge typeOf(id,activity)
+\\
+\quad\Rightarrow
+False
+\end{array}$</div>
+<div class="constraint" number="56" id="membership-empty-collection">$\begin{array}[t]{l}
+\forall c,e.~
+\\
+\qquad hasMember(c,e) \wedge typeOf(c,prov:EmptyCollection)
+\\
+\quad\Rightarrow
+False
+\end{array}$</div>
+
+
+<!--
+
+<h2>OLD</h2>
<div class="inference" number="5" id="communication-generation-use-inference">$\begin{array}[t]{l}
\forall id,a_2,a_1,attrs.~
@@ -2109,6 +2941,141 @@
\quad\Rightarrow
start_1 \preceq end2
\end{array}$</li></ol></div>
+
+<div class="constraint" number="50" id="typing"><ol><li>$\begin{array}[t]{l}
+\forall e,attrs.~
+\\
+\qquad entity(e,attrs)
+\\
+\quad\Rightarrow
+typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall ag,attrs.~
+\\
+\qquad agent(ag,attrs)
+\\
+\quad\Rightarrow
+typeOf(ag,agent)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall a,t_1,t_2,attrs.~
+\\
+\qquad activity(a,t_1,t_2,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall u,a,e,t,attrs.~
+\\
+\qquad used(u,a,e,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall g,a,e,t,attrs.~
+\\
+\qquad wasGeneratedBy(g,e,a,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall inf,a_2,a_1,t,attrs.~
+\\
+\qquad wasInformedBy(inf,a_2,a_1,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a_1,activity) \wedge typeOf(a_2,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall start,a_2,e,a_1,t,attrs.~
+\\
+\qquad wasStartedBy(start,a_2,e,a_1,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a_1,activity) \wedge typeOf(a_2,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall end,a_2,e,a_1,t,attrs.~
+\\
+\qquad wasEndedBy(end,a_2,e,a_1,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a_1,activity) \wedge typeOf(a_2,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall inv,a,e,t,attrs.~
+\\
+\qquad wasInvalidatedBy(inv,e,a,t,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_2,e_1,a,g_2,u_1,attrs.~
+\\
+\qquad notNull(a) \wedge notNull(g_2) \wedge notNull(u_1) \wedge wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,activity) \wedge typeOf(a,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e_2,e_1,attrs.~
+\\
+\qquad wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,e,ag,attrs.~
+\\
+\qquad wasAttributedTo(id,e,ag,attrs)
+\\
+\quad\Rightarrow
+typeOf(e,entity) \wedge typeOf(ag,agent)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a,ag,pl,attrs.~
+\\
+\qquad notNull(pl) \wedge wasAssociatedWith(id,a,ag,pl,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(ag,agent) \wedge typeOf(pl,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,a,ag,attrs.~
+\\
+\qquad wasAssociatedWith(id,a,ag,-,attrs)
+\\
+\quad\Rightarrow
+typeOf(a,activity) \wedge typeOf(ag,agent)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall id,ag_2,ag_1,a,attrs.~
+\\
+\qquad actedOnBehalfOf(id,ag_2,ag_1,a,attrs)
+\\
+\quad\Rightarrow
+typeOf(ag_2,agent) \wedge typeOf(ag_1,agent) \wedge typeOf(a,activity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall e_2,e_1.~
+\\
+\qquad alternateOf(e_2,e_1)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall e_2,e_1.~
+\\
+\qquad specializationOf(e_2,e_1)
+\\
+\quad\Rightarrow
+typeOf(e_2,entity) \wedge typeOf(e_1,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall c,e.~
+\\
+\qquad hadMember(c,e)
+\\
+\quad\Rightarrow
+typeOf(c,prov:Collection) \wedge typeOf(e,entity)
+\end{array}$</li><li>$\begin{array}[t]{l}
+\forall c.~
+\\
+\qquad entity(c,.(prov:type = prov:emptyCollection,[]))
+\\
+\quad\Rightarrow
+typeOf(c,entity) \wedge typeOf(c,prov:Collection) \wedge typeOf(c,prov:EmptyCollection)
+\end{array}$</li></ol></div>
<div class="constraint" number="51" id="impossible-unspecified-derivation-generation-use"><ol><li>$\begin{array}[t]{l}
\forall id,e_1,e_2,g,attrs.~
\\
@@ -2147,14 +3114,18 @@
\quad\Rightarrow
False
\end{array}$</div>
-<div class="constraint" number="54" id="impossible-object-property-overlap">For each $p \in \{entity,activity,agent\}$ and each $r \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$, the following constraint holds:<br />$\begin{array}[t]{l}
+<div class="constraint" number="54"
+ id="impossible-object-property-overlap">
+ <p>
+ For each $p \in \{entity,activity,agent\}$ and each $r \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$, the following constraint holds:<br />$\begin{array}[t]{l}
\forall id,a_1,\ldots,a_m,b_1,\ldots,b_n.~
\\
\qquad p(id,a_1,\ldots,a_m) \wedge r(id,b_1,\ldots,b_n)
\\
\quad\Rightarrow
False
-\end{array}$</div>
+\end{array}$</p>
+</div>
<div class="constraint" number="55" id="entity-activity-disjoint">$\begin{array}[t]{l}
\forall id.~
\\
@@ -2172,15 +3143,76 @@
False
\end{array}$</div>
+-->
</section>
+<section id="completeness">
+<h2>Soundness and Completeness</h2>
+
+<p>Above we have presented arguments for the soundness of the
+constraints and inferences with respect to the reference semantics.
+This implies the following:
+
+<div class="theorem" id="soundness">
+ <ol>
+ <li>If $I$ is an instance and $W \models I$ and $I'$ is obtained from $I$ by applying one
+ of the PROV inferences, then $W \models I'$.</li>
+ <li>If $I$ is an instance and $W \models I$ then $I$ has a normal
+ form $I'$ and $ W \models I'$.</li>
+ <li>If $I$ is a normal form and $W \models I$ then $I$ satisfies all of the ordering,
+ typing and impossibility constraints.
+ <li>If $W \models I$ then $I$ is valid.</li>
+ </p>
+</div>
+<div class="proof">
+ <p>For part 1, the arguments are as in the previous section. </p>
+ <p>For
+ part 2, proceed by induction on a terminating sequence of inference
+ or uniqueness constraint steps: if $I$ is in normal form them we are
+ done. If $I$ is not in normal form then if an inference is applicable, then use part 1; if a uniqueness constraint is
+ applicable, then from $W \models I$ the uniqueness constraint cannot
+ fail on $I$ and $W \models I'$.</p>
+<p>
+ For part 3, the arguments are as
+ in the previous section for each constraints. </p>
+ <p>Finally, for part 4,
+ suppose $W \models I$. Then $W \models I'$ where $I'$ is the normal
+ form of $I$ by part 2. By part 3, $I'$ satisfies all of the
+ remaining constraints, so $I$ is valid.</p>
+ </div>
+
+<p> The goal of this section is to prove the converse: if $I$ is valid
+ then it has a (reference) model. First, however, observe that this
+ is not true in general for first-order theories with respect to PROV
+ reference models: for example, the fact that time instants are
+ linearly ordered ($t < t' \vee t = t' \vee t > t'$) does not follow
+ from the theory of PROV, but it is true in every reference model by
+ definition. Nevertheless, because we restrict attention to
+ collections of atomic formulas, it is possible to prove this.
+ Essentially, the reason is that within a PROV instance there is no
+ way to say that (for example) time instants are linearly ordered.
+ If $I$ is valid, we can obtain a unique canonical, finite, first-order model from the normal
+ form of $I$, as shown in [[DBCONSTRAINTS]]. Although this normal
+ form is not a reference model, we can transform it to a reference
+ model that still satisfies $I$.
+ </p>
+
+
+ <div class="note">
+ TODO; not sure about all of above yet.
+ </div>
+
+</section>
<section class="appendix">
<h2>Acknowledgements</h2>
<p>
This document has been produced by the PROV Working Group, and its contents reflect extensive discussion within the Working Group as a whole. The editors extend special thanks to Ivan Herman (W3C/ERCIM), Paul Groth, Tim Lebo, Simon Miles, Stian Soiland-Reyes, for their thorough reviews.
- </p>
+ </p>
+<p>Thanks also to Robin Berjon for the ReSPec.js specification writing
+tool and to MathJax for their LaTeX-to-HTML conversion tools, both of
+ which aided in the preparation of this document.</p>
<p>
Members of the PROV Working Group at the time of publication of this document were: