- This version:
- http://www.w3.org/TR/2013/WD-prov-sem-20130312/
- Latest published version:
- http://www.w3.org/TR/prov-sem/
- Latest editor's draft:
- http://dvcs.w3.org/hg/prov/raw-file/default/semantics/prov-sem.html
- Previous version:
- Editor:
- James Cheney, University of Edinburgh

Copyright © 2013 W3C^{®} (MIT, ERCIM, Keio, Beihang), All Rights Reserved. W3C liability, trademark and document use rules apply.

Provenance is information about entities, activities, and people involved in producing a piece of data or thing, which can be used to form assessments about its quality, reliability or trustworthiness. PROV-DM is the conceptual data model that forms a basis for the W3C provenance (PROV) family of specifications.

This document presents a model-theoretic semantics for the PROV
data model (called the naive semantics), 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 naive semantics.
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 **not** proposed
as a canonical or required semantics of PROV and does not place any
constraints on the use of PROV.

The PROV Document Overview describes the overall state of PROV, and should be read before other PROV documents.

*This section describes the status of this document at the time of its publication. Other
documents may supersede this document. A list of current W3C publications and the latest revision
of this technical report can be found in the W3C technical reports
index at http://www.w3.org/TR/.*

- PROV-OVERVIEW (To be published as Note), an overview of the PROV family of documents [PROV-OVERVIEW];
- PROV-PRIMER (To be published as Note), a primer for the PROV data model [PROV-PRIMER];
- PROV-O (Proposed Recommendation), the PROV ontology, an OWL2 ontology allowing the mapping of PROV to RDF [PROV-O];
- PROV-DM (Proposed Recommendation), the PROV data model for provenance [PROV-DM];
- PROV-N (Proposed Recommendation), a notation for provenance aimed at human consumption [PROV-N];
- PROV-CONSTRAINTS (Proposed Recommendation), a set of constraints applying to the PROV data model [PROV-CONSTRAINTS];
- PROV-XML (To be published as Note), an XML schema for the PROV data model [PROV-XML];
- PROV-AQ (To be published as Note), the mechanisms for accessing and querying provenance [PROV-AQ];
- PROV-DICTIONARY (To be published as Note) introduces a specific type of collection, consisting of key-entity pairs [PROV-DICTIONARY];
- PROV-DC (To be published as Note) provides a mapping between PROV and Dublic Core Terms [PROV-DC];
- PROV-SEM (To be published as Note), a declarative specification in terms of first-order logic of the PROV data model (this document);
- PROV-LINKS (To be published as Note) introduces a mechanism to link across bundles [PROV-LINKS].

This document was published by the Provenance Working Group as a First Public Working Draft. If you wish to make comments regarding this document, please send them to public-prov-comments@w3.org (subscribe, archives). All comments are welcome.

Publication as a First Public Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.

This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. The group does not expect this document to become a W3C Recommendation. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.

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, and the PROV-CONSTRAINTS specification [PROV-CONSTRAINTS] that specifies definitions, inferences, and constraints that can be used to reason about PROV documents, or determine their validity. This document provides a naive formal semantics of PROV, providing a formal counterpart to the informal descriptions and motivations given elsewhere in PROV specifications.

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/invalidation, and derivation, the meaning is either obvious or situation-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.

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 lightweight). 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 **one** semantics for PROV, not a definitive specification of the **only**
semantics of PROV. We intend to provide an intuitive semantics that satisfies all
of the constraints on valid PROV instances, which ensures that no
invalid PROV instance has a model. The current naive semantics, however, is
not complete in the sense that some valid PROV instances lack models.

Note

TODO: Revise this to reflect future improvements in the semantics.

Although it is a work in progress, the naive semantics has some 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 was adopted to keep the specification closer to implementations, although other implementations are possible and allowed. In addition to providing a naive semantics, this document shows that the operational presentation of PROV validity checking is sound with respect to the declarative presentation adopted here. This could help justify alternative approaches to validity checking.

This document mostly considers the semantics of PROV statements and instances. PROV documents can consist of multiple instances, and the semantics does not (as yet) cover PROV documents, but the semantics can be used on each instance in a document separately, just as PROV-CONSTRAINTS specifies that each instance in a document is to be validated separately. So, in the rest of this document, we do not discuss PROV documents. The semantics of other features of PROV, such as dictionaries [PROV-DICTIONARY] and linking across bundles [PROV-LINKS], are beyond the scope of this document.

- Section 2 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.
- Section 3 presents the mathematical structures used for situations that PROV statements can describe.
- Section 4 defines the semantics of PROV statements and auxiliary formulas, indicating when a given formula is satisfied in a structure.
- Section 5 presents the inferences and constraints from PROV-CONSTRAINTS as first-order formulas, and gives brief justifications for their soundness.
- Section 6 summarizes the main result: soundness of
the theory introduced in section 5 with respect to the naive
semantics. Completeness does not hold for the naive semantics. The
theory is, however, sound and complete with respect to a larger
class of
*syntactic models*, which implies that a PROV instance is valid if and only if it has a syntactic model.

Note

TODO: We would like to say something stronger here, such as a completeness result for naive models, but this will take more work.

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 Section 2.5 of PROV-CONSTRAINTS.

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.

A lowercase symbol $x,y,...$ on its own denotes an identifier. Identifiers may or may not be URIs. Identifiers are viewed as variables from the point of view of logic: they denote objects, but just because we have two different identifiers $x$ and $y$ doesn't tell us that they denote different objects, 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).

We assume a linearly ordered set $(Times,\le )$ 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.

Restricting attention to linearly-ordered times, and imposing this order on events, is a simplifying assumption; it is more restrictive than required to model the constraints. As a result, there are currently some valid PROV instances that do not have naive models. It is intended that the final version of the semantics will provide a more general class of models such that every valid instance has a model.

We also consider a set $Intervals$ of closed intervals of the form $\{t\mid {t}_{1}\le t\le {t}_{2}\}$.

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 can have undefined or multiple values, we sometimes use the set $P(Value)$, that is, the set of sets of values.

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},\dots ,{a}_{n})$ instead of the semicolon notation $r(id;{a}_{1},\dots ,{a}_{n})$.

Each parameter is either an identifier, a constant (e.g. a time or other literal value in an attribute list), or a null symbol "-". Placeholder symbols $-$ can only appear in the specified arguments $pl$ in $wasAssociatedWith$ and $a,g,u$ in $wasDerivedFrom$, as shown in the grammar below.

$$\begin{array}{rcl}atomic\mathrm{\_}formula& ::=& element\mathrm{\_}formula\\ & |& relation\mathrm{\_}formula\\ & |& auxiliary\mathrm{\_}formula\\ element\mathrm{\_}formula& ::=& entity(id,attrs)\\ & |& activity(id,st,et,attrs)\\ & |& agent(id,attrs)\\ relation\mathrm{\_}formula& ::=& 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},t,attrs)\\ & |& wasEndedBy(id,{a}_{2},e,{a}_{1},t,attrs)\\ & |& wasAssociatedWith(id,ag,act,pl,attrs)\\ & |& wasAssociatedWith(id,ag,act,-,attrs)\\ & |& wasAttributedTo(id,e,ag,attrs)\\ & |& actedOnBehalfOf(if,a{g}_{2},a{g}_{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\mathrm{\_}formula& ::=& x=y\\ & |& x\prec y\\ & |& x\u2aafy\\ & |& notNull(x)\\ & |& typeOf(x,ty)\\ attrs& ::=& [att{r}_{1}={v}_{1},\dots ,att{r}_{n}={v}_{n}]\\ ty& ::=& entity\\ & |& activity\\ & |& agent\\ & |& Collection\\ & |& EmptyCollection\end{array}$$

We include the standard PROV collection types ($Collection$ and $EmptyCollection$) and the membership relation $hadMember$; however, we do not model dictionaries or the insertion or deletion relations in the PROV-DICTIONARY [PROV-DICTIONARY], since these are not part of the PROV recommendations. If these features are incorporated into future standards, their semantics (and the soundness of the associated constraints) should be modeled. We omit the $prov$ prefixes from the $Collection$ and $EmptyCollection$ types.

As stated in the Introduction, we do not explicitly model bundles or PROV documents; however, each instance can be viewed as a set of formulas and can be modeled separately. The semantics of the standard features of PROV can be defined without talking about multiple instances; however, the $mentionOf$ relation in PROV-LINKS [PROV-LINKS] is intended to support linking across bundles. Future editions of PROV may incoporate $mentionOf$ or other cross-instance assertions, and this semantics should be generalized in order to provide a rationale for such an extension and to establish the soundness of constaints associated with $memberOf$.

We also consider the usual connectives and quantifiers of first-order logic [Logic].

$$\begin{array}{rcl}\mathit{\varphi}& ::=& atomic\mathrm{\_}formula\\ & |& True\\ & |& False\\ & |& \mathrm{\neg}\text{}\mathit{\varphi}\\ & |& {\mathit{\varphi}}_{1}\wedge {\mathit{\varphi}}_{2}\\ & |& {\mathit{\varphi}}_{1}\vee {\mathit{\varphi}}_{2}\\ & |& {\mathit{\varphi}}_{1}\Rightarrow {\mathit{\varphi}}_{2}\\ & |& \mathrm{\forall}x.\mathit{\varphi}\\ & |& \mathrm{\exists}x.\mathit{\varphi}\end{array}$$

Note

TODO: Add semantic structure for collections and membership.

*Things* is a set of things in the situation being modeled. Each thing has a lifetime during which it exists and attributes whose values can change over time.

To model this, a structure $W$ includes:

- a set $Things$ of things
- a function $lifetime:Things\to Intervals$ from things to time intervals
- a function $value:Things\times Attributes\times Times\to P(Values)$

The range of $value$ is the set $P(Values)$, indicating that $value$ is essentially a multi-valued that returns a set of values (possibly empty). When $value(x,a,t)=\mathrm{\varnothing}$, we say that attribute $a$ is undefined for $x$ at time $t$.

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. A thing could 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 $\mathit{\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.

The identity of a Thing is not observable through its attributes or lifetime, so it is possible for two different $Things$ to be indistinguishable by their attribute values and lifetime. That is, if the set of $Things=\{{T}_{0},{T}_{1}\}$ and the attributes are specified as $value({T}_{0},a,t)=value({T}_{1},a,t)$ for each $t\in Times$ and $a\in Attributes$, this does not imply that ${T}_{0}={T}_{1}$.

$Things$ are things in the world that have attributes that can change over time. $Things$ may not have distinguishing features that are readily observable and permanent. In PROV, we do not talk explicitly about $Things$, but instead we talk about various objects that have discrete, fixed features, and relationships among these objects. Some objects, called $Entities$, are associated with $Things$, and their fixed attributes need to match those of the associated $Thing$ during their common lifetime.

In this section, we detail the different subsets $Objects$, and give disjointness constraints and associated functions. Generally, these constraints are necessary to validate disjointness constraints from PROV-CONSTRAINTS [PROV-CONSTRAINTS].

An *Object* is described by a time interval and attributes with
fixed values. Objects encompass entities, activities, agents, and
interactions (i.e., usage, generation, and other events or influence relations).
To model this, a structure includes:

- a set $Objects$
- a function $lifetime:Objects\to Intervals$ from objects to time intervals
- a function $value:Objects\times Attributes\to P(Values)$

Intuitively, $lifetime(e)$ is the time interval during which object $e$ exists. The set $value(e,a)$ is the set of values of attribute $a$ during the object's lifetime.

As with *Things*, the range of $value$ is sets of values,
making $value$ effectively a multivalued 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 associated with things.

Disjointness between $Objects$ and $Things$ is not necessary but is assumed in order to avoid confusion between the different categories (time-varying $Things$ vs fixed $Objects$).

An *entity* 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:

- a set $Entities\subseteq Objects$ of entities, disjoint from $Activities$ and $Events$ below.
- 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$ we have $value(obj,a)\subseteq value(thingOf(obj),a,t)$.
- $lifetime(e)\subseteq lifetime(t)$.

Although both entities and things can have undefined or multiple attribute values, their meaning is slightly different: for a thing, $value(x,a,t)=\mathrm{\varnothing}$ means that the attribute $a$ has no value at time $t$, whereas for an entity, $value(x,a)=\mathrm{\varnothing}$ only means that the thing associated to entity $x$ does not have a fixed value for $a$ during the lifetime of $x$. This does not imply that $value(thingOf(e),a,t)=\mathrm{\varnothing}$ when $t\in lifetime(e)$.

Furthermore, all of the attribute values of the entity must be present in the associated thing throughout the lifetime of the entity. For example, suppose $value(thingOf(e),a,t)$ is $\{1\}$ at some time in $lifetime(e)$ and $value(thingOf(e),a,{t}^{\prime})=\{2\}$ at some other time ${t}^{\prime}$. Then $value(e,a)$ must be $\mathrm{\varnothing}$ because there is no other set of values that is simultaneously contained in both $\{1\}$ and $\{2\}$.

In the above description of how $Entities$ relate to $Things$, we require $value(e,a)\subseteq value(thingOf(e),a,t)$ whenever $t\in lifetime(e)$. Intuitively, this means that if we are talking about a $Thing$ indirectly by describing an $Entity$, then any attributes we ascribe to the $Entity$ must also describe the associated $Thing$ during their common lifetime. Attributes of both $Entities$ and $Things$ are multi-valued, so there is no inconsistency in saying that an entity has two different values for some attribute. In some situations, further uniqueness constraints or range constraints could be imposed on attributes, for example by extending the PROV-O ontology.

Only $Entities$ are associated with $Things$, and this is necessary to provide an interpretation for the $alternateOf$ and $specializationOf$ relations. It might also make sense to associate $Agents$, $Activities$, and $Interactions$ with $Things$, or with some other structures; however, this is not necessary to model any of the current features of PROV, so in the interest of simplicity we do not do this.

We identify a specific subset of the entities called
*plans*:

A set $Plans\subseteq Entities$ of plans.

An *activity* is an object that encompasses a set of events. We introduce

- A set $Activities\subseteq Objects$ of activities.
- Activities are disjoint from Entities: $Entities\cap Activities=\mathrm{\varnothing}$.

An agent is an object that can act, by controlling, starting, ending, or participating in activities. An agent is something that bears some form of responsibility for an activity taking place, for the existence of an entity, or for another agent's activity. Agents can act on behalf of other agents. An agent may be a particular type of entity or activity; an agent cannot be both entity and activity because the sets of entities and activities are disjoint. We introduce:

A set $Agents\subseteq Objects$ of agents.

There is no requirement that every agent is either an activity or an entity.

We consider a set $Interactions\subseteq Objects$ which are split into
*Events* connecting entities and activities,
*Associations* between agents and activities,
*Communications* between pairs of activities,
*Delegations* between pairs of agents, and
*Derivations* that describe chains of generation and usage
steps. These kinds of interactions are discussed further below. Interactions are disjoint from entities, activities and agents.

- A set $Interactions=Events\cup Associations\cup Communications\cup Delegations\cup Derivations\subseteq Objects$
- A function $type:Interactions\to \{start,end,usage,generation,invalidation,derivation,revision,quotation,primarySource,attribution,delegation\}$.
- The sets $Events$, $Associations$, $Communications$, $Delegations$ and $Derivations$ are all disjoint.
- Interactions are disjoint from entities, agents and activities: $Interactions\cap (Entities\cup Activities\cup Agents)=\mathrm{\varnothing}$

An *Event* 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:

- A set $Events\subseteq Interactions$ of events, such that $type(evt)\in \{start,end,generation,usage,invalidation\}$ if and only if $evt\in Events$.
- A function $time:Events\to Times$ giving the time of each event; i.e. $lifetime(evt)=\{time(evt)\}$.
- The derived ordering on events given by $ev{t}_{1}\le ev{t}_{2}\phantom{\rule{thickmathspace}{0ex}}\u27fa\phantom{\rule{thickmathspace}{0ex}}time(ev{t}_{1})\le time(ev{t}_{2})$

An *Association* is an interaction relating an agent to an activity. To model associations, we introduce:

A set $Associations\subseteq Interactions$, such that $type(assoc)=association$ if and only if $assoc\in Associations$.

Associations are used below in the $ActsFor$ and $AssociatedWith$ relations.

Note

TODO

Note

TODO

A *Derivation* is an interaction chaining one or more generation and use steps.

A set $Derivations\subseteq Interactions$, such that $type(deriv)\in \{derivation,revision,primarySource,quotation\}$ if and only if $deriv\in Derivations$.

See below for the associated derivation path and DerivedFrom relation.

A derivation path implies the existence of at least one chained generation and use step. However, not all such potential derivation paths are associated with derivations; there can (and in general will) be many such paths that are not associated with derivation steps. In other words, because we require derivations to be explicitly assocated with derivation paths, it is not sound to infer the existence of a derivation from the existence of an alternating generation/use chain.

The entities, interactions, and activities in a structure are related in the following ways:

- 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(evt)=usage$ must hold.
- 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(evt)=generation$ must hold.
- 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 $max(lifetime(e))=time(evt)$ and $type(evt)=invalidation$ must hold.
- A relation $EventActivity\subseteq Events\times Activities$ associating activities with events, such that $(act,evt)\in EventActivity$ implies $time(evt)\in lifetime(act)$.
- A relation $AssociatedWith\subseteq Associations\times Agents\times Activities\times Plan{s}_{\mathrm{\perp}}$ indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan.
- 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.

Note

TODO: Communication, start, end relations

Note

TODO: Specialization relation

Note

TODO: Additional axioms concerning the relations; for example:
clarify that every Event is associated with an Activity and
Entity; ensure that for attribution the agent's lifetime must
start before that of the entity.

Recall that above we introduced a subset of interactions called *Derivations*. These identify *paths* of the form

$$en{t}_{n}\cdot {g}_{n}\cdot ac{t}_{n}\cdot {u}_{n}\cdot en{t}_{n-1}\cdot ...\cdot en{t}_{1}\cdot {g}_{1}\cdot ac{t}_{1}\cdot {u}_{1}\cdot en{t}_{0}$$

where the $en{t}_{i}$ are entities, $ac{t}_{i}$ are activities, ${g}_{i}$ are generations, and ${u}_{i}$ are usages.

Formally, we consider the (regular) language:

$$DerivationPaths=Entities\cdot (Events\cdot Activities\cdot Events\cdot Entities{)}^{+}$$

with the constraints that for each derivation path:

- for each substring $ent\cdot g\cdot act$ we have $(g,ent)\in Generated$ and $(g,act)\in EventActivity$, and
- for each substring $act\cdot u\cdot ent$ we have $(u,ent)\in Used$ and $(u,act)\in EventActivity$.

Each derivation $d\in Derivations$ has an associated derivation path. We link each derivation to an associated derivation path using the function $derivationPath:Derivations\to DerivationPaths$.

The $derivationPath$ function links each $d\in Derivations$ to a derivation path. A derivation has exactly one associated derivation path. However, if the PROV-N statement wasDerivedFrom(e_2,e_1,-,-,-) is asserted in an instance, there may be multiple derivation paths linking ${e}_{2}$ to ${e}_{1}$, each corresponding to a different, identified by different derivations $d\in Derivations$.

Note

We can make the characterization of DerivationPaths more
precise/concise by introducing sets of Usage and Generation events.

The reason why we need paths and not just individual derivation steps is that $wasDerivedFrom(id,{e}_{2},{e}_{1},-,-,-,attrs)$ formulas can represent multiple derivation steps.

A *structure* $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.

Note

TODO: Highlight the distinctive vs obvious/routine features.

We need to link identifiers to the objects they denote. We do this using a function which we shall call an *interpretation*.
Thus, we consider interpretations as follows:
An interpretation is a function $\mathit{\rho}:Identifiers\to Objects$ describing
which object is the target of each identifier. The mapping from identifiers to objects may **not** change over time.

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.

Consider a formula $\mathit{\varphi}$, a structure $W$ and an interpretation $I$. We define notation $W,\mathit{\rho}\models \mathit{\varphi}$ which means that $\mathit{\varphi}$ is satisfied in $W,\mathit{\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:

- $W,\mathit{\rho}\models True$ always holds.
- $W,\mathit{\rho}\models False$ never holds.
- $W,\mathit{\rho}\models \mathrm{\neg}\mathit{\varphi}$ holds if and only if $W,\mathit{\rho}\models \mathit{\varphi}$ does not hold.
- $W,\mathit{\rho}\models \mathit{\varphi}\wedge \mathit{\psi}$ holds if and only if $W,\mathit{\rho}\models \mathit{\varphi}$ and $W,i\models \mathit{\psi}$.
- $W,\mathit{\rho}\models \mathit{\varphi}\vee \mathit{\psi}$ holds if either $W,\mathit{\rho}\models \mathit{\varphi}$ or $W,\mathit{\rho}\models \mathit{\psi}$ holds.
- $W,\mathit{\rho}\models \mathit{\varphi}\Rightarrow \mathit{\psi}$ holds if $W,\mathit{\rho}\models \mathit{\varphi}$ implies $W,\mathit{\rho}\models \mathit{\psi}$.
- $W,\mathit{\rho}\models \mathrm{\exists}x.\mathit{\varphi}$ holds if there exists some $obj\in Objects$ such that $W,\mathit{\rho}[x:=obj]\models \mathit{\varphi}$.
- $W,\mathit{\rho}\models \mathrm{\forall}x.\mathit{\varphi}$ holds if there for every $obj\in Objects$ we have $W,\mathit{\rho}[x:=obj]\models \mathit{\varphi}$.

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.

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 $\{{\mathit{\varphi}}_{1},\dots ,{\mathit{\varphi}}_{n}\}$, or equivalently a single formula $\mathrm{\exists}{x}_{1},\dots ,{x}_{k}.\text{}{\mathit{\varphi}}_{1}\wedge \cdots \wedge {\mathit{\varphi}}_{n}$, where ${x}_{1},\dots ,{x}_{k}$ are the existential variables of $I$.

We say that an object $obj$ matches attributes $[att{r}_{1}=va{l}_{1},...]$ in structure $W$ provided: for each attribute $att{r}_{i}$, we have $va{l}_{i}\in W.value(obj,att{r}_{i})$. This is sometimes abbreviated as: $match(W,obj,attrs)$.

An entity formula is of the form $entity(id,attrs)$ where $id$ denotes an entity.

Entity formulas $entity(id,attrs)$ can be interpreted as follows:

$W,\mathit{\rho}\models entity(id,attrs)$ holds if and only if:

- [WF] $id$ denotes an entity $ent=\mathit{\rho}(id)\in Entities$
- the attributes match: $match(W,ent,attrs)$.

Not all of the attributes of an entity object are required to be present in an entity formula about that object. For example, the following formulas all hold if $x$ denotes an entity $e$ such that $value(e,a)=\{4,5\},value(e,b)=\{6\}$ hold:

entity(x,[]) entity(x,[a=5]) entity(x,[a=4,a=5]) entity(x,[a=4,b=6])

Note that PROV-CONSTRAINTS normalization will merge these formulas to a single one:

entity(x,[a=4,a=5,b=6])

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$.

$W,\mathit{\rho}\models activity(id,st,et,attrs)$ holds if and only if:

- [WF] The identifier $id$ maps to an activity $act=\mathit{\rho}(id)\in Activities$
- $\mathit{\rho}(st)\in Times$ is the activity's start time, that is: $min(lifetime(id))=\mathit{\rho}(st)$
- $\mathit{\rho}(et)$ is the activity's end time, that is: $max(lifetime(id))=\mathit{\rho}(et)$
- The attributes match: $match(W,act,attrs)$.

An agent formula is of the form $agent(id,attrs)$ where $id$ denotes the agent and $attrs$ describes additional attributes.

$W,\mathit{\rho}\models agent(id,attrs)$ holds if and only if:

- [WF] $id$ denotes an agent $ag=\mathit{\rho}(id)\in Agents$
- The attributes match: $match(W,ag,attrs)$.

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 a time.

$W,\mathit{\rho}\models wasGeneratedBy(id,e,a,t,attrs)$ holds if and only if:

- [WF] The identifier $id$ denotes an event $evt=\mathit{\rho}(id)\in Events$.
- [WF] The identifier $e$ denotes an entity $ent=\mathit{\rho}(e)\in Entities$.
- [WF] The identifier $a$ denotes an activity $act=\mathit{\rho}(a)\in Activities$.
- The event $evt$ is involved in $act$, that is, $(evt,act)\in EventActivity$.
- The type of $evt$ is $generation$, i.e. $type(evt)=generation$.
- The event $evt$ occurred at time $\mathit{\rho}(t)\in Times$, i.e. $time(evt)=\mathit{\rho}(t)$.
- The event $evt$ generated $ent$, i.e. $(evt,ent)\in Generated$.
- The attribute values match: $match(W,evt,attrs)$.

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 a time.

$W,\mathit{\rho}\models used(id,a,e,t,attrs)$ holds if and only if:

- [WF] The identifier $id$ denotes an event $evt=\mathit{\rho}(id)\in Events$.
- [WF] The identifier $a$ denotes an activity $act=\mathit{\rho}(id)\in Activities$.
- [WF] The identifier $e$ denotes an entity $ent=\mathit{\rho}(e)\in Entities$.
- The event $evt$ is part of $act$, i.e. $(evt,act)\in EventActivity$.
- The type of $evt$ is $use$, i.e., $type(evt)=use$.
- The event $evt$ occurred at time $\mathit{\rho}(t)\in Times$, i.e. $time(evt)=\mathit{\rho}(t)$.
- The event $evt$ used $obj$, i.e. $(evt,ent)\in Used$.
- The attribute values match: $match(W,evt,attrs)$.

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 a time.

An invalidation formula $W,\mathit{\rho}\models wasInvalidatedBy(id,e,a,t,attrs)$ holds if and only if:

- [WF] The identifier $id$ denotes an event $evt=\mathit{\rho}(id)\in Events$.
- [WF] The identifier $e$ denotes an entity $ent=\mathit{\rho}(e)\in Entities$.
- [WF] The identifier $a$ denotes an activity $act=\mathit{\rho}(a)\in Activities$.
- The event $evt$ is involved in $act$, that is, $(evt,act)\in EventActivity$.
- The type of $evt$ is $invalidation$, i.e. $type(evt)=invalidation$.
- The event $evt$ occurred at time $\mathit{\rho}(t)\in Times$, i.e. $time(evt)=\mathit{\rho}(t)$.
- The event $evt$ invalidated $ent$, i.e. $(evt,ent)\in Invalidated$.
- The attribute values match: $match(W,evt,attrs)$.

An association formula has the form $wasAssociatedWith(id,a,ag,pl,attrs)$.

$W,\mathit{\rho}\models wasAssociatedWith(id,a,ag,pl,attrs)$ holds if and only if:

- [WF] $assoc$ denotes an association $assoc=\mathit{\rho}(id)\in Associations$.
- [WF] $a$ denotes an activity $act=\mathit{\rho}(a)\in Activities$.
- [WF] $ag$ denotes an agent $agent=\mathit{\rho}(ag)\in Agents$.
- [WF] $pl$ denotes a plan $plan=\mathit{\rho}(pl)\in Plans$.
- The association associates the agent with the activity and plan, i.e. $(assoc,agent,act,plan)\in AssociatedWith$.
- The attributes match: $match(W,assoc,attrs)$.

$W,\mathit{\rho}\models wasAssociatedWith(id,a,ag,-,attrs)$ holds if and only if:

- [WF] $assoc$ denotes an association $assoc=\mathit{\rho}(id)\in Associations$.
- [WF] $a$ denotes an activity $act=\mathit{\rho}(a)\in Activities$.
- [WF] $ag$ denotes an agent $agent=\mathit{\rho}(ag)\in Agents$.
- The association associates the agent with the activity and plan, i.e. $(assoc,agent,act,\mathrm{\perp})\in AssociatedWith$.
- The attributes match: $match(W,assoc,attrs)$.

A start formula $wasStartedBy(id,{a}_{2},e,{a}_{1},t,attrs)$ is interpreted as follows:

$W,\mathit{\rho}\models wasStartedBy(id,{a}_{2},e,{a}_{1},t,attrs)$ holds if and only if:

- [WF] $id$ denotes an event $evt=\mathit{\rho}(id)\in Events$.
- [WF] ${a}_{2}$ denotes an activity $ac{t}_{2}=\mathit{\rho}({a}_{2})\in Activities$.
- [WF] $e$ denotes an entity $ent=\mathit{\rho}(e)\in Entities$.
- [WF] ${a}_{1}$ denotes an activity $ac{t}_{1}=\mathit{\rho}({a}_{1})\in Activities$.
- The event $evt$ has type $start$, i.e. $type(evt)=start$.
- The event happened at the start of $ac{t}_{2}$, that is, $(evt,ac{t}_{2})\in EventsActivities$, and $\mathit{\rho}(t)=min(lifetime(ac{t}_{2}))=time(evt)$.
- TODO: The entity $e$ was generated by $ac{t}_{1}$ and started $ac{t}_{2}$.
- The event happened during $ac{t}_{1}$, that is, $(evt,ac{t}_{1})\in EventsActivities$.
- The attributes match: $match(W,evt,attrs)$.

An activity end formula $wasEndedBy(id,{a}_{2},e,{a}_{1},t,attrs)$ is interpreted as follows:

$W,\mathit{\rho}\models wasEndedBy(id,{a}_{2},e,{a}_{1},t,attrs)$ holds if and only if:

- [WF] $id$ denotes an event $evt=\mathit{\rho}(id)\in Events$.
- [WF] ${a}_{2}$ denotes an activity $ac{t}_{2}=\mathit{\rho}({a}_{2})\in Activities$.
- [WF] $e$ denotes an entity $ent=\mathit{\rho}(e)\in Entities$.
- [WF] ${a}_{1}$ denotes an activity $ac{t}_{1}=\mathit{\rho}({a}_{1})\in Activities$.
- The event $evt$ has type $end$, i.e. $type(evt)=end$.
- The event happened at the end of $ac{t}_{2}$, that is, $(evt,ac{t}_{2})\in EventsActivities$, and $\mathit{\rho}(t)=max(lifetime(ac{t}_{2}))=time(evt)$.
- TODO: The entity $e$ was generated by $ac{t}_{1}$ and ended $ac{t}_{2}$.
- The event happened during $ac{t}_{1}$, that is, $(evt,act_1) \in EventActivity.
- The attributes match: $match(W,evt,attrs)$.

An attribution formula $wasAttributedTo(id,e,ag,attrs)$ is interpreted as follows:

$W,\mathit{\rho}\models wasAttributedTo(id,e,ag,attrs)$ holds if and only if:

- [WF] $id$ denotes an association $assoc=\mathit{\rho}(id)\in Associations$.
- [WF] $e$ denotes an entity $ent=\mathit{\rho}(e)\in Entities$.
- [WF] $ag$ denotes an agent $agent=\mathit{\rho}(ag)\in Agents$.
- The entity was attributed to the agent, i.e. $(assoc,ent,agent)\in AttributedTo$.
- The attributes match: $match(W,evt,attrs)$.

Note

TODO: Communication

The $actedOnBehalfOf(id,a{g}_{2},a{g}_{1},act,attrs)$ relation is interpreted using the $ActsFor$ relation as follows:

$W,\mathit{\rho}\models actedOnBehalfOf(id,a{g}_{2},a{g}_{1},act,attrs)$ holds if and only if:

- [WF] $id$ denotes an association $deleg=\mathit{\rho}(id)\in Delegations$.
- [WF] $a$ denotes an activity $act=\mathit{\rho}(a)\in Activities$.
- [WF] $a{g}_{1},a{g}_{2}$ denote agents $agen{t}_{1}=\mathit{\rho}(a{g}_{1}),agen{t}_{2}=\mathit{\rho}(a{g}_{2})\in Agents$.
- The agent $agen{t}_{2}$ acts for the agent $agen{t}_{1}$ with respect to the activity $act$, i.e. $(deleg,agen{t}_{2},agen{t}_{1},act)\in ActsFor$.
- The attributes match: $match(W,assoc,attrs)$.

Derivation formulas can be of one of two forms:

- $wasDerivedFrom(id,{e}_{2},{e}_{1},a,g,u,attrs)$, which specifies an activity, generation and usage event. For convenience we call a precise derivation.
- and $wasDerivedFrom(id,{e}_{2},{e}_{1},-,-,-,attrs)$, which does not specify an activity, generation and usage event. For convenience we call this an imprecise derivation.

A precise derivation formula has the form $wasDerivedFrom(id,{e}_{2},{e}_{1},a,g,u,attrs)$.

$W,\mathit{\rho}\models wasDerivedFrom(id,{e}_{2},{e}_{1},act,g,u,attrs)$ holds if and only if:

- [WF] $id$ denotes a derivation $deriv=\mathit{\rho}(id)\in Derivations$.
- [WF] ${e}_{1},{e}_{2}$ denote entities $en{t}_{1}=\mathit{\rho}({e}_{1}),en{t}_{2}=\mathit{\rho}({e}_{2})\in Entities$.
- [WF] $a$ denotes an activity $act=\mathit{\rho}(a)\in Activities$.
- [WF] $g$ denotes a generation event $gen=\mathit{\rho}(g)\in Events$ and $type(\mathit{\rho}(g))=generation$.
- [WF] $u$ denotes a use event $\mathit{\rho}(u)\in Events$ and $type(\mathit{\rho}(u))=use$.
- The derivation denotes a one-step derivation $derivationPath(deriv)=en{t}_{2}\cdot gen\cdot act\cdot use\cdot en{t}_{1}$.
- The attribute values match: $match(W,deriv,attrs)$.

An imprecise derivation formula has the form $wasDerivedFrom(id,{e}_{2},{e}_{1},-,-,-,attrs)$.

$W,\mathit{\rho}\models wasDerivedFrom(id,{e}_{2},{e}_{1},-,-,-,attrs)$ holds if and only if:

- [WF] $id$ denotes a derivation $deriv=\mathit{\rho}(id)\in Derivations$
- [WF] ${e}_{1},{e}_{2}$ denote entities $en{t}_{1}=\mathit{\rho}({e}_{1}),en{t}_{2}=\mathit{\rho}({e}_{2})\in Entities$
- $derivationPath(deriv)=en{t}_{2}\cdot w\cdot en{t}_{1}$ for some $w$
- The attribute values match: $match(W,deriv,attrs)$.

Note

TODO: Define influence semantics.

The $specializationOf({e}_{1},{e}_{2})$ relation indicates when one entity formula presents more specific aspects of another.

Note

TODO: The content of this definition may need to be moved into the semantic structure via an irreflexive/transitive specialization relation on Entities, since by itself this definition is not transitive.

$W,\mathit{\rho}\models specializationOf({e}_{1},{e}_{2})$ holds if and only if:

- [WF] Both ${e}_{1}$ and ${e}_{2}$ are entity identifiers, denoting distinct entities $en{t}_{1}=\mathit{\rho}({e}_{1})\in Entities$ and $en{t}_{2}=\mathit{\rho}({e}_{2})\in Entities$, where $en{t}_{1}\ne en{t}_{2}$.
- The two Entities refer to the same Thing, that is, $thingOf(en{t}_{1})=thingOf(en{t}_{2})$.
- The lifetime of $en{t}_{1}$ is contained in that of $en{t}_{2}$, i.e. $lifetime(en{t}_{1})\subseteq lifetime(en{t}_{2})$.
- For each attribute $attr$ we have $value(en{t}_{1},attr)\supseteq value(en{t}_{2},attr)$.

The second criterion says that the two Entities present (possibly different) aspects of the same Thing. Note that the third criterion allows $en{t}_{1}$ and $en{t}_{2}$ to have the same lifetime (or that of $en{t}_{2}$ can be larger). The last criterion allows $en{t}_{1}$ to have more defined attributes than $en{t}_{2}$, but they must include the attributes defined by $en{t}_{2}$.

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.

$W,\mathit{\rho}\models alternateOf({e}_{1},{e}_{2})$ holds if and only if:

- [WF] Both ${e}_{1}$ and ${e}_{2}$ are entity identifiers, denoting $en{t}_{1}=\mathit{\rho}({e}_{1})$ and $en{t}_{2}=\mathit{\rho}({e}_{2})$.
- The two objects refer to the same underlying Thing: $thingOf(en{t}_{1})=thingOf(en{t}_{2})$

The $hadMember$ relation relates a collection to an element of the collection.

$W,\mathit{\rho}\models hadMember(c,e)$ holds if and only if:

- [WF] Both ${e}_{1}$ and ${e}_{2}$ are entity identifiers, denoting $coll=\mathit{\rho}(c)\in Collections$ and $ent=\mathit{\rho}(e)\in Entities$.
- TODO

Note

Additional constraints needed above to refer to (not yet defined) collection structure of entities/things.

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.

As usual, an equality formula means that two expressions denote the same value. Identifiers always denote $Objects$.

$W,\mathit{\rho}\models x=y$ holds if and only if $\mathit{\rho}(x)=\mathit{\rho}(y)$.

The precedes relation $x\u2aafy$ holds between two events, one taking place before (or simultaneously with) another. Since the naive 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$).

- $W,\mathit{\rho}\models x\u2aafy$ holds if and only if $\mathit{\rho}(x),\mathit{\rho}(y)\in Events$ and $time(\mathit{\rho}(x))\le time(\mathit{\rho}(y))$.
- $W,\mathit{\rho}\models x\prec y$ holds if and only if $\mathit{\rho}(x),\mathit{\rho}(y)\in Events$ and $time(\mathit{\rho}(x))<time(\mathit{\rho}(y))$.

Because we use a linearly ordered time to define event precedence, there are valid PROV instances that are not satisfied in any naive model. For example:

entity(e) activity(a1) activity(a2) wasGeneratedBy(gen1; e, a1, 2011-11-16T16:05:00) wasGeneratedBy(gen2; e, a2, 2012-11-16T16:05:00) //different date

This instance is valid, and must satisfy precedence constraints $ge{n}_{1}\u2aafge{n}_{2}$ and $ge{n}_{2}\u2aafge{n}_{1}$, but $time(gen_1)=

The $notNull(x)$ formula is used to specify that a value may not be the null value $\mathrm{\perp}$. The symbol $-$ always denotes the null value (i.e. $\mathit{\rho}(-)=\mathrm{\perp}$).

$W,\mathit{\rho}\models notNull(e)$ holds if and only if $e\ne \mathrm{\perp}$.

The typing formula $typeOf(x,t)$ constrains the type of the value of $x$.

- $W,\mathit{\rho}\models typeOf(e,entity)$ holds if and only if $\mathit{\rho}(e)\in Entities$.
- $W,\mathit{\rho}\models typeOf(a,activity)$ holds if and only if $\mathit{\rho}(a)\in Activities$.
- $W,\mathit{\rho}\models typeOf(ag,agent)$ holds if and only if $\mathit{\rho}(ag)\in Agents$.
- $W,\mathit{\rho}\models typeOf(c,Collection)$ holds if and only if TODO.
- $W,\mathit{\rho}\models typeOf(c,EmptyCollection)$ holds if and only if TODO.

Note

TODO Collections

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 naive 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.

$\begin{array}{l}\mathrm{\forall}id,{a}_{2},{a}_{1},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasInformedBy(id,{a}_{2},{a}_{1},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}e,gen,{t}_{1},use,{t}_{2}.\text{}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},[])\wedge used(use,{a}_{2},e,{t}_{2},[])\end{array}$

$\begin{array}{l}\mathrm{\forall}gen,e,{a}_{1},{t}_{1},attr{s}_{1},i{d}_{2},{a}_{2},{t}_{2},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge used(i{d}_{2},{a}_{2},e,{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}id.\text{}wasInformedBy(id,{a}_{2},{a}_{1},[])\end{array}$

$\begin{array}{l}\mathrm{\forall}e,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}entity(e,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}gen,{a}_{1},{t}_{1},inv,{a}_{2},{t}_{2}.\text{}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},[])\wedge wasInvalidatedBy(inv,e,{a}_{2},{t}_{2},[])\end{array}$

$\begin{array}{l}\mathrm{\forall}a,{t}_{1},{t}_{2},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}activity(a,{t}_{1},{t}_{2},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}start,{e}_{1},{a}_{1},end,{a}_{2},{e}_{2}.\text{}wasStartedBy(start,a,{e}_{1},{a}_{1},{t}_{1},[])\wedge wasEndedBy(end,a,{e}_{2},{a}_{2},{t}_{2},[])\end{array}$

$\begin{array}{l}\mathrm{\forall}id,a,{e}_{1},{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(id,a,{e}_{1},{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}gen,{t}_{1}.\text{}wasGeneratedBy(gen,{e}_{1},{a}_{1},{t}_{1},[])\end{array}$

$\begin{array}{l}\mathrm{\forall}id,a,{e}_{1},{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasEndedBy(id,a,{e}_{1},{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}gen,{t}_{1}.\text{}wasGeneratedBy(gen,{e}_{1},{a}_{1},{t}_{1},[])\end{array}$

In this inference, none of $a$,$ge{n}_{2}$, or $us{e}_{1}$ can be placeholders -.

$\begin{array}{l}\mathrm{\forall}id,{e}_{2},{e}_{1},a,ge{n}_{2},us{e}_{1},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(a)\wedge notNull(ge{n}_{2})\wedge notNull(us{e}_{1})\wedge wasDerivedFrom(id,{e}_{2},{e}_{1},a,ge{n}_{2},us{e}_{1},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}{t}_{1},{t}_{2}.\text{}used(us{e}_{1},a,{e}_{1},{t}_{1},[])\wedge wasGeneratedBy(ge{n}_{2},{e}_{2},a,{t}_{2},[])\end{array}$In this inference, any of $a$,$ge{n}_{2}$, or $us{e}_{1}$ can be placeholders -.

$\begin{array}{l}\mathrm{\forall}id,{e}_{1},{e}_{2},a,g,u.\text{}\\ \phantom{\rule{2em}{0ex}}wasDerivedFrom(id,{e}_{2},{e}_{1},a,g,u,[prov:type=prov:Revision]))\\ \phantom{\rule{1em}{0ex}}\Rightarrow alternateOf({e}_{2},{e}_{1})\end{array}$$\begin{array}{l}\mathrm{\forall}att,e,ag,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasAttributedTo(att,e,ag,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}a,t,gen,assoc,pl.\text{}wasGeneratedBy(gen,e,a,t,[])\wedge wasAssociatedWith(assoc,a,ag,pl,[])\end{array}$

$\begin{array}{l}\mathrm{\forall}id,a{g}_{1},a{g}_{2},a,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}actedOnBehalfOf(id,a{g}_{1},a{g}_{2},a,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow \mathrm{\exists}i{d}_{1},p{l}_{1},i{d}_{2},p{l}_{2}.\text{}wasAssociatedWith(i{d}_{1},a,a{g}_{1},p{l}_{1},[])\wedge wasAssociatedWith(i{d}_{2},a,a{g}_{2},p{l}_{2},[])\end{array}$

- $\begin{array}{l}\mathrm{\forall}id,e,a,t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(id,e,a,t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,e,a,attrs)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,a,e,t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}used(id,a,e,t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,a,e,attrs)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{a}_{2},{a}_{1},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasInformedBy(id,{a}_{2},{a}_{1},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,{a}_{2},{a}_{1},attrs)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{a}_{2},e,{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(id,{a}_{2},e,{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,{a}_{2},e,attrs)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{a}_{2},e,{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasEndedBy(id,{a}_{2},e,{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,{a}_{2},e,attrs)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,e,a,t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasInvalidatedBy(id,e,a,t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,e,a,attrs)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{e}_{2},{e}_{1},a,g,u,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasDerivedFrom(id,{e}_{2},{e}_{1},a,g,u,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,{e}_{2},{e}_{1},attrs)\end{array}$
In this rule, $a$,$g$, or $u$ may be placeholders -.

$\begin{array}{l}\mathrm{\forall}id,e,ag,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasAttributedTo(id,e,ag,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,e,ag,attrs)\end{array}$In this rule, $pl$ may be a placeholder -.

$\begin{array}{l}\mathrm{\forall}id,a,ag,pl,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasAssociatedWith(id,a,ag,pl,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,a,ag,attrs)\end{array}$- $\begin{array}{l}\mathrm{\forall}id,a{g}_{2},a{g}_{1},a,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}actedOnBehalfOf(id,a{g}_{2},a{g}_{1},a,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow wasInfluencedBy(id,a{g}_{2},a{g}_{1},attrs)\end{array}$

$\begin{array}{l}\mathrm{\forall}e.\text{}\\ \phantom{\rule{2em}{0ex}}entity(e)\\ \phantom{\rule{1em}{0ex}}\Rightarrow alternateOf(e,e)\end{array}$

Suppose $ent=\mathit{\rho}(e)$. Clearly $e\in Entities$ and $thingOf(e)=thingOf(e)$, so $W,\mathit{\rho}\models alternateOf(e,e)$.

$\begin{array}{l}\mathrm{\forall}{e}_{1},{e}_{2},{e}_{3}.\text{}\\ \phantom{\rule{2em}{0ex}}alternateOf({e}_{1},{e}_{2})\wedge alternateOf({e}_{2},{e}_{3})\\ \phantom{\rule{1em}{0ex}}\Rightarrow alternateOf({e}_{1},{e}_{3})\end{array}$

Suppose $en{t}_{1}=\mathit{\rho}({e}_{1})$ and $en{t}_{2}=\mathit{\rho}({e}_{2})$ and $en{t}_{3}=\mathit{\rho}({e}_{3})$. Then by assumption $en{t}_{1}$, $en{t}_{2}$, and $en{t}_{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,\mathit{\rho}\models alternateOf({e}_{1},{e}_{3})$.

$\begin{array}{l}\mathrm{\forall}{e}_{1},{e}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}alternateOf({e}_{1},{e}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow alternateOf({e}_{2},{e}_{1})\end{array}$

Suppose $en{t}_{1}=\mathit{\rho}({e}_{1})$ and $en{t}_{2}=\mathit{\rho}({e}_{2})$. Then by assumption both $en{t}_{1}$ and $en{t}_{2}$ are in $Entities$ and $thingOf({e}_{1})=thingOf({e}_{2})$, as required to conclude $W,\mathit{\rho}\models alternateOf({e}_{2},{e}_{1})$.

$\begin{array}{l}\mathrm{\forall}{e}_{1},{e}_{2},{e}_{3}.\text{}\\ \phantom{\rule{2em}{0ex}}specializationOf({e}_{1},{e}_{2})\wedge specializationOf({e}_{2},{e}_{3})\\ \phantom{\rule{1em}{0ex}}\Rightarrow specializationOf({e}_{1},{e}_{3})\end{array}$

Suppose the conditions for specialization hold of $en{t}_{1}$ and $en{t}_{2}$ and for $en{t}_{2}$ and $en{t}_{3}$, where $en{t}_{1}=\mathit{\rho}({e}_{1})$ and $en{t}_{2}=\mathit{\rho}({e}_{2})$ and $en{t}_{3}=\mathit{\rho}({e}_{3})$. Then $lifetime({e}_{1})\subseteq lifetime({e}_{2})\subseteq lifetime({e}_{3})$. Moreover, $value(ob{j}_{2},attr)\supseteq value(ob{j}_{3},attr)$, and similarly $value(ob{j}_{1},attr)\supseteq value(ob{j}_{2},attr)$ so $value(ob{j}_{1},attr)\supseteq value(ob{j}_{3},attr)$. (TODO: How do we know ${e}_{3}\ne {e}_{1}$? Need strict ordering on entities in semantics.)

$\begin{array}{l}\mathrm{\forall}{e}_{1},{e}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}specializationOf({e}_{1},{e}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow alternateOf({e}_{1},{e}_{2})\end{array}$

If $en{t}_{1}=\mathit{\rho}({e}_{1})$ and $en{t}_{2}=\mathit{\rho}({e}_{2})$ are specializations, then $thingOf(en{t}_{1})=thingOf(en{t}_{2})$.

$\begin{array}{l}\mathrm{\forall}{e}_{1},attrs,{e}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}entity({e}_{1},attrs)\wedge specializationOf({e}_{2},{e}_{1})\\ \phantom{\rule{1em}{0ex}}\Rightarrow entity({e}_{2},attrs)\end{array}$

Suppose $en{t}_{1}=\mathit{\rho}({e}_{1})$ and $en{t}_{2}=\mathit{\rho}({e}_{2})$. Suppose $(att,v)$ is an attribute-value pair in $attrs$. Since $entity({e}_{1},attrs)$ holds, we know that $v\in value(en{t}_{1},att)$. Thus $v\in value(en{t}_{2},att)$ since $value(en{t}_{2},att)\supseteq value(en{t}_{1},att)$. Since this is the case for all attribute-value pairs in $attrs$, and since ${e}_{2}$ obviously denotes an entity, we can conclude $W,\mathit{\rho}\models entity(e,attrs$).

- The identifier field $id$ is a KEY for the $entity(id,attrs)$ statement.
- The identifier field $id$ is a KEY for the $activity(id,{t}_{1},{t}_{2},attrs)$ statement.
- The identifier field $id$ is a KEY for the $agent(id,attrs)$ statement.

- The identifier field $id$ is a KEY for the $wasGeneratedBy(id,e,a,t,attrs)$ statement.
- The identifier field $id$ is a KEY for the $used(id,a,e,t,attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasInformedBy(id,{a}_{2},{a}_{1},attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasStartedBy(id,{a}_{2},e,{a}_{1},t,attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasEndedBy(id,{a}_{2},e,{a}_{1},t,attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasInvalidatedBy(id,e,a,t,attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasDerivedFrom(id,{e}_{2},{e}_{1},a,{g}_{2},{u}_{1},attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasAttributedTo(id,e,ag,attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasAssociatedWith(id,a,ag,pl,attrs)$ statement.
- The identifier field $id$ is a KEY for the $actedOnBehalfOf(id,a{g}_{2},a{g}_{1},a,attrs)$ statement.
- The identifier field $id$ is a KEY for the $wasInfluencedBy(id,o2,o1,attrs)$ statement.

$\begin{array}{l}\mathrm{\forall}ge{n}_{1},ge{n}_{2},e,a,{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(ge{n}_{1},e,a,{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(ge{n}_{2},e,a,{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}=ge{n}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}in{v}_{1},in{v}_{2},e,a,{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasInvalidatedBy(in{v}_{1},e,a,{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(in{v}_{2},e,a,{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow in{v}_{1}=in{v}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}star{t}_{1},star{t}_{2},a,{e}_{1},{e}_{2},{a}_{0},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(star{t}_{1},a,{e}_{1},{a}_{0},{t}_{1},attr{s}_{1})\wedge wasStartedBy(star{t}_{2},a,{e}_{2},{a}_{0},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}=star{t}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}en{d}_{1},en{d}_{2},a,{e}_{1},{e}_{2},{a}_{0},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasEndedBy(en{d}_{1},a,{e}_{1},{a}_{0},{t}_{1},attr{s}_{1})\wedge wasEndedBy(en{d}_{2},a,{e}_{2},{a}_{0},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow en{d}_{1}=en{d}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}start,{a}_{1},{a}_{2},t,{t}_{1},{t}_{2},e,attrs,attr{s}_{1}.\text{}\\ \phantom{\rule{2em}{0ex}}activity({a}_{2},{t}_{1},{t}_{2},attrs)\wedge wasStartedBy(start,{a}_{2},e,{a}_{1},t,attr{s}_{1})\\ \phantom{\rule{1em}{0ex}}\Rightarrow {t}_{1}=t\end{array}$

$\begin{array}{l}\mathrm{\forall}end,{a}_{1},{a}_{2},t,{t}_{1},{t}_{2},e,attrs,attr{s}_{1}.\text{}\\ \phantom{\rule{2em}{0ex}}activity({a}_{2},{t}_{1},{t}_{2},attrs)\wedge wasEndedBy(end,{a}_{2},e,{a}_{1},t,attr{s}_{1})\\ \phantom{\rule{1em}{0ex}}\Rightarrow {t}_{2}=t\end{array}$

$\begin{array}{l}\mathrm{\forall}start,end,a,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(start,a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(end,a,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow start\u2aafend\end{array}$

$\begin{array}{l}\mathrm{\forall}star{t}_{1},star{t}_{2},a,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(star{t}_{1},a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasStartedBy(star{t}_{2},a,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}\u2aafstar{t}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}en{d}_{1},en{d}_{2},a,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasEndedBy(en{d}_{1},a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(en{d}_{2},a,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow en{d}_{1}\u2aafen{d}_{2}\end{array}$

- $\begin{array}{l}\mathrm{\forall}start,use,a,{e}_{1},{e}_{2},{a}_{1},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(start,a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge used(use,a,{e}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow start\u2aafuse\end{array}$
- $\begin{array}{l}\mathrm{\forall}use,end,a,{e}_{1},{e}_{2},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}used(use,a,{e}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(end,a,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow use\u2aafend\end{array}$

- $\begin{array}{l}\mathrm{\forall}start,gen,{e}_{1},{e}_{2},a,{a}_{1},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(start,a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(gen,{e}_{2},a,{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow start\u2aafgen\end{array}$
- $\begin{array}{l}\mathrm{\forall}gen,end,e,{e}_{1},a,{a}_{1},t,{t}_{1},attrs,attr{s}_{1}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(gen,e,a,t,attrs)\wedge wasEndedBy(end,a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\\ \phantom{\rule{1em}{0ex}}\Rightarrow gen\u2aafend\end{array}$

$\begin{array}{l}\mathrm{\forall}id,start,end,{a}_{1},{a}_{1}^{\prime},{a}_{2},{a}_{2}^{\prime},{e}_{1},{e}_{2},{t}_{1},{t}_{2},attrs,attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasInformedBy(id,{a}_{2},{a}_{1},attrs)\wedge wasStartedBy(start,{a}_{1},{e}_{1},{a}_{1}^{\prime},{t}_{1},attr{s}_{1})\wedge wasEndedBy(end,{a}_{2},{e}_{2},{a}_{2}^{\prime},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow start\u2aafend\end{array}$

$\begin{array}{l}\mathrm{\forall}gen,inv,e,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(inv,e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow gen\u2aafinv\end{array}$

$\begin{array}{l}\mathrm{\forall}gen,use,e,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge used(use,{a}_{2},e,{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow gen\u2aafuse\end{array}$

$\begin{array}{l}\mathrm{\forall}use,inv,{a}_{1},{a}_{2},e,{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}used(use,{a}_{1},e,{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(inv,e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow use\u2aafinv\end{array}$

$\begin{array}{l}\mathrm{\forall}ge{n}_{1},ge{n}_{2},e,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(ge{n}_{1},e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(ge{n}_{2},e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}\u2aafge{n}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}in{v}_{1},in{v}_{2},e,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasInvalidatedBy(in{v}_{1},e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(in{v}_{2},e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow in{v}_{1}\u2aafin{v}_{2}\end{array}$

In this constraint, $a$,$ge{n}_{2}$, or $us{e}_{1}$ must not be placeholders -.

$\begin{array}{l}\mathrm{\forall}d,{e}_{1},{e}_{2},a,ge{n}_{2},us{e}_{1},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(a)\wedge notNull(ge{n}_{2})\wedge notNull(us{e}_{1})\wedge wasDerivedFrom(d,{e}_{2},{e}_{1},a,ge{n}_{2},us{e}_{1},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow us{e}_{1}\u2aafge{n}_{2}\end{array}$In this constraint, any of $a$,$g$, or $u$ may be placeholders -.

$\begin{array}{l}\mathrm{\forall}d,ge{n}_{1},ge{n}_{2},{e}_{1},{e}_{2},a,{a}_{1},{a}_{2},g,u,{t}_{1},{t}_{2},attrs,attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasDerivedFrom(d,{e}_{2},{e}_{1},a,g,u,attrs)\wedge wasGeneratedBy(ge{n}_{1},{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(ge{n}_{2},{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}\prec ge{n}_{2}\end{array}$- $\begin{array}{l}\mathrm{\forall}gen,start,e,a,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasStartedBy(start,a,e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow gen\u2aafstart\end{array}$
- $\begin{array}{l}\mathrm{\forall}start,inv,e,a,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(start,a,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(inv,e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow start\u2aafinv\end{array}$

- $\begin{array}{l}\mathrm{\forall}gen,end,e,a,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(gen,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(end,a,e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow gen\u2aafend\end{array}$
- $\begin{array}{l}\mathrm{\forall}end,inv,e,a,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasEndedBy(end,a,e,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(inv,e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow end\u2aafinv\end{array}$

$\begin{array}{l}\mathrm{\forall}ge{n}_{1},ge{n}_{2},{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}specializationOf({e}_{2},{e}_{1})\wedge wasGeneratedBy(ge{n}_{1},{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(ge{n}_{2},{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}\u2aafge{n}_{2}\end{array}$

$\begin{array}{l}\mathrm{\forall}in{v}_{1},in{v}_{2},{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}specializationOf({e}_{1},{e}_{2})\wedge wasInvalidatedBy(in{v}_{1},{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(in{v}_{2},{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow in{v}_{1}\u2aafin{v}_{2}\end{array}$

In the following inferences, $pl$ may be a placeholder -.

- $\begin{array}{l}\mathrm{\forall}assoc,star{t}_{1},in{v}_{2},ag,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasAssociatedWith(assoc,a,ag,pl,attrs)\wedge wasStartedBy(star{t}_{1},a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(in{v}_{2},ag,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}\u2aafin{v}_{2}\end{array}$
- $\begin{array}{l}\mathrm{\forall}assoc,ge{n}_{1},en{d}_{2},ag,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasAssociatedWith(assoc,a,ag,pl,attrs)\wedge wasGeneratedBy(ge{n}_{1},ag,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(en{d}_{2},a,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}\u2aafen{d}_{2}\end{array}$
- $\begin{array}{l}\mathrm{\forall}assoc,star{t}_{1},en{d}_{2},ag,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasAssociatedWith(assoc,a,ag,pl,attrs)\wedge wasStartedBy(star{t}_{1},a,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(en{d}_{2},ag,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}\u2aafen{d}_{2}\end{array}$
- $\begin{array}{l}\mathrm{\forall}assoc,star{t}_{1},en{d}_{2},ag,{e}_{1},{e}_{2},{a}_{1},{a}_{2},{t}_{1},{t}_{2},attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasAssociatedWith(assoc,a,ag,pl,attrs)\wedge wasStartedBy(star{t}_{1},ag,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(en{d}_{2},a,{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}\u2aafen{d}_{2}\end{array}$

- $\begin{array}{l}\mathrm{\forall}att,ge{n}_{1},ge{n}_{2},e,{a}_{1},{a}_{2},{t}_{1},{t}_{2},ag,attrs,attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasAttributedTo(att,e,ag,attrs)\wedge wasGeneratedBy(ge{n}_{1},ag,{a}_{1},{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(ge{n}_{2},e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}\u2aafge{n}_{2}\end{array}$
- $\begin{array}{l}\mathrm{\forall}att,star{t}_{1},ge{n}_{2},e,{e}_{1},{a}_{1},{a}_{2},ag,{t}_{1},{t}_{2},attrs,attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}wasAttributedTo(att,e,ag,attrs)\wedge wasStartedBy(star{t}_{1},ag,{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasGeneratedBy(ge{n}_{2},e,{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}\u2aafge{n}_{2}\end{array}$

- $\begin{array}{l}\mathrm{\forall}del,ge{n}_{1},in{v}_{2},a{g}_{1},a{g}_{2},a,{a}_{1},{a}_{2},{t}_{1},{t}_{2},attrs,attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}actedOnBehalfOf(del,a{g}_{2},a{g}_{1},a,attrs)\wedge wasGeneratedBy(ge{n}_{1},a{g}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasInvalidatedBy(in{v}_{2},a{g}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow ge{n}_{1}\u2aafin{v}_{2}\end{array}$
- $\begin{array}{l}\mathrm{\forall}del,star{t}_{1},en{d}_{2},a{g}_{1},a{g}_{2},a,{a}_{1},{a}_{2},{e}_{1},{e}_{2},{t}_{1},{t}_{2},attrs,attr{s}_{1},attr{s}_{2}.\text{}\\ \phantom{\rule{2em}{0ex}}actedOnBehalfOf(del,a{g}_{2},a{g}_{1},a,attrs)\wedge wasStartedBy(star{t}_{1},a{g}_{1},{e}_{1},{a}_{1},{t}_{1},attr{s}_{1})\wedge wasEndedBy(en{d}_{2},a{g}_{2},{e}_{2},{a}_{2},{t}_{2},attr{s}_{2})\\ \phantom{\rule{1em}{0ex}}\Rightarrow star{t}_{1}\u2aafen{d}_{2}\end{array}$

- $\begin{array}{l}\mathrm{\forall}e,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}entity(e,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}ag,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}agent(ag,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(ag,agent)\end{array}$
- $\begin{array}{l}\mathrm{\forall}a,{t}_{1},{t}_{2},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}activity(a,{t}_{1},{t}_{2},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a,activity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}u,a,e,t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}used(u,a,e,t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a,activity)\wedge typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}g,a,e,t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasGeneratedBy(g,e,a,t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a,activity)\wedge typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}inf,{a}_{2},{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasInformedBy(inf,{a}_{2},{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({a}_{1},activity)\wedge typeOf({a}_{2},activity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}start,{a}_{2},e,{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasStartedBy(start,{a}_{2},e,{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({a}_{1},activity)\wedge typeOf({a}_{2},activity)\wedge typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}end,{a}_{2},e,{a}_{1},t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasEndedBy(end,{a}_{2},e,{a}_{1},t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({a}_{1},activity)\wedge typeOf({a}_{2},activity)\wedge typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}inv,a,e,t,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasInvalidatedBy(inv,e,a,t,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a,activity)\wedge typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{e}_{2},{e}_{1},a,{g}_{2},{u}_{1},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(a)\wedge notNull({g}_{2})\wedge notNull({u}_{1})\wedge wasDerivedFrom(id,{e}_{2},{e}_{1},a,{g}_{2},{u}_{1},attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({e}_{2},entity)\wedge typeOf({e}_{1},activity)\wedge typeOf(a,activity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{e}_{2},{e}_{1},attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasDerivedFrom(id,{e}_{2},{e}_{1},-,-,-,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({e}_{2},entity)\wedge typeOf({e}_{1},activity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,e,ag,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasAttributedTo(id,e,ag,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(e,entity)\wedge typeOf(ag,agent)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,a,ag,pl,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(pl)\wedge wasAssociatedWith(id,a,ag,pl,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a,activity)\wedge typeOf(ag,agent)\wedge typeOf(pl,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,a,ag,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}wasAssociatedWith(id,a,ag,-,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a,activity)\wedge typeOf(ag,agent)\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,a{g}_{2},a{g}_{1},a,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}actedOnBehalfOf(id,a{g}_{2},a{g}_{1},a,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(a{g}_{2},agent)\wedge typeOf(a{g}_{1},agent)\wedge typeOf(a,activity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}{e}_{2},{e}_{1}.\text{}\\ \phantom{\rule{2em}{0ex}}alternateOf({e}_{2},{e}_{1})\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({e}_{2},entity)\wedge typeOf({e}_{1},entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}{e}_{2},{e}_{1}.\text{}\\ \phantom{\rule{2em}{0ex}}specializationOf({e}_{2},{e}_{1})\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf({e}_{2},entity)\wedge typeOf({e}_{1},entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}c,e.\text{}\\ \phantom{\rule{2em}{0ex}}hadMember(c,e)\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(c,Collection)\wedge typeOf(e,entity)\end{array}$
- $\begin{array}{l}\mathrm{\forall}c.\text{}\\ \phantom{\rule{2em}{0ex}}entity(c,[prov:type=prov:emptyCollection]))\\ \phantom{\rule{1em}{0ex}}\Rightarrow typeOf(c,entity)\wedge typeOf(c,Collection)\wedge typeOf(c,EmptyCollection)\end{array}$

Each typing constraint follows immediately from well-formedness criteria marked [WF] in the corresponding semantics for formulas.

- $\begin{array}{l}\mathrm{\forall}id,{e}_{1},{e}_{2},g,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(g)\wedge wasDerivedFrom(id,{e}_{2},{e}_{1},-,g,-,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{e}_{1},{e}_{2},u,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(u)\wedge wasDerivedFrom(id,{e}_{2},{e}_{1},-,-,u,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$
- $\begin{array}{l}\mathrm{\forall}id,{e}_{1},{e}_{2},g,u,attrs.\text{}\\ \phantom{\rule{2em}{0ex}}notNull(g)\wedge notNull(u)\wedge wasDerivedFrom(id,{e}_{2},{e}_{1},-,g,u,attrs)\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$

Each part follows from the fact that the semantics of $wasDerivedFrom$ only allows formulas to hold when either all three of $a,g,u$ are $-$ (denoting $\mathrm{\perp}$) or none of them are.

$\begin{array}{l}\mathrm{\forall}e.\text{}\\ \phantom{\rule{2em}{0ex}}specializationOf(e,e)\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$

This follows from the fact that in the semantics of $specializationOf$, the two entities denoted by the first and second arguments are required to be distinct.

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:

$\begin{array}{l}\mathrm{\forall}id,{a}_{1},\dots ,{a}_{m},{b}_{1},\dots ,{b}_{n}.\text{}\\ \phantom{\rule{2em}{0ex}}r(id,{a}_{1},\dots ,{a}_{m})\wedge s(id,{b}_{1},\dots ,{b}_{n})\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$This follows from the assumption that the different classes of interactions are disjoint sets, characterized by their types.

For each $p\in \{entity,activity,agent\}$ and each $r\in \{used,wasGeneratedBy,wasInvalidatedBy,wasStartedBy,wasEndedBy,wasInformedBy,wasAttributedTo,wasAssociatedWith,actedOnBehalfOf\}$, the following constraint holds:

$\begin{array}{l}\mathrm{\forall}id,{a}_{1},\dots ,{a}_{m},{b}_{1},\dots ,{b}_{n}.\text{}\\ \phantom{\rule{2em}{0ex}}p(id,{a}_{1},\dots ,{a}_{m})\wedge r(id,{b}_{1},\dots ,{b}_{n})\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$This follows from the assumption that interactions are distinct from other objects (entities, activities or agents).

$\begin{array}{l}\mathrm{\forall}id.\text{}\\ \phantom{\rule{2em}{0ex}}typeOf(id,entity)\wedge typeOf(id,activity)\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$

This follows from the assumption that entities and activities are disjoint.

$\begin{array}{l}\mathrm{\forall}c,e.\text{}\\ \phantom{\rule{2em}{0ex}}hasMember(c,e)\wedge typeOf(c,EmptyCollection)\\ \phantom{\rule{1em}{0ex}}\Rightarrow False\end{array}$

Above we have presented arguments for the soundness of the constraints and inferences with respect to the naive semantics. Here, we relate the notions of validity and normal form defined in PROV-CONSTRAINTS to the semantics. Our main observation is:

- If $I$ is an instance and $W\models I$ and ${I}^{\prime}$ is obtained from $I$ by applying one of the PROV inferences, then $W\models {I}^{\prime}$.
- If $I$ is an instance and $W\models I$ then $I$ has a normal form ${I}^{\prime}$ and $W\models {I}^{\prime}$.
- If $I$ is a normal form and $W\models I$ then $I$ satisfies all of the ordering, typing and impossibility constraints.
- If $W\models I$ then $I$ is valid.

For part 1, the arguments are as in the previous section.

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}^{\prime}$.

For part 3, the arguments are as in the previous section for each constraint.

Finally, for part 4, suppose $W\models I$. Then $W\models {I}^{\prime}$ where ${I}^{\prime}$ is the normal form of $I$ by part 2. By part 3, ${I}^{\prime}$ satisfies all of the remaining constraints, so $I$ is valid.

In this section we relate PROV instances and validation as specified in PROV-CONSTRAINTS to certain models, which we call syntactic models. We will show that valid PROV instances correspond to syntactic models of the first-order theory of PROV.

Note

Explain how to translate PROV formulas to purely relational
formulas.

This document has been produced by the PROV Working Group, and its contents reflect extensive discussion within the Working Group as a whole.

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.

Members of the PROV Working Group at the time of publication of this document were: Ilkay Altintas (Invited expert), Reza B'Far (Oracle Corporation), Khalid Belhajjame (University of Manchester), James Cheney (University of Edinburgh, School of Informatics), Sam Coppens (IBBT), David Corsar (University of Aberdeen, Computing Science), Stephen Cresswell (The National Archives), Tom De Nies (IBBT), Helena Deus (DERI Galway at the National University of Ireland, Galway, Ireland), Simon Dobson (Invited expert), Martin Doerr (Foundation for Research and Technology - Hellas(FORTH)), Kai Eckert (Invited expert), Jean-Pierre EVAIN (European Broadcasting Union, EBU-UER), James Frew (Invited expert), Irini Fundulaki (Foundation for Research and Technology - Hellas(FORTH)), Daniel Garijo (Universidad Politécnica de Madrid), Yolanda Gil (Invited expert), Ryan Golden (Oracle Corporation), Paul Groth (Vrije Universiteit), Olaf Hartig (Invited expert), David Hau (National Cancer Institute, NCI), Sandro Hawke (W3C/MIT), Jörn Hees (German Research Center for Artificial Intelligence (DFKI) Gmbh), Ivan Herman, (W3C/ERCIM), Ralph Hodgson (TopQuadrant), Hook Hua (Invited expert), Trung Dong Huynh (University of Southampton), Graham Klyne (University of Oxford), Michael Lang (Revelytix, Inc.), Timothy Lebo (Rensselaer Polytechnic Institute), James McCusker (Rensselaer Polytechnic Institute), Deborah McGuinness (Rensselaer Polytechnic Institute), Simon Miles (Invited expert), Paolo Missier (School of Computing Science, Newcastle university), Luc Moreau (University of Southampton), James Myers (Rensselaer Polytechnic Institute), Vinh Nguyen (Wright State University), Edoardo Pignotti (University of Aberdeen, Computing Science), Paulo da Silva Pinheiro (Rensselaer Polytechnic Institute), Carl Reed (Open Geospatial Consortium), Adam Retter (Invited Expert), Christine Runnegar (Invited expert), Satya Sahoo (Invited expert), David Schaengold (Revelytix, Inc.), Daniel Schutzer (FSTC, Financial Services Technology Consortium), Yogesh Simmhan (Invited expert), Stian Soiland-Reyes (University of Manchester), Eric Stephan (Pacific Northwest National Laboratory), Linda Stewart (The National Archives), Ed Summers (Library of Congress), Maria Theodoridou (Foundation for Research and Technology - Hellas(FORTH)), Ted Thibodeau (OpenLink Software Inc.), Curt Tilmes (National Aeronautics and Space Administration), Craig Trim (IBM Corporation), Stephan Zednik (Rensselaer Polytechnic Institute), Jun Zhao (University of Oxford), Yuting Zhao (University of Aberdeen, Computing Science).

- [Logic]
- W. E. Johnson. Logic: Part III.1924. URL: http://www.ditext.com/johnson/intro-3.html
- [PROV-AQ]
- Graham Klyne; Paul Groth; eds. Provenance Access and Query. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-aq-20130312/
- [PROV-CONSTRAINTS]
- James Cheney; Paolo Missier; Luc Moreau; eds. Constraints of the PROV Data Model. 12 March 2013, W3C Proposed Recommendation. URL: http://www.w3.org/TR/2013/PR-prov-constraints-20130312/
- [PROV-DC]
- Daniel Garijo; Kai Eckert; eds. Dublin Core to PROV Mapping. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-dc-20130312/
- [PROV-DICTIONARY]
- Tom De Nies; Sam Coppens; eds. PROV Dictionary. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-dictionary-20130312/
- [PROV-DM]
- Luc Moreau; Paolo Missier; eds. PROV-DM: The PROV Data Model. 12 March 2013, W3C Proposed Recommendation. URL: http://www.w3.org/TR/2013/PR-prov-dm-20130312/
- [PROV-LINKS]
- Luc Moreau; Timothy Lebo; eds. Linking Across Provenance Bundles. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-links-20130312/
- [PROV-N]
- Luc Moreau; Paolo Missier; eds. PROV-N: The Provenance Notation. 12 March 2013, W3C Proposed Recommendation. URL: http://www.w3.org/TR/2013/PR-prov-n-20130312/
- [PROV-O]
- Timothy Lebo; Satya Sahoo; Deborah McGuinness; eds. PROV-O: The PROV Ontology. 12 March 2013, W3C Proposed Recommendation. URL: http://www.w3.org/TR/2013/PR-prov-o-20130312/
- [PROV-OVERVIEW]
- Paul Groth; Luc Moreau; eds. PROV-OVERVIEW: An Overview of the PROV Family of Documents. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-overview-20130312/
- [PROV-PRIMER]
- Yolanda Gil; Simon Miles; eds. PROV Model Primer. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-primer-20130312/
- [PROV-XML]
- Hook Hua; Curt Tilmes; Stephan Zednik; eds. PROV-XML: The PROV XML Schema. 12 March 2013, Working Draft. URL: http://www.w3.org/TR/2013/WD-prov-xml-20130312/