--- a/semantics/prov-sem.html Sun Feb 24 14:42:47 2013 +0000
+++ b/semantics/prov-sem.html Sun Feb 24 19:12:21 2013 +0000
@@ -1,7 +1,7 @@
<!DOCTYPE html>
<html><head>
- <title>Semantics of the Provenance Data Model</title>
+ <title>Semantics of the PROV Data Model</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
/>
<!--
@@ -77,6 +77,13 @@
background: #fff;
}
+.component {
+ padding: 1em;
+ margin: 1em 0em 0em;
+ border: 1px solid #088;
+ background: #fff;
+}
+
.theorem {
@@ -597,7 +604,7 @@
function updateRules() {
var count=1;
- $('.constraint,.definition,.inference,.formalism,.theorem').each(function(index) {
+ $('.constraint,.definition,.inference,.formalism,.component,.theorem').each(function(index) {
var myid=$(this).attr('id');
var mycount=$(this).attr('number');
@@ -983,9 +990,9 @@
<ul>
<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-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>
@@ -1095,11 +1102,17 @@
<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
+ <li><a href="#soundness">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>
-
+ satisfiable.</li>
+</ul>
+<div class="note">
+ Completeness direction above doesn't hold for current semantics,
+ because attributes assumed to be single-valued; for
+ example, $entity(id,[a=1,a=2])$ is valid but doesn't have a
+ reference model.
+ </div>
</section>
<section id="audience">
@@ -1146,11 +1159,19 @@
<h3> Idea of the semantics </h3>
-<p>As a starting point, I will assume that we intend the assertions made in a PROV-DM instance to be intended to describe one, consistent state of the world, much like a logical formula is said to be satisfied in a mathematical model. That is, I propose an approach similar to that taken in model theory, where the PROV-DM instance corresponds to a formula or theory of a logic, and the semantics corresponds to what logicians call a model.</p>
-
-<p>For example, the formula $\forall x. P(x) \Rightarrow Q(x)$ is satisfied in a mathematical model where the relation $P$ denotes a set of elements that is contained in that denoted by $Q$. Here, the goal is to come up with a plausible "intended model" for interpreting PROV-DM instances, where the formulas are assertions in PROV-DM and the individuals are things and agents. This is complicated by the fact that many statements about provenance involve talking about objects that change over time.</p>
-
-<p>The word "world" is used in PROV-DM to talk about the actual state of affairs that the PROV-DM instance describes, which is what I would usually call a "model". The word "model" is used in PROV-DM mainly in the sense of "data model", that is, to talk about what I would otherwise call the syntax of PROV-DM. To avoid confusion with the uses of terms in PROV-DM, I will use "world model" to describe the mathematical structure that corresponds to actual state of affairs, and will try to avoid ambiguous, unqualified uses of the word "model".</p>
+<p>As a starting point, I will assume that we intend the statements made in a PROV-DM instance to be intended to describe one, consistent state of the world, much like a logical formula is said to be satisfied in a mathematical model. That is, I propose an approach similar to that taken in model theory, where the PROV-DM instance corresponds to a formula or theory of a logic, and the semantics corresponds to what logicians call a model.</p>
+
+<p>For example, the formula $\forall x. P(x) \Rightarrow Q(x)$ is satisfied in a mathematical model where the relation $P$ denotes a set of elements that is contained in that denoted by $Q$. Here, the goal is to come up with a plausible "intended model" for interpreting PROV-DM instances, where the formulas are statements in PROV-DM and the individuals are things and agents. This is complicated by the fact that many statements about provenance involve talking about objects that change over time.</p>
+
+<p>The word "world" is used in PROV-DM to talk about the actual state
+of affairs that the PROV-DM instance describes, which is what I would
+usually call a "model". The word "model" is used in PROV-DM mainly in
+the sense of "data model", that is, to talk about what I would
+otherwise call the syntax of PROV-DM. To avoid confusion with the
+uses of terms in PROV-DM, I will use "structure" to describe the
+mathematical structure that corresponds to actual state of affairs.
+We use the term "model" to describe a structure that satisfies a given
+theory; this sense of "model" does not mean "data model".</p>
<h3> Axiomatization and relationship to PROV-CONSTRAINTS </h3>
@@ -1169,7 +1190,8 @@
<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>A lowercase symbol $x,y,...$ on its own denotes an identifier.
+Identifiers may or may not be URIs. Identifiers are viewed as 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>
@@ -1185,9 +1207,12 @@
<section>
<h3> Attributes and Values </h3>
-<p>We assume a set $Attributes$ of attribute labels and a set $Values$ of possible values of attributes.
-</p>
-</section>
+<p>We assume a set $Attributes$ of attribute labels and a set $Values$
+of possible values of attributes. To allow for the fact that some
+attributes have undefined values, we sometimes use the set
+$Value_\bot$, that is, $Values \uplus \{\bot\}$, the set of values
+with an additional element $\bot \notin Values$.
+</p> </section>
<section id="formulas">
<h2>Atomic Formulas</h2>
@@ -1198,7 +1223,7 @@
</p>
$$
\begin{array}{rcl}
- atomic\_formula &{::=}& element\_formula\\
+ atomic\_formula & {::=}& element\_formula\\
& | & relation\_formula\\
& | & auxiliary\_formula\\
element\_formula
@@ -1209,25 +1234,29 @@
&{::=}& wasGeneratedBy(id,e,a,t,attrs)\\
& |& used(id,e,a,t,attrs)\\
& |& wasInvalidatedBy(id,e,a,t,attrs)\\
+ & |& wasStartedBy(id,a_2,e,a_1,attrs)\\
+ & |& wasEndedBy(id,a_2,e,a_1,attrs)\\
& |& wasAssociatedWith(id,ag,act,pl,attrs)\\
& |& wasAssociatedWith(id,ag,act,-,attrs)\\
- & |& wasStartedBy(id,a_2,e,a_1,attrs)\\
- & |& wasEndedBy(id,a_2,e,a_1,attrs)\\
& |& wasAttributedTo(id,e,ag,attrs)\\
& |& actedOnBehalfOf(if,ag_2,ag_1,act,attrs)\\
+ & |& wasInformedBy(id,a_2,a_1,attrs)\\
& |& wasDerivedFrom(id,e_2,e_1,act,g,u,attrs)\\
& |& wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)\\
+& | & wasInfluencedBy(id,x,y,attrs)\\
& |& alternateOf(e_1,e_2)\\
& |& specializationOf(e_1,e_2)\\
+ & | & hadMember(c,e)\\
auxiliary\_formula
- &{::=}& x \prec y\\
+ &{::=}& x = y\\
+ & | & x \prec y\\
& | & x \preceq y\\
& | & notNull(x)\\
& | & typeOf(x,ty)\\
ty &{::=}& entity \\
&|& activity\\
&|& agent\\
-&|& prov:collection\\
+&|& prov:Collection\\
&|& prov:EmptyCollection
\end{array}
$$
@@ -1241,12 +1270,15 @@
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
+ \phi &{::=}& atomic\_formula\\
+& | & True\\
+& | & False\\
+&|& \neg~\phi\\
+ &|& \phi_1 \wedge \phi_2\\
+ &|& \phi_1 \vee \phi_2\\
+ &|& \phi_1 \Rightarrow \phi_2\\
+&|& \forall x. \phi\\
+&|& \exists x. \phi\\
\end{array}
$$
@@ -1261,145 +1293,227 @@
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>
+<h2> Structures and Interpretations </h2>
+
+<section>
<h3> Things </h3>
+<div class="note">TODO: Containment of things / collections? (for hadMember).</div>
<p><em>Things</em> are things in the world. Each thing has a lifetime during which it exists and attributes whose values can change over time.
</p>
-<p>To model this, a world model $W$ includes
+<p>To model this, a structure $W$ includes
</p>
-<ul>
+<div class="component" id="things"><ol>
<li> a set $Things$ of things</li>
<li> a function $lifetime : Things \to Intervals$ from objects to time intervals</li>
<li>a function $value : Things \times Attributes \times Times \to Values_\bot$
</li>
-</ul>
-
-<p>Note that this description does not say what the structure of an object is, only how it may be described in terms of its time interval and attribute values. An object could just be a record of fixed attribute values; it could be a bear; it could be the Royal Society; it could be a transcendental number like $\pi$. All that matters from our point of view is that we know how to map the object to its time interval and attribute mapping.
+</ol>
+</div>
+<p>
+The range of $value$ is the set $Values_\bot$, indicating that $value$
+is essentially a partial function that returns either a value or
+$\bot$. When $value(x,a,t) =
+\bot$, we say that attribute $a$ is undefined for $x$ at time $t$.</p>
+
+<p>Note that this description does not say what the structure of a
+$Thing$ is, only how it may be described in terms of its time interval
+and attribute values. An object could just be a record of fixed
+attribute values; it could be a bear; it could be the Royal Society;
+it could be a transcendental number like $\pi$. All that matters from
+our point of view is that we know how to map the $Thing$ to its time interval and attribute mapping.
</p>
-<p>The range of the $value$ function us $Values_\bot$, that is, $Values \uplus \{\bot\}$, the set of values with an additional element $\bot \notin Values$. When $value(x,a,t) = \bot$, we say that attribute $a$ is undefined for $x$ at time $t$.
-</p>
<p>It is possible for two Things to be indistinguishable by their attribute values and lifetime, but have different identity.
</p>
+
+</section>
+
+<section>
<h3> Objects </h3>
-A <em>Object</em> is described by a time interval and attributes with unchanging values. Objects encompass entities, interactions, and activities.
-
-To model this, a world includes
-
-<ul><li> a set $Objects$
+<p>
+An <em>Object</em> is described by a time interval and attributes with unchanging values. Objects encompass entities, interactions, and activities.
+To model this, a structure includes:
+</p>
+
+<div class="component" id="objects">
+ <ol><li> a set $Objects$
</li><li> a function $lifetime : Objects \to Intervals$ from objects to time intervals
</li><li> a function $value : Objects \times Attributes \to Values_\bot$
-</li></ul>
-
-Intuitively, $lifetime(e)$ is the time interval during which object $e$ exists. The value $value(e,a)$ is the value of attribute $a$ during the object's lifetime.
-
-As with <em>Things</em>, the range of $value$ includes the special undefined value $\bot$, making $value$ effectively a partial function. It is also possible to have two different objects that are indistinguishable by their attributes and time intervals. Objects are not things, and the sets of $Objects$ and $Things$ are disjoint; however, certain objects, namely entities, are linked to things.
-
+</li></ol>
+</div>
+
+<p>Intuitively, $lifetime(e)$ is the time interval during which object $e$ exists. The value $value(e,a)$ is the value of attribute $a$ during the object's lifetime.
+</p>
+
+<p>As with <em>Things</em>, the range of $value$ includes the special undefined value $\bot$, making $value$ effectively a partial function. It is also possible to have two different objects that are indistinguishable by their attributes and time intervals. Objects are not things, and the sets of $Objects$ and $Things$ are disjoint; however, certain objects, namely entities, are linked to things.
+
+</p>
+<section>
<h4> Entities </h4>
An <em>entity</em> is a kind of object that describes a time-slice of a thing, during which some of the thing's attributes are fixed. We assume:
-<ul><li> a set $Entities \subseteq Objects$ of entities, disjoint from $Activities$ and $Events$ below.
+<div class="component" id="entities">
+ <ol><li> a set $Entities \subseteq Objects$ of entities, disjoint from $Activities$ and $Events$ below.
</li><li> a function $thingOf : Entities \to Things$ that associates each Entity with a Thing, such that for each $t \in lifetime(obj)$, and for each attribute $a$ such that $value(obj,a) \neq \bot$, we have $value(obj,a) = value(thingOf(obj),a,t)$.
</li><li> $lifetime(e) \subseteq lifetime(t)$.
-</li></ul>
-
-<div class="remark"><p> Although both entities and things can have undefined attribute values, their meaning is slightly different: for a thing, $value(x,a,t) = \bot$ means that the attribute $a$ has no value at time $t$, whereas for an entity, $value(x,a) = \bot$ only means that the entity does not record a fixed value for $a$. This does not imply that $value(thingOf(e),a,t) = \bot$ when $t \in lifetime(e)$. In particular, if the $value(x,a,t)$ has multiple values during the lifetime of $e$, then $value(e,a)$ <b>must</b> be $\bot$, since assigning a value to $value(e,a)$ would violate condition (3) above.
+</li></ol>
+</div>
+
+<div class="remark"><p> Although both entities and things can have undefined attribute values, their meaning is slightly different: for a thing, $value(x,a,t) = \bot$ means that the attribute $a$ has no value at time $t$, whereas for an entity, $value(x,a) = \bot$ only means that the entity does not record a fixed value for $a$. This does not imply that $value(thingOf(e),a,t) = \bot$ when $t \in lifetime(e)$. In particular, if the $value(x,a,t)$ has multiple values during the lifetime of $e$, then $value(e,a)$ <b>must</b> be $\bot$, since assigning a value to $value(e,a)$ would violate condition (2) above.
</p>
</div>
-
+
+<section>
<h5> Plans </h5>
-<p>We identify a specific subset of the entities called <em>plans</em>, $Plans \subseteq Entities$.
-</p>
-<h4> Agents </h4>
-
-<p>An agent is an entity that can act, by controlling, starting, ending, or participating in activities. Agents can act on behalf of other agents. We introduce:
-</p>
-* a set $Agents \subseteq Objects$ of agents.
-
+<p>We identify a specific subset of the entities called
+ <em>plans</em>:
+<div class="component" id="plans">
+ <p> A set $Plans \subseteq Entities$ of plans.</p>
+ </div>
+</p></section>
+
+ </section>
+
+ <section>
<h4> Actvities </h4>
<p>An <em>activity</em> is an object that encompasses a set of events. We introduce
</p>
-* a set $Activities \subseteq Objects$ of activities, disjoint from $Entities$ and $Events$
-
-
-<h4> Interactions </h4>
-
-<p>We consider a $Interactions \subseteq Objects$ which are split into <em>Events</em> between entities and activities, <em>Associations</em> between agents and activities, and <em>Derivations</em> that describe chains of generation and usage steps. (The first two sets may overlap.) Interactions are disjoint from entities, activities and agents.
+<div class="component" id="activities">
+ <ol><li>A set $Activities \subseteq Objects$ of activities.</li>
+ <li> Activities are disjoint from Entities: $Entities\cap Activities
+ = \emptyset$.</li>
+ </ol>
+</section>
+
+ <section>
+<h4> Agents </h4>
+
+<p>An agent is an object that can act, by controlling, starting,
+ ending, or participating in activities. Agents can act on behalf of
+ other agents. An agent can be an entity, an activity, or neither; an
+ agent cannot be both entity and activity because the sets of
+ entities and activities are disjoint. We introduce:
</p>
-<ul><li> $Interactions = (Events \cup Associations) \cup Derivations \subseteq Objects$
-</li><li> $(Events \cup Associations) \cap Derivations = \emptyset$
-</li><li> $Interactions \cap (Entities \cup Activities \cup Agents) = \emptyset$
-</li></ul>
-
+<div class="component" id="agents">
+ <p>A set $Agents \subseteq Objects$ of agents.</p>
+ </div>
+</section>
+
+
+<section>
+<h4> Interactions </h4>
+
+<p>We consider a $Interactions \subseteq Objects$ which are split into
+ <em>Events</em> connecting entities and activities,
+ <em>Associations</em> between agents and activities,
+ <em>Communications</em> between pairs of activities,
+ <em>Delegations</em> between pairs of agents, and <em>Derivations</em> that describe chains of generation and usage steps. (The first two sets may overlap.) Interactions are disjoint from entities, activities and agents.
+</p>
+<div class="component" id="interactions">
+ <ol><li> A set $Interactions = Events \cup Associations \cup
+ Communications \cup Delegations \cup Derivations \subseteq Objects$
+</li>
+<li> A function $type: Interactions \to
+ \{start,end,usage,generation,invalidation,derivation,version,quotation,primarySource,attribution,delegation\}$.
+</li>
+<li> The sets $Events$, $Associations$, $Communications$, $Delegations$
+ and $Derivations$ are all disjoint.
+</li><li> Interactions are disjoint from entities, agents and
+activities: $Interactions \cap (Entities \cup Activities \cup Agents) = \emptyset$
+</li></ol>
+</div>
+
+<section>
<h5> Events </h5>
-<p>An <em>Event</em> is an interaction whose lifetime is a single time instant, and relates an activity to an entity (which could be an agent). Events have types including usage, generation, starting and ending (possibly more may be added such as destruction/invalidation of an entity). Events are instantaneous. We introduce:
+<p>An <em>Event</em> is an interaction whose lifetime is a single time
+instant, and relates an activity to an entity (which could be an
+agent). Events have types including usage, generation, invalidation, starting and ending. Events are instantaneous. We introduce:
</p>
-<div class="formalism">
-<ul><li> A set $Events \subseteq Interactions$ of events.
+<div class="component" id="events">
+<ol><li> A set $Events \subseteq Interactions$ of events, such that
+ $type(evt) \in \{start,end,generation,usage,invalidation\}$ if and
+ only of $evt \in Events$.
</li><li> A function $time : Events \to Times$ giving the time of each event; i.e. $lifetime(evt) = \{time(t)\}$.
</li><li> The derived ordering on events given by $evt_1 \leq evt_2 \iff time(evt_1) \leq time(evt_2)$
-</li><li> A function $type: Events \to \{start,end,use,generate\}$ such that Events have types in $\{start,end,use,generate\}$.
-</li></ul>
+</li></ol>
</div>
+</section>
+<section>
+
<h5> Associations </h5>
<p>An <em>Association</em> is an interaction relating an agent to an activity. Associations can overlap with events; for example, a start event is also an association. To model associations, we introduce:
</p>
-<div class="formalism">
- <p>A set $Associations \subseteq Interactions$, such that every event $evt \in Events$ that is a start or end event is also an association. That is, $type(evt) \in \{start,end\}$ implies $evt \in Associations$
+<div class="component" id="associations">
+ <p>A set $Associations \subseteq Interactions$, such that
+ $type(assoc) = association$ if and only if $assoc \in Associations$.
</p>
</div>
<p>Associations are used below in the $ActsFor$ and $AssociatedWith$ relations.
-<b>TODO: Add types for association or delegation?</b>
-</p>
-<h5> Derivations </h5>
+
+
+</section>
+ <section>
+ <h5>Communications</h5>
+ <div class="note">TODO</div>
+
+</section>
+ <section>
+ <h5>Delegations</h5>
+ <div class="note">TODO</div>
+</section>
+ <section>
+
+ <h5> Derivations </h5>
<p>A <em>Derivation</em> is an interaction chaining one or more generation and use steps. Derivations can also carry attributes, so we introduce an explicit kind of interaction for them that can carry attributes.
</p>
-<div class="formalism">
-<p> * A set $Derivations \subseteq Interactions$, disjoint from $Events \cup Associations$.
+<div class="component" id="derivations">
+<p> A set $Derivations \subseteq Interactions$, such that
+ $type(deriv) \in \{derivation, version, primarySource,quotation\}$
+ if and only if $deriv \in Derivations$.
</p></div>
<p>See below for the associated derivation path and DerivedFrom relation.
</p>
+</section>
+</section>
+</section>
+<section>
+
<h3> Relations </h3>
<h4> Simple relations </h4>
-<p>The entities, interactions, and activities in a world model are related in the following ways:
+<p>The entities, interactions, and activities in a structure are related in the following ways:
</p>
-<ul><li> A relation $Used \subseteq Events \times Entities$ saying when an event used an entity. An event can use at most one entity, and if $(evt,e)\in Used$ then $time(evt) \in lifetime(e)$ and $type(g) = use$ must hold.
+<ol><li> A relation $Used \subseteq Events \times Entities$ saying when an event used an entity. An event can use at most one entity, and if $(evt,e)\in Used$ then $time(evt) \in lifetime(e)$ and $type(g) = use$ must hold.
</li><li> A relation $Generated \subseteq Events \times Entities$ saying when an event generated an entity. An event can generate at most one entity, and if $(evt,e)\in Generated$ then $min(lifetime(e)) = time(evt)$ and $type(g) = generation$ must hold.
</li><li> A relation $Invalidated \subseteq Events \times Entities$ saying when an event invalidated an entity. An event can invalidate at most one entity, and if $(evt,e)\in Invalidated$ then $min(lifetime(e)) = time(evt)$ and $type(g) = invalidation$ must hold.
</li><li> A relation $EventActivity \subseteq Events \times Activities$ associating activities with events, such that $(act,evt) \in EventActivity$ implies $time(evt) \in lifetime(act)$.
-</li><li> A relation $AssociatedWith \subseteq Association \times Agents \times Activities \times Plans^?$ indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan.
-</li><li> A relation $ActsFor \subseteq Agents \times Agents \times Activities$ indicating when one agent acts on behalf of another with respect to a given activity.
-</li></ul>
-
+</li><li> A relation $AssociatedWith \subseteq Association \times Agents \times Activities \times Plans_\bot$ indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan.
+</li><li> A relation $ActsFor \subseteq Delegations \times Agents \times Agents \times Activities$ indicating when one agent acts on behalf of another with respect to a given activity.
+</li></ol>
+
+<div class="note">
+ TODO: Communication, start, end relations
+ </div>
+
+<section>
<h4> Derivation paths and DerivedFrom </h4>
<p>Recall that above we introduced a subset of interactions called <em>Derivations</em>. These identify <em>paths</em> of the form </p>
@@ -1415,65 +1529,134 @@
Events \cdot Entities)^+$$
<p>with the constraints that for each derivation path:
</p>
-<ol>
+<ul>
<li>for each substring $ent\cdot g \cdot act$ we have $(g,ent) \in Generated$ and $(g,act) \in EventActivities$, and
</li>
<li>for each substring $act \cdot u \cdot ent$ we have $(u,ent) \in Used$ and $(u,act) \in EventActivities$.
and we use this language to give meaning to derivations:
</li>
-</ol>
+</ul>
<p>We also consider a function $derivedFrom : Derivations \to
DerivationPaths$ linking each derivation to its path.</p>
<div class="remark">The reason why we need paths and not just individual derivation steps is that imprecise wasDerivedFrom formulas can represent multiple derivation steps.</div>
-
+</section>
+</section>
+
+<section>
<h3> Putting it all together </h3>
-<p>A <em>world model</em> W is a structure containing all of the above described data. If we need to talk about the objects or relations of more than one world model then we may write $W_1.Objects$; otherwise, to decrease notational clutter, when we consider a fixed world model then the names of the sets, relations and functions above refer to the components of that model.
+<p>A <em>structure</em> $W$ is a structure containing all of the above
+described data. If we need to talk about the objects or relations of
+more than one structure then we may write $W_1.Objects$, $W_1.Things$,
+etc.; otherwise, to
+decrease notational clutter, when we consider a fixed structure then the names of the sets, relations and functions above refer to the components of that model.
</p>
<p><b>TODO: List the components.</b>
</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>.
+ Thus, we consider interpretations as follows:
+An interpretation is a function $\rho : Identifiers \to Objects$ describing
+which object is the target of each identifier. The mapping from identifiers to objects may <b>not</b> change over time.
+</p>
+</section>
+
+</section>
<section id="semantics">
<h2> Semantics </h2>
-<p>In what follows, let $W$ be a fixed world model with the associated sets and relations discussed in the previous section, and let $I$ be an interpretation of identifiers as objects in $W$.
-</p>
-<p>The annotations [WF] refer to well-formedness constraints that correspond to typing constraints.
-</p>
-
-<h3> Satisfaction </h3>
-
-<p>Consider an atomic formula $\phi$, a world $W$ and an interpretation $I$. We define notation $W,I \models \phi$ which means that $\phi$ is satisfied in $W,I$. For basic assertions, the definition of the satisfaction relation is given in the next few subsections. For a conjunction of assertions $\phi_1,\ldots,\phi_n$ we write $W,I \models \phi_1,\ldots,\phi_n$ to indicate that $W,I \models \phi_1$ and ... and $W,I \models \phi_n$ hold.
-</p>
-<p><b>TODO: Satisfiability of additional formulas to explain constraints/inferences</b>
+<p>In what follows, let $W$ be a fixed structure with the associated sets and relations discussed in the previous section, and let $I$ be an interpretation of identifiers as objects in $W$.
+The annotations [WF] refer to well-formedness constraints that correspond to typing constraints.
</p>
-<h3> Attribute matching </h3>
-
-
-<p>We say that an object $obj$ matches attributes $[attr_1=val_1,...]$ in world $W$ provided:
+
+<section>
+<h3> Satisfaction </h3>
+
+<p>Consider a formula $\phi$, a structure $W$ and an interpretation
+ $I$.
+We define notation $W,\rho \models \phi$ which means that $\phi$ is
+ satisfied in $W,\rho$. For atomic formulas, the definition of the
+ satisfaction relation is given in the next few subsections. We give
+ the standard definition of the semantics of the other formulas:
</p>
-<ul><li> for each attribute $attr_i$, we have $W.value(obj,attr_i) = val_i$.
-This is sometimes abbreviated as: $match(W,obj,attrs)$
-</li></ul>
-
-<h3> Semantics of Element Records </h3>
-
-<h4> Entity Records </h4>
+
+<div class="formalism" id="first-order-logic">
+<ol>
+ <li>$W,\rho \models True$ always holds.</li>
+ <li>$W,\rho \models False$ never holds.</li>
+ <li>$W,\rho \models \neg \phi$ holds if and only if $W,\rho \models
+ \phi$ does not hold.</li>
+ <li>$W,\rho \models \phi \wedge \psi$ holds if and only if $W,\rho \models
+ \phi$ and $W,i\models \psi$.</li>
+ <li>$W,\rho \models \phi \vee \psi$ holds if either $W,\rho \models \phi$
+ or $W,\rho \models \psi$ holds.</li>
+ <li>$W,\rho \models \phi \Rightarrow \psi$ holds if $W,\rho \models \phi$
+ implies $W,\rho \models \psi$.</li>
+ <li>$W,\rho \models \exists x. \phi$ holds if there exists some $obj \in
+ Objects$ such that $W,\rho[x:=obj] \models \phi$.</li>
+ <li>$W,\rho \models \forall x. \phi$ holds if there for every $obj \in
+ Objects$ we have $W,\rho[x:=obj] \models \phi$.</li>
+ </div>
+
+<div class="remark">
+ <p>In the semantics above, note that the domain of quantification is
+ the set of $Objects$; that is, quantifiers range over entities,
+ activities, agents, or interactions (which are in turn further
+ subdivided into types of interactions). $Things$ and relations
+ cannot be referenced directly by identifiers.
+</p>
+ </div>
+
+ <div class="remark">
+ <p>A PROV instance $I$ consists of a set of statements, each of
+ which can be translated to an atomic formula following the
+ definitional rules in PROV-CONSTRAINTS, possibly by introducing
+ fresh existential variables. Thus, we can view an
+ instance $I$ as a set of atomic formulas $\{\phi_1,\ldots,\phi_n\}$, or equivalently a
+ single formula $\exists x_1,\ldots,x_k.~\phi_1 \wedge \cdots
+ \wedge \phi_n$, where $x_1,\ldots,x_k$ are the existential
+ variables of $I$.
+ </p>
+ </div>
+
+</section>
+ <section>
+
+<h3> Attribute matching </h3>
+
+
+<p>We say that an object $obj$ matches attributes $[attr_1=val_1,...]$ in structure $W$ provided:
+for each attribute $attr_i$, we have $W.value(obj,attr_i) = val_i$.
+This is sometimes abbreviated as: $match(W,obj,attrs)$.
+</p>
+
+</section>
+
+<section>
+<h3> Semantics of Element Formulas </h3>
+
+<section>
+
+<h4> Entity </h4>
<p>An entity formula is of the form $entity(id,attrs)$ where $id$ denotes an entity.
</p>
-<p>Entity assertions $entity(id,attrs)$ can be interpreted as follows:
+<p>Entity formulas $entity(id,attrs)$ can be interpreted as follows:
</p>
<div class="formalism">
- $W,I \models entity(id,attrs)$ if and only if:
+ <p>$W,\rho \models entity(id,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes an entity $ent = I(id) \in Entities$
+<li>[WF] $id$ denotes an entity $ent = \rho(id) \in Entities$
</li>
<li>the attributes match: $match(W,ent, attrs)$.
</li>
</ol>
+
</div>
<p>For example, the following formulas both hold if $x$ denotes an entity $e$ such that $value(e,a) = 4, value(e,b) = 5, value(e,c) = 6$ hold:
@@ -1481,15 +1664,21 @@
entity(x,[a=4,b=5])
entity(x,[a=4,b=5,c=6])
</pre>
-
-<h4> Activity Records </h4>
-
-<p>An activity record is of the form $activity(id,st,et,attrs)$ where $id$ is a identifier referring to the activity, $st$ is a start time and $et$ is an end time.
+ </section>
+<section>
+
+<h4> Activity </h4>
+
+<p>An activity formula is of the form $activity(id,st,et,attrs)$
+where $id$ is a identifier referring to the activity, $st$ is a start
+time and $et$ is an end time, and $attrs$ are the attributes of
+activity $id$.
</p>
<div class="formalism">
- <p>We say that $W,I \models activity(id,st,et,attrs)$ if and only if:</p>
+ <p>$W,\rho \models activity(id,st,et,attrs)$
+ holds if and only if:</p>
<ol>
-<li>[WF] The identifier $id$ maps to an activity $act = I(id) \in Activities$
+<li>[WF] The identifier $id$ maps to an activity $act = \rho(id) \in Activities$
</li>
<li>If $st$ is specified then it is equal to the start time of the activity, that is: $min(lifetime(id)) = st$
</li>
@@ -1499,39 +1688,44 @@
</li>
</ol>
</div>
-
-<h4> Agent Records </h4>
+</section>
+<section>
+
+<h4> Agent </h4>
<p>An agent formula is of the form $agent(id,attrs)$ where $id$ denotes the agent and $attrs$ describes additional attributes.
</p>
<div class="formalism">
- <p>Agent assertions $agent(id,attrs)$ can be interpreted as follows:
- $W,I \models agent(id,attrs)$ if and only if:
+ <p>$W,\rho \models agent(id,attrs)$ holds if and only if:
</p>
<ol>
- <li>[WF] $id$ denotes an agent $ag = I(id) \in Agents$
+ <li>[WF] $id$ denotes an agent $ag = \rho(id) \in Agents$
</li>
<li>The attributes match: $match(W,ag,attrs)$.
</li>
</ol>
</div>
-
+</section>
+</section>
+
+<section>
<h3> Semantics of Relations </h3>
-<h4> Entity-Activity </h4>
-
+
+<section>
<h5> Generation </h5>
-<p>The generation assertion is of the form $wasGeneratedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
+<p>The generation formula is of the form $wasGeneratedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
</p>
<div class="formalism">
- $W,I \models wasGeneratedBy(id,e,a,t,attrs)$ if and only if:
+ <p>A generation formula $W,\rho \models
+ wasGeneratedBy(id,e,a,t,attrs)$ holds if and only if:</a>
<ol>
-<li>[WF] The identifier $id$ denotes an event $evt = I(id) \in Events$
+<li>[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$
</li>
-<li>[WF] The identifier $e$ denotes an entity $ent = I(e) \in Entities$
+<li>[WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$
</li>
-<li>[WF] The identifier $a$ denotes an activity $act = I(a) \in Activities$.
+<li>[WF] The identifier $a$ denotes an activity $act = \rho(a) \in Activities$.
</li>
<li>The event $evt$ is involved in $act$, that is, such that $(evt,act) \in EventActivities$.
</li>
@@ -1546,17 +1740,20 @@
</ol>
</div>
+</section>
+<section>
<h5> Use </h5>
-The use assertion is of the form $used(id,a,e,t,attrs)$ where $id$ denotes an event, $a$ is an activity identifier, $e$ is an object identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
-
-<div class="formalism"> $W,I \models used(id,a,e,t,attrs)$ if and only if:
+<p>The use formula is of the form $used(id,a,e,t,attrs)$ where $id$ denotes an event, $a$ is an activity identifier, $e$ is an object identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
+</p>
+<div class="formalism">
+ <p>$W,\rho \models used(id,a,e,t,attrs)$ holds if and only if:</p>
</li>
-<li>[WF] The identifier $id$ denotes an event $evt = I(id) \in Events$
+<li>[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$
</li>
-<li>[WF] The identifier $a$ denotes an activity $act = I(id) \in Activities$
+<li>[WF] The identifier $a$ denotes an activity $act = \rho(id) \in Activities$
</li>
-<li>[WF] The identifier $e$ denotes an entity $ent = I(e) \in Entities$
+<li>[WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$
</li>
<li>The event $evt$ is part of $act$, i.e. $(evt,act) \in EventActivities$.
</li>
@@ -1569,19 +1766,22 @@
<li>The attribute values match: $match(W,evt,attrs)$
</li></ol></div>
+</section>
+<section>
<h5> Invalidation </h5>
-The invalidation assertion is of the form $wasInvalidatedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
-
-<div class="formalism"> $W,I \models wasInvalidatedBy(id,e,a,t,attrs)$ if and only if:
+<p>The invalidation formula is of the form $wasInvalidatedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.</p>
+
+<div class="formalism"> <p>An invaliation formula $W,\rho \models
+ wasInvalidatedBy(id,e,a,t,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] The identifier $id$ denotes an event $evt = I(id) \in Events$
+<li>[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$
</li>
-<li>[WF] The identifier $e$ denotes an entity $ent = I(e) \in Entities$
+<li>[WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$
</li>
-<li>[WF] The identifier $a$ denotes an activity $act = I(a) \in Activities$.
+<li>[WF] The identifier $a$ denotes an activity $act = \rho(a) \in Activities$.
</li>
-<li>The event $evt$ is involved in $act$, that is, such that $(evt,act) \in EventActivities$.
+<li>The event $evt$ is involved in $act$, that is, $(evt,act) \in EventActivities$.
</li>
<li>The type of $evt$ is $invalidation$, i.e. $type(evt) = invalidation$
</li>
@@ -1591,158 +1791,200 @@
</li>
<li>The attribute values match: $match(W,evt,attrs)$
</li></ol></div>
-<h4> Agent-Activity </h4>
-
-<h5> Association Records </h5>
-
-An association record has the form $wasAssociatedWith(id,a,ag,pl,attrs)$.
-
-<div class="formalism"> $W,I \models wasAssociatedWith(id,a,ag,pl,attrs)$ holds if and only if:
+</section>
+
+<section>
+
+<h5> Association </h5>
+
+<p>An association formula has the form $wasAssociatedWith(id,a,ag,pl,attrs)$.</p>
+
+<div class="formalism"><p>
+ $W,\rho \models wasAssociatedWith(id,a,ag,pl,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $assoc$ denotes an association $assoc = I(id) \in Associations$.
+<li>[WF] $assoc$ denotes an association $assoc = \rho(id) \in Associations$.
</li>
-<li>[WF] $a$ denotes an activity $act = I(a) \in Activities$.
+<li>[WF] $a$ denotes an activity $act = \rho(a) \in Activities$.
</li>
-<li>[WF] $ag$ denotes an agent $agent = I(ag) \in Agents$.
+<li>[WF] $ag$ denotes an agent $agent = \rho(ag) \in Agents$.
</li>
-<li>[WF] $pl$ is either the placeholder $-$ or denotes a plan $plan=I(pl) \in Plans$.
+<li>[WF] $pl$ is either the placeholder $-$ or denotes a plan $plan=\rho(pl) \in Plans$.
</li>
<li>The association associates the agent with the activity and plan, i.e. $(assoc,agent,act,plan) \in AssociatedWith$.
</li>
<li>The attributes match: $match(W,assoc,attrs)$.
</li></ol></div>
-
-<h5> Start Records </h5>
-
-A start record $wasStartedBy(id,a2,e,a1,attrs)$ is interpreted as follows:
-
-<div class="formalism"> $W,I \models wasStartedBy(id,a2,e,a1,attrs)$ holds if and only if:
+</section>
+<section>
+<h5> Start Formulas </h5>
+
+<p>A start formula $wasStartedBy(id,a_2,e,a_1,attrs)$ is interpreted as follows:</p>
+
+<div class="formalism">
+ <p>$W,\rho \models wasStartedBy(id,a_2,e,a_1,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes an event $evt = I(id) \in Events$
+<li>[WF] $id$ denotes an event $evt = \rho(id) \in Events$
</li>
-<li>[WF] $a2$ denotes an activity $act2 = I(a2)$
+<li>[WF] $a_2$ denotes an activity $act_2 = \rho(a_2)$
</li>
-<li>[WF] $e$ denotes an entity $ent = I(e)$
+<li>[WF] $e$ denotes an entity $ent = \rho(e)$
</li>
-<li>[WF] $a1$ denotes an activity $act1 = I(a1)$
+<li>[WF] $a_1$ denotes an activity $act_1 = \rho(a_1)$
</li>
<li>The event $evt$ has type $start$, i.e. $type(evt) = start$.
</li>
-<li>The event happened at the start of $act2$, that is, $(act2,evt) \in ActivitiesEvents$, and $min(lifetime(act2)) = time(evt)$.
+<li>The event happened at the start of $act_2$, that is, $(act_2,evt) \in ActivitiesEvents$, and $min(lifetime(act_2)) = time(evt)$.
</li>
-<li>The event happened during $act1$, that is, $(act1,evt) \in ActivitiesEvents$.
+<li>The event happened during $act_1$, that is, $(act_1,evt) \in ActivitiesEvents$.
</li>
<li>The attributes match: $match(W,evt,attrs)$.
</li></ol></div>
-
-<h5> End Records </h5>
-
-An activity end record $wasEndedBy(id,a2,e,a1,attrs)$ is interpreted as follows:
+</section>
+<section>
+<h5> End </h5>
+
+<p>An activity end formula $wasEndedBy(id,a_2,e,a_1,attrs)$ is interpreted as follows:</p>
<div class="formalism">
- $W,I \models wasEndedBy(id,a2,e,a1,attrs)$ holds if and only if:
+<p>
+ $W,\rho \models wasEndedBy(id,a_2,e,a_1,attrs)$ holds if and only
+ if:</p>
+
<ol>
- <li>[WF] $id$ denotes an event $evt = I(id) \in Events$</li>
-<li> [WF] $a2$ denotes an activity $act2 = I(a2)$</li>
-<li> [WF] $e$ denotes an entity $ent = I(e)$</li>
-<li>[WF] $a1$ denotes an activity $act1 = I(a1)$</li>
+ <li>[WF] $id$ denotes an event $evt = \rho(id) \in Events$</li>
+<li> [WF] $a_2$ denotes an activity $act_2 = \rho(a_2)$</li>
+<li> [WF] $e$ denotes an entity $ent = \rho(e)$</li>
+<li>[WF] $a_1$ denotes an activity $act_1 = \rho(a_1)$</li>
<li>The event $evt$ has type $end$, i.e. $type(evt) = end$.</li>
-<li>The event happened at the end of $act2$, that is, $(act2,evt) \in ActivitiesEvents$, and $max(lifetime(act2)) = time(evt)$.</li>
-<li>The event happened during $act1$, that is, $(act1,evt) \in ActivitiesEvents$.</li>
+<li>The event happened at the end of $act_2$, that is, $(act_2,evt) \in ActivitiesEvents$, and $max(lifetime(act_2)) = time(evt)$.</li>
+<li>The event happened during $act_1$, that is, $(act_1,evt) \in ActivitiesEvents$.</li>
<li>The attributes match: $match(W,evt,attrs)$.</li>
-</ol></div>
-
-<h4> Agent-Entity </h4>
-
-<h5> Attribution Records </h5>
-
-An attribution record $wasAttributedTo(id,e,ag,attrs)$ is interpreted as follows:
-
-<div class="formalism"> $W,I \models wasAttributedTo(id,e,ag,attrs)$ holds if and only if:
+</ol>
+</div>
+</section>
+
+<section>
+<h5> Attribution </h5>
+
+<p>
+An attribution formula $wasAttributedTo(id,e,ag,attrs)$ is interpreted as follows:
+</p>
+<div class="formalism">
+ <p>
+ $W,\rho \models wasAttributedTo(id,e,ag,attrs)$
+ holds if and only if:
+ </p>
<ol>
-<li>[WF] $id$ denotes an event $evt = I(id)$ that is also an association $evt \in Associations$
-</li>
-<li>[WF] $e$ denotes an entity $ent = I(e)$
+<li>[WF] $id$ denotes an association $assoc = \rho(id) \in Associations$
</li>
-<li>[WF] $ag$ denotes an agent $agent = I(ag)$
+<li>[WF] $e$ denotes an entity $ent = \rho(e)$
</li>
-<li>The event $evt$ has type $attribution$, i.e. $type(evt) = attribution$.
+<li>[WF] $ag$ denotes an agent $agent = \rho(ag)$
</li>
-<li>The entity was attributed to the agent, i.e. $(id,ent,ag) \in AttributedTo$
+<li>The entity was attributed to the agent, i.e. $(assoc,ent,agent) \in AttributedTo$
</li>
<li>The attributes match: $match(W,evt,attrs)$.
-</li></ol></div>
-
-<h4> Agent-Agent </h4>
+</li></ol>
+</div>
+</section>
+
+<section>
+<h4>Communication</h4>
+<div class="note">TODO: Communication</div>
+
+</section>
+
+
+<section>
<h5> Responsibility </h5>
-The $actedOnBehalfOf(id,ag2,ag1,act,attrs)$ relation is interpreted using the $ActsFor$ relation as follows:
-
-<div class="formalism"> $W,I \models actedOnBehalfOf(id,ag2,ag1,act,attrs)$ holds if and only if:
+<p>The $actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$ relation is interpreted using the $ActsFor$ relation as follows:</p>
+
+<div class="formalism">
+ <p>
+ $W,\rho \models actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes an association $assoc=I(id) \in Associations$ that is an association interaction, and $type(id) = responsibility$.
+<li>[WF] $id$ denotes an association $deleg=\rho(id) \in Delegations$.
</li>
-<li>[WF] $a$ denotes an activity $act=I(a) \in Activities$ is an activity.
+<li>[WF] $a$ denotes an activity $act=\rho(a) \in Activities$ is an activity.
</li>
-<li>[WF] $ag1,ag2$ denote agents $agent1=I(ag1), agent2=I(ag2) \in Agents$ are agents.
+<li>[WF] $ag_1,ag_2$ denote agents $agent_1=\rho(ag_1), agent_2=\rho(ag_2) \in Agents$ are agents.
</li>
-<li>The agent $agent2$ acts for the agent $agent1$ with respect to the activity $act$, i.e. $(agent2,agent1,act) \in ActsFor$.
-</li>
-<li>[Redundant?] The association $id$ associates both agents with the activity, i.e. $(assoc,agent1,act),(assoc,agent2,act) \in AssociatedWith$.
+<li>The agent $agent_2$ acts for the agent $agent_1$ with respect to the activity $act$, i.e. $(deleg,agent_2,agent_1,act) \in ActsFor$.
</li>
<li>The attributes match: $match(W,assoc,attrs)$.
</li></ol></div>
-
-<h4> Entity-Entity </h4>
+</section>
+
+
+<section>
<h5> Derivation </h5>
+<section>
<h6> Precise </h6>
-<p>A precise derivation record has the form $wasDerivedFrom(id,e2,e1,a,g,u,attrs)$.
+<p>A precise derivation formula has the form $wasDerivedFrom(id,e_2,e_1,a,g,u,attrs)$.
</p>
-<div class="formalism"> $W,I \models wasDerivedFrom(id,e2,e1,act,g,u,attrs)$ if and only if:
+<div class="formalism">
+ <p>$W,\rho \models wasDerivedFrom(id,e_2,e_1,act,g,u,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes a derivation $deriv = I(id) \in Derivations$
+<li>[WF] $id$ denotes a derivation $deriv = \rho(id) \in Derivations$
</li>
-<li>[WF] $e1,e2$ denote entities $ent1 = I(e1), ent2=I(e2) \in Entities$
-</li>
-<li>[WF] $a$ denotes an activity $act = I(a) \in Activities$
+<li>[WF] $e_1,e_2$ denote entities $ent_1 = \rho(e_1), ent_2=\rho(e_2) \in Entities$
</li>
-<li>[WF] $g$ denotes a generation event $gen = I(g) \in Events$ and $type(I(g)) = generation$
+<li>[WF] $a$ denotes an activity $act = \rho(a) \in Activities$
</li>
-<li>[WF] $u$ denotes a use event $I(u) \in Events$ and $type(I(u)) = use$
+<li>[WF] $g$ denotes a generation event $gen = \rho(g) \in Events$ and $type(\rho(g)) = generation$
</li>
-<li>The derivation denotes a valid one-step derivation $derivedFrom(deriv) = I(e2) \cdot I(g) \cdot I(act) \cdot I(u) \cdot I(e1)$
+<li>[WF] $u$ denotes a use event $\rho(u) \in Events$ and $type(\rho(u)) = use$
+</li>
+<li>The derivation denotes a valid one-step derivation $derivedFrom(deriv) = \rho(e_2) \cdot \rho(g) \cdot \rho(act) \cdot \rho(u) \cdot \rho(e_1)$
</li>
<li>The attribute values match: $match(W,deriv,attrs)$.</li>
</ol>
</div>
+</section>
+<section>
<h6> Imprecise </h6>
<p>
-An imprecise derivation record has the form $wasDerivedFrom(id,e2,e1,-,-,-,attrs)$.</p>
-
-<div class="formalism"> $W,I \models wasDerivedFrom(id,e2,e1,-,-,-,attrs)$ if and only if there exists $path \in DerivationPaths$ such that:
+An imprecise derivation formula has the form $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$.</p>
+
+<div class="formalism">
+ <p>$W,\rho \models wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ holds if and only if:</p>
<ol>
-<li>[WF] $id$ denotes a derivation $deriv = I(id) \in Derivations$
+<li>[WF] $id$ denotes a derivation $deriv = \rho(id) \in Derivations$
</li>
-<li>[WF] $e1,e2$ denote entities $ent1 = I(e1), ent2=I(e2) \in Entities$
+<li>[WF] $e_1,e_2$ denote entities $ent_1 = \rho(e_1), ent_2=\rho(e_2) \in Entities$
</li>
-<li>$derivedFrom(deriv)= ent2 \cdot w \cdot ent1$ for some $w$
+<li>$derivedFrom(deriv)= ent_2 \cdot w \cdot ent_1$ for some $w$
</li>
<li>The attribute values match: $match(W,deriv,attrs)$.
</li></ol></div>
-
-
+</section>
+</section>
+
+ <section>
+ <h3>Influence</h3>
+
+ <div class="note">TODO: Define influence semantics.</div>
+
+ </section>
+
+<section>
<h5> Specialization </h5>
-<p>The $specializationOf(e1,e2)$ relation indicates when one entity record presents more specific aspects of another.
+<p>The $specializationOf(e_1,e_2)$ relation indicates when one entity formula presents more specific aspects of another.
</p>
-<div class="formalism"> $W,I \models specializationOf(e1,e2)$ if and only if:
+<div class="formalism"> <p>
+ $W,\rho \models specializationOf(e_1,e_2)$ holds if and only if:</p>
<ol>
-<li>[WF] Both $e1$ and $e2$ are entity identifiers, denoting $ent_1 = I(e1) \in Entities$ and $ent_2 = I(e2) \in Entities$.
+<li>[WF] Both $e_1$ and $e_2$ are entity identifiers, denoting
+ distinct entities $ent_1
+ = \rho(e_1) \in Entities$ and $ent_2 = \rho(e_2) \in Entities$,
+ where $ent_1 \neq ent_2$.
</li>
<li>The two Entities refer to the same Thing, that is, $thingOf(ent_1) = thingOf(ent_2)$.
</li>
@@ -1753,48 +1995,144 @@
<p>The second criterion says that the two Entities present aspects of the same Thing. Note that the third criterion allows $obj_1$ and $obj_2$ to have the same lifetime (or that of $obj_2$ can be larger). The last criterion allows $obj_1$ to have more defined attributes than $obj_2$, but they must agree on the attributes defined by $obj_2$.
</p>
-<div class="remark">
- <p>There has been discussion whether $specializationOf$ is <em>transitive</em> and/or<em>anti-symmetric</em>:</p>
-<ul><li>
- Transitivity: If $specializationOf(a,b)$ and $specializationOf(b,c)$ hold then $specializationOf(a,c)$ hold. This holds for the above definition.
-</li>
-<li>Antisymmetry: If $specializationOf(a,b)$ and
-$specializationOf(b,a)$ hold then $a=b$. This doesn't follow from the
-current definition (but it would if we stipulated that two entities
-that have the same interval, attribute and thing are equal).
-</li>
-</ul>
-</div>
+
+</section>
+<section>
<h5> Alternate </h5>
-<p>The $alternateOf$ relation indicates when two entity records present (possibly different) aspects of the same thing. The two entities may or may not overlap in time.
+<p>The $alternateOf$ relation indicates when two entity formulas present (possibly different) aspects of the same thing. The two entities may or may not overlap in time.
</p>
-<div class="formalism"> $W,I \models alternateOf(e1,e2)$ if and only if:
+<div class="formalism">
+ <p>
+ $W,\rho \models alternateOf(e_1,e_2)$ holds if and only if:</p>
<ol>
-<li>[WF] Both $e1$ and $e2$ are entity identifiers, denoting $ent_1 = I(e1)$ and $ent_2 = I(e2)$.
+<li>[WF] Both $e_1$ and $e_2$ are entity identifiers, denoting $ent_1 = \rho(e_1)$ and $ent_2 = \rho(e_2)$.
</li>
<li>The two objects refer to the same underlying Thing: $thingOf(ent_1) = thingOf(ent_2)$
</li></ol>
</div>
-<div class="remark">
- <p>There has been discussion whether $alternateOf$ is <em>symmetric</em> and <em>transitive</em>:</p>
-<ul><li> <b>Symmetry</b>: If $alternateOf(a,b)$ holds then $alternateOf(b,a)$ holds.
-</li><li> <b>Transitivity</b>: If $alternateOf(a,b)$ and $alternateOf(b,c)$ hold then $alternateOf(a,c)$ hold. This holds of the above definition.
-</li></ul>
-
-<p>We also consider the following properties which have been suggested:</p>
-<ul>
- <li> $specializationOf(e_1,e_2)$ implies $alternateOf(e_1,e_2)$? (This holds at the moment.)</li>
-<li> $alternateOf(a, b)$ if and only if there exists c such that $specializationOf(a,c)$ and $specializationOf(b,c)$? This does <b>not</b> necessarily hold without further assumptions about the Entities.</li>
-</ul>
</section>
+
+<section>
+
+<h5> Membership </h5>
+
+<p>The $hadMember$ relation relates a collection to an element of the collection.
+</p>
+<div class="formalism">
+ <p>
+ $W,\rho \models hadMember(c,e)$ holds if and only if:</p>
+<ol>
+<li>[WF] Both $e_1$ and $e_2$ are entity identifiers, denoting $coll
+ = \rho(c) \in Collections$ and $ent = \rho(e) \in Entities$.
+</li>
+<li>TODO
+</li></ol>
+</div>
+<div class="note">
+ <p>Additional constraints needed above to refer to (not yet defined)
+collection structure of entities/things.</p>
+ </div>
+
+
+</section>
+
+</section>
+
+ <section>
+ <h3>Auxiliary formulas</h3>
+
+ <p>In this section, we define the semantics of additional formulas
+ concerning ordering, null values, and typing. These are used in the
+ logical versions of constraints.</p>
+
+ <section>
+ <h4>Equals</h4>
+ <p>As usual, an equality formula means that two expressions denote
+ the same value. Identifiers always denote $Objects$.</p>
+ <div class="formalism" id="equality">
+ <p>$W,\rho \models x = y$ holds if and only if $\rho(x) =
+ \rho(y)$.</p>
+ </div>
+ </section>
+ <section>
+ <h4>Precedes and Strictly Precedes</h4>
+ <p>The precedes relation $x \preceq y$ holds between two events, one taking
+ place before (or simultaneouslt with) another. Since the
+ reference semantics assumes that times are linearly ordered and
+ event times are
+ mapped to a single time line, this amounts to
+ comparing the event times. The semantics of strictly precedes ($x
+ \prec y$ is similar, only $x$ must take place strictly before $y$.</p>
+ <div class="formalism" id="precedes">
+ <ol>
+ <li>$W,\rho \models x \preceq y$ holds if and only if
+ $time(\rho(x)) \leq time(\rho(y))$.</li>
+ <li>$W,\rho \models x \prec y$ holds if and only if
+ $time(\rho(x)) < time(\rho(y))$.</li>
+ </ol>
+ </div>
+ </section>
+
+ <section>
+ <h4>notNull</h4>
+ <p>The $notNull(x)$ formula is used to specify that a value may not
+ be the null value $\bot$. The symbol $-$ always denotes the null
+ value (i.e. $\rho(-) = \bot$).
+ <div class="formalism" id="notNull">
+ <p>$W,\rho\models notNull(e)$ holds if and only if $e \neq
+ \bot$.
+ </p>
+ </div>
+
+ </section>
+
+ <section>
+ <h4>typeOf</h4>
+
+ <p>The typing formula $typeOf(x,t)$ constrains the type of the value of
+ $x$. </p>
+
+ <div class="formalism" id="typeOf">
+ <ol><li>$W,\rho\models typeOf(e,entity)$ holds if and only if
+ $\rho(e) \in Entities$.</li>
+ <li>$W,\rho\models typeOf(a,activity)$ holds if and only if
+ $\rho(a) \in Activities.</li>
+ <li>$W,\rho\models typeOf(ag,activity)$ holds if and only if
+ $\rho(ag) \in Agents.</li>
+ <li>$W,\rho\models typeOf(c,prov:Collection)$ holds if and only if
+ TODO.</li>
+ <li>$W,\rho\models typeOf(c,prov:EmptyCollection)$ holds if and only if
+ TODO.</li>
+ </ol>
+
+ </div>
+
+ <div class="note">TODO Collections</div>
+
+ </section>
+
+ </section>
+ </section>
+
<section id="theory">
<h2> Inferences and Constraints </h2>
+ <p>
+ In this section we restate all of the inferences and constraints
+ of PROV-CONSTRAINTS in terms of first-order logic. For each, we
+ give a proof sketch showing why the inference or constraint is
+ sound for reasoning about the reference semantics. We exclude the
+ definitional rules in PROV-CONSTRAINTS because they are only
+ needed for expanding the abbreviated forms of PROV-N statements to
+ the logical formulas used here.</p>
+<section>
+<h2>Inferences</h2>
+
<div class="inference" number="5" id="communication-generation-use-inference">$\begin{array}[t]{l}
\forall id,a_2,a_1,attrs.~
\\
@@ -1854,7 +2192,7 @@
<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,[]))
+\qquad wasDerivedFrom(id,e_2,e_1,a,g,u,[prov:type = prov:Revision]))
\\
\quad\Rightarrow
alternateOf(e_2,e_1)
@@ -1954,6 +2292,10 @@
\quad\Rightarrow
alternateOf(e,e)
\end{array}$</div>
+<div class="proof">
+ <p> Suppose $ent = rho(e)$. Clearly $e \in Entities$ and
+ $thingOf(e) = thingOf(e)$, so $W,\rho \models alternateOf(e,e)$.</p>
+ </div>
<div class="inference" number="17" id="alternate-transitive">$\begin{array}[t]{l}
\forall e_1,e_2,e_3.~
\\
@@ -1962,6 +2304,13 @@
\quad\Rightarrow
alternateOf(e_1,e_3)
\end{array}$</div>
+<div class="proof">
+ <p> Suppose $ent_1 = rho(e_1)$ and $ent_2 = \rho(e_2)$ and $ent_3 = \rho(e_3)$. Then by
+ assumption $ent_1$, $ent_2$, and $ent_3$ are in $Entities$ and
+ $thingOf(e_1) = thingOf(e_2)$ and $thingOf(e_2) = thingOf(e_3)$, so
+ $thingOf(e_1) = thingOf(e_3), as required to conclude $W,\rho
+ \models alternateOf(e_2,e_1)$.</p>
+ </div>
<div class="inference" number="18" id="alternate-symmetric">$\begin{array}[t]{l}
\forall e_1,e_2.~
\\
@@ -1970,6 +2319,13 @@
\quad\Rightarrow
alternateOf(e_2,e_1)
\end{array}$</div>
+<div class="proof">
+ <p> Suppose $ent_1 = rho(e_1)$ and $ent_2 = \rho(e_2)$. Then by
+ assumption both $ent_1$ and $ent_2$ are in $Entities$ and
+ $thingOf(e_1) = thingOf(e_2)$, as required to conclude $W,\rho
+ \models alternateOf(e_2,e_1)$.</p>
+ </div>
+
<div class="inference" number="19" id="specialization-transitive">$\begin{array}[t]{l}
\forall e_1,e_2,e_3.~
\\
@@ -1978,6 +2334,17 @@
\quad\Rightarrow
specializationOf(e_1,e_3)
\end{array}$</div>
+<div class="proof">
+ <p> Suppose the conditions for specialization hold of $ent_1$ and
+ $ent_2$ and for $ent_2$ and $ent_3$, where $ent_1 = \rho(e_1)$ and $ent_2 = \rho(e_2)$ and $ent_3 =
+ \rho(e_3)$. Then $lifetime(e_1) \subseteq lifetime(e_2) \subseteq
+ lifetime(e_3)$. Moreover, suppose $value(obj_3) \neq \bot$. Then
+ $value(obj_2,attr) = value(obj_3,attr) \neq \bot$, and similarly
+ $value(obj_1,attr) = value(obj_2,attr) = value(obj_1,attr)$. (TODO:
+ How do we know $e_3 \neq e_1$?)
+</p>
+</div>
+
<div class="inference" number="20" id="specialization-alternate-inference">$\begin{array}[t]{l}
\forall e_1,e_2.~
\\
@@ -1986,6 +2353,12 @@
\quad\Rightarrow
alternateOf(e_1,e_2)
\end{array}$</div>
+<div class="proof">
+ <p> If $ent_1=\rho(e_1)$ and $ent_2 = \rho(e_2)$ are
+ specializations, then $thingOf(ent_1) = thingOf(ent_2)$.
+</p>
+</div>
+
<div class="inference" number="21" id="specialization-attributes-inference">$\begin{array}[t]{l}
\forall e_1,attrs,e_2.~
\\
@@ -1994,6 +2367,22 @@
\quad\Rightarrow
entity(e_2,attrs)
\end{array}$</div>
+</section>
+<div class="proof">
+ <p> Suppose $ent_1 = \rho(e_1)$ and $ent_2 = \rho(e_2)$. Suppose
+ $(att,v)$ is an attribute-value pair in $attrs$. Since
+ $entity(e_1,attrs)$ holds, we know that $value(ent_1,att) = v \neq
+ \bot$. Thus $value(ent_2,att) = value(ent_1,att) = v$ also. Since
+ this is the case for all attribute-value pairs in $attrs$, and since
+ $e_2$ obviously denotes an entity, we can conclude $W,\rho \models entity(e,attrs$).
+ </p>
+</div>
+
+<section>
+<h2>Constraints</h2>
+<section>
+<h3>Uniqueness constraints</h3>
+
<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}
@@ -2044,6 +2433,12 @@
\quad\Rightarrow
t_2 = t
\end{array}$</div>
+</section>
+
+<section>
+<h3>Ordering constraints</h3>
+
+
<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.~
\\
@@ -2267,680 +2662,11 @@
\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.~
-\\
-\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">In this inference, none of $a$,$gen_2$, or $use_1$ can be placeholders -.<br />$\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">In this inference, any of $a$,$gen_2$, or $use_1$ can be placeholders -.<br />$\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>In this rule, $a$,$g$, or $u$ may be placeholders -.<br />$\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>In this rule, $pl$ may be a placeholder -.<br />$\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,t1,t2,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,g2,u1,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 end2
-\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">In this constraint$a$,$gen_2$, or $use_1$ must not be placeholders -.<br />$\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">In this constraint, any of $a$,$g$, or $u$ may be placeholders -.<br />$\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_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_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">In the following inferences, $pl$ may be a placeholder -.<br /><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,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(end2,ag_2,e_2,a_2,t_2,attrs_2)
-\\
-\quad\Rightarrow
-start_1 \preceq end2
-\end{array}$</li></ol></div>
+
+</section>
+
+<section>
+<h3>Typing constraints</h3>
<div class="constraint" number="50" id="typing"><ol><li>$\begin{array}[t]{l}
\forall e,attrs.~
@@ -3076,6 +2802,11 @@
\quad\Rightarrow
typeOf(c,entity) \wedge typeOf(c,prov:Collection) \wedge typeOf(c,prov:EmptyCollection)
\end{array}$</li></ol></div>
+</section>
+
+<section>
+<h3>Impossibility constraints</h3>
+
<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.~
\\
@@ -3106,7 +2837,7 @@
\quad\Rightarrow
False
\end{array}$</div>
-<div class="constraint" number="53" id="impossible-property-overlap">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:<br />$\begin{array}[t]{l}
+<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)
@@ -3114,22 +2845,18 @@
\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:<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:</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}$</p>
-</div>
+\end{array}$</div>
<div class="constraint" number="55" id="entity-activity-disjoint">$\begin{array}[t]{l}
\forall id.~
\\
-\qquad entity \in typeOf(id) \wedge activity \in typeOf(id)
+\qquad typeOf(id,entity) \wedge typeOf(id,activity)
\\
\quad\Rightarrow
False
@@ -3137,17 +2864,19 @@
<div class="constraint" number="56" id="membership-empty-collection">$\begin{array}[t]{l}
\forall c,e.~
\\
-\qquad hasMember(c,e) \wedge prov:EmptyCollection \in typeOf(c)
+\qquad hasMember(c,e) \wedge typeOf(c,prov:EmptyCollection)
\\
\quad\Rightarrow
False
\end{array}$</div>
--->
</section>
-
-<section id="completeness">
-<h2>Soundness and Completeness</h2>
+</section>
+</section>
+
+
+<section id="soundness">
+<h2>Soundness</h2>
<p>Above we have presented arguments for the soundness of the
constraints and inferences with respect to the reference semantics.
@@ -3181,26 +2910,7 @@
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>