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, 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 valid PROV
instances (in the sense of PROV-CONSTRAINTS) correspond to satisfiable
theories.
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.

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

The Provenance Working Group encourages implementations that make use of or extend the semantics in this document. Although work on this document by the Provenance Working Group is complete, errors may be recorded in the errata or and these may be addressed in future revisions.

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. [[PROV-DM]] 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 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 specifications 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 provide a semantics that satisfies all
of the constraints on valid PROV instances, and such that valid PROV
instances correspond to satisfiable theories: every valid instance has
a model, and vice versa.

The 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 semantics, this document shows that the operational presentation of PROV validity checking is equivalent 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, such as named bundles. The semantics do not cover general 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 discuss only PROV instances and not PROV documents. The semantics of extensions of PROV, such as dictionaries [[PROV-DICTIONARY]] and linking across bundles [[PROV-LINKS]], are beyond the scope of this document.

This document has been reviewed by the Working Group, but the theorems and proofs have not been formally peer-reviewed in the sense of an academic paper. Thus, the Working Group believes this document is an appropriate starting point for future study of the semantics of PROV, but further work may be needed.

- 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 results relating PROV-CONSTRAINTS validation to the semantics, including soundness and a weak form of completeness: a PROV instance is valid if and only if it has a model.

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 researchers 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 are viewed as variables from the point of view of logic. Identifiers denote objects, and two different identifiers $x$ and $y$ may denote equal or different objects. 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 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(Values)$, that is, the set of sets of values. Thus, we can use the empty set to stand for an undefined value and $\{a,b\}$ to stand for the set of values of a two-valued attribute.

We assume an ordered set $(Times,\leq)$ of time instants, where $Times \subseteq Values$ and $\leq$ is a linear order.

The following atomic formulas correspond to the statements of PROV-DM. We assume that definitions 1-4 of PROV-CONSTRAINTS have been applied in order to expand all optional parameters; thus, we use uniform notation $r(id,a_1,\ldots,a_n)$ instead of the semicolon notation $r(id;a_1,\ldots,a_n)$.

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.

$$ \newcommand{\precedes}{~\mathrel{\textrm{precedes}}~} \newcommand{\strictlyPrecedes}{~\mathrel{\textrm{strictlyPrecedes}}~} \begin{array}{rcl} atomic\_formula & {::=}& element\_formula\\ & | & relation\_formula\\ & | & auxiliary\_formula\\ element\_formula &{::=} &entity(id,attrs) \\ & |& activity(id,st,et,attrs)\\ & |& agent(id,attrs)\\ relation\_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,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 \strictlyPrecedes y\\ & | & x \precedes y\\ & | & notNull(x)\\ & | & typeOf(x,ty)\\ attrs &::=& [attr_1 = v_1, \ldots,attr_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 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 incorporate $mentionOf$ or other cross-instance assertions, and if so this semantics should be generalized in order to provide a rationale for such an extension and to establish the soundness of constraints associated with $mentionOf$.

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

$$ \begin{array}{rcl} \phi &{::=}& atomic\_formula\\ & | & True\\ & | & False\\ &|&x = y\\ & | & \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} $$ In this section we define mathematical structures $W$ that can be used to
interpret PROV formulas and instances. A structure consists of a
collection of sets, functions and relations. The components of a
structure $W$ are given in the rest of the section in
*components*, highlighted in boxes.

We use the term "component" here in a different sense than in PROV-DM. Here, the components are parts of a large definition, whereas PROV-DM defines six components that group different parts of the PROV data model.

*Things* is a set of things in the situation being modeled.
Each thing has an associated set of $Events$ and attributes whose
values can change over time. Different kinds of $Events$ are specified further below.

To model this, a structure $W$ includes:

- a set $Things$ of things
- a set $Events$ of events
- a function $events : Things \to P(Events)$ from things to associated sets of events.
- a function $value : Things \times Attributes \times Events \to P(Values)$ giving the possible values of each attribute of a $Thing$ at the instant of a given event.
- Attributes are only defined during the events of a thing, that is, $value(T,a,evt) \neq \emptyset$ implies $evt \in events(T)$.

The range of $value$ is the set $P(Values)$, indicating that $value$ is essentially a multi-valued function that returns a set of values (possibly empty). When $value(x,a,evt) = \emptyset$, we say that attribute $a$ is undefined for $x$ at event $evt$.

Note that this description does not say what the structure of a $Thing$ is, only how it may be described in terms of its events 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 $\pi$. All that matters from our point of view is that we know how to map the $Thing$ to its events and attribute mapping.

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

$Things$ are associated with certain kinds of $Objects$ called $Entities$, defined in the next subsection. Specifically, the function $thingOf$ associates an $Entity$ to a $Thing$.

$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 events. Others correspond to agents, activities, or identifiable interactions among them.

In this section, we detail the different subsets of $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 set of events 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 $events : Objects \to P(Events)$ from objects to associated sets of events.
- a function $value : Objects \times Attributes \to P(Values)$.

Intuitively, $events(e)$ is the set of events in which $e$ participated. The set $value(e,a)$ is the set of values of attribute $a$ during the object's events.

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 associated events. 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 fixes some aspects of a
thing. We assume:

- a set $Entities \subseteq Objects$ of entities, disjoint from $Activities$ below.
- a function $thingOf : Entities \to Things$ that associates each $Entity$ $e$ with a $Thing$, such that $events(e) \subseteq events(thingOf(e))$ and for each $evt \in events(e)$ and for each attribute $a$ we have $value(e,a) \subseteq value(thingOf(e),a,evt)$.

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

Furthermore, all of the attribute values of the entity must be present in the associated thing throughout the events of the entity. For example, suppose $value(thingOf(e),a,evt)$ is $\{1\}$ at some event $ evt \in events(e)$ and $value(thingOf(e),a,evt') = \{2\}$ at some other event $evt'$. Then $value(e,a)$ must be $\emptyset$ 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,evt)$ whenever $evt \in events(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 events. 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.

Only $Entities$ are associated with $Things$, and this association 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.

We identify another specific subset of the entities called
*collections*, with the following associated structure:

- A set $Collections \subseteq Entities$
- A membership function $members : Collections \to P( Entities)$ mapping each collection to its set of members.

An *activity* is an object corresponding to a continuing
process rather than an evolving thing. We introduce:

- A set $Activities \subseteq Objects$ of activities.
- Functions $startTime : Activities \to Times$ and $endTime :Activities \to Times$ giving the start and end time of each activity.
- Activities are disjoint from Entities: $Entities\cap Activities = \emptyset$.

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 $Influences \subseteq Objects$ which has disjoint subsets $Events$ connecting entities and activities, $Associations$ between agents and activities, $Attributions$ between entities and agents, $Communications$ between pairs of activities, $Delegations$ between pairs of agents, and $Derivations$ that describe chains of generation and usage steps. These kinds of influences are discussed further below. Influences are disjoint from entities, activities and agents.

- A set $Influences = Events \cup Associations \cup Communications \cup Delegations \cup Derivations \subseteq Objects$
- The sets $Events$, $Associations$, $Communications$, $Delegations$ and $Derivations$ are all pairwise disjoint.
- Influences are disjoint from entities, agents and activities: $Influences \cap (Entities \cup Activities \cup Agents) = \emptyset$
- An associated function $influenced : Influences \to Objects \times Objects$ giving the source and target of each influence.

An $Event$ is an instantaneous influence that relates an activity to an entity (either of which could also be an agent). Events have types including usage, generation, invalidation, starting and ending. Events are instantaneous. We introduce:

- A set $Events \subseteq Influences$ of events, partitioned into disjoint subsets $Starts, Ends, Generations, Usages, Invalidations$.
- A function $time : Events \to Times$.
- A quasi-ordering on events $\preceq \subset Events \times Events$. We write $e \prec e'$ when $e \preceq e'$ and $e' \not\preceq e$ hold.
- A function $started : Starts \to Activities \times Entities \times Activities$, such that $started(start) = (a,e,a')$ implies $start \in events(a) \cap events(e) \cap events(a')$.
- A function $ended : Ends \to Activities \times Entities \times Activities$, such that $ended(end) = (a,e,a')$ implies $end \in events(a) \cap events(e) \cap events(a')$.
- A function $used : Usages \to Activities \times Entities$ such that $used(use) = (a,e)$ implies $use \in events(a) \cap events(e)$.
- A function $generated : Generations \to Entities \times Activities$ such that $generated(gen) = (a,e)$ implies $gen \in events(a) \cap events(e)$.
- A function $invalidated : Invalidations \to Entities \times Activities$ such that $invalidated(inv) = (a,e)$ implies $inv \in events(a) \cap events(e)$.

An $Association$ is an influence relating an agent to an activity and optional plan. To model associations, we introduce:

A set $Associations \subseteq Influences$ with associated function $associatedWith : Associations \to Agents \times Activities \times Plans_\bot$.

An $Attribution$ is an influence relating an entity to an agent. To model attributions, we introduce:

A set $Attributions \subseteq Influences$ with associated function $attributedTo : Attributions \to Entities \times Agents$.

A $Communication$ is an influence indicating exchange of information between activities. To model communications, we introduce:

A set $Communications \subseteq Influences$ with associated function $communicated : Communications \to Activities \times Activities$.

A $Delegation$ is an influence relating two agents. To model delegations, we introduce:

A set $Delegations \subseteq Influences$ and associated function $actedFor : Delegations \to Agents \times Agents \times Activities$

A $Derivation$ is an influence chaining one or more
generation and use steps. To model derivations, we introduce an
auxiliary notion of *derivation path*. These paths are of the form

where the $ent_i$ are entities, $act_i$ are activities, $g_i$ are generations, and $u_i$ are usages.

Formally, we consider the (regular) language:

$$DerivationPaths = Entities \cdot (Generations \cdot Activities \cdot Usages \cdot Entities)^+$$with the constraints that for each derivation path:

- for each substring $ent\cdot g \cdot act$ we have $generated(g) = (ent,act)$, and
- for each substring $act \cdot u \cdot ent$ we have $used(u) = (act,ent)$.

A set $Derivations \subseteq Influences$ with an associated function $derivationPath : Derivations \to DerivationPaths$ linking each derivation to a derivation path.

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 path, identified by different derivations $d \in Derivations$.

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 associated with derivation paths, it is not sound to infer the existence of a derivation from the existence of an alternating generation/use chain.

The reason why we need paths and not just individual derivation steps is to reflect that $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ formulas can represent multiple derivation steps. However, there is no way to force a derivation to take multiple steps. Any valid PROV instance has a model in which all derivation paths are one-step.

Above we have stated some properties of the components. We impose some additional properties that relate several components, as follows:

- If $generated(g) = (e,a_1)$ and $used(u) = (a_2,e)$ then there exists $c \in Communications$ such that $communicated(c) = (a_2,a_1)$.
- If $e \in Entities$ then there exist $gen,inv,a,a'$ such that $generated(gen) = (e,a)$ and $invalidated(inv) = (e,a')$.
- If $started(start) = (a_2,e,a_1)$ then there exists $gen$ such that $generated(gen) = (e,a_1)$.
- If $ended(end) = (a_2,e,a_1)$ then there exists $gen$ such that $generated(gen) = (e,a_1)$.
- If $d \in Derivations$ and $prov:Revision \in value(d,prov:type)$ and there exists $w \in (Generations \cup Activities \cup Uses \cup Entities)^* $ such that $derivationPath(deriv) = e_2 \cdot w \cdot e_1 \in DerivationPaths$ then $thingOf(e_1) = thingOf(e_2)$.
- If $attributedTo(att) = (e,ag)$ then there exist $gen$, $assoc$ and $a$ such that $generated(gen) = (e,a)$ and $associatedWith(assoc) = (a,ag)$.
- If $actedFor(deleg) = (ag_2,ag_1,act)$ then there exist $assoc_1,assoc_2,pl_1,pl_2$ such that $associatedWith(assoc_1) = (ag_1,act,pl_1)$ and $associatedWith(assoc_2) = (ag_2,act,pl_2)$.
- If $generated(id) = (e,a)$ then $influenced(id) = (e,a)$.
- If $used(id) = (e,a)$ then $influenced(id) = (e,a)$.
- If $communicated(id) = (a_2,a_1)$ then $influenced(id) = (a_2,a_1)$.
- If $started(id) = (a_2,e,a_1)$ then $influenced(id) = (a_2,e)$.
- If $ended(id) = (a_2,e,a_1)$ then $influenced(id) = (a_2,e)$.
- If $invalidated(id) = (e,a)$ then $influenced(id) = (e,a)$.
- If $derivationPath(id) = e_2 \cdot w \cdot e_1$ then $influenced(id) = (e_2,e_1)$.
- If $attributedTo(id) = (e,ag)$ then $influenced(id) = (e,ag)$.
- If $associatedWith(id) = (a,ag,pl)$ then $influenced(id) = (a,ag)$.
- If $actedFor(id) = (ag_2,ag_1)$ then $influenced(id) = (ag_2,ag_1)$.
- If $generated(gen) = (e,a) = generated(gen')$ then $gen = gen'$.
- If $invalidated(inv) = (e,a) = invalidated(inv')$ then $inv=inv'$.
- If $started(st) = (a,e_1,a')$ and $started(st') = (a,e_2,a')$ then $st=st'$.
- If $ended(end) = (a,e_1,a')$ and $ended(end') = (a,e_2,a')$ then $end=end'$.
- If $started(st) = (a,e,a')$ then $st \preceq evt$ for all $evt \in events(a) - Invalidations$.
- If $ended(end) = (a,e,a') $ then $evt \preceq end$ for all $evt \in events(a) - Invalidations$.
- If $generated(gen) = (e,a)$ then $gen \preceq evt$ for all $evt \in events(e)$.
- If $invalidated(inv) = (e,a)$ then $evt\preceq inv$ for all $evt \in events(e)$.
- For any derivation $deriv$, with path $derivationPath(deriv) = w$, if $e_2 \cdot g \cdot a \cdot u \cdot e_1 $ is a substring of $w$ where $e_1,e_2 \in Entities$, $g \in Generations$, $u \in Usages$ and $a \in Activities$ then $u \preceq g$.
- For any derivation $deriv$, with path $derivationPath(deriv) = e_2 \cdot w \cdot e_1$, if $generated(gen_1) = (e_1,a_1)$ and $generated(gen_2) = (e_2,a_2)$ then $gen_1 \prec gen_2$.
- If $associatedWith(assoc) = (a,ag,pl)$ and $started(start) = (a,e_1,a_1)$ and $invalidated(inv) = (ag,a_2)$ then $start \preceq inv$.
- If $associatedWith(assoc) = (a,ag,pl)$ and $generated(gen) = (ag,a_1)$ and $ended(end) = (a,e_2,a_2)$ then $gen \preceq end$.
- If $associatedWith(assoc) = (a,ag,pl)$ and $started(start) = (a,e_1,a_1)$ and $ended(end) = (ag,e_2,a_2)$ then $start \preceq end$.
- If $associatedWith(assoc) = (a,ag,pl)$ and $started(start) = (ag,e_1,a_1)$ and $ended(end) = (a,e_2,a_2)$ then $start \preceq end$.
- If $attributedTo(attrib) = (e,ag)$ and $generated(gen_1) = (ag_1,a_1)$ and $generated(gen_2) = (e,a_2)$ then $gen_1 \preceq gen_2$.
- If $attributedTo(attrib) = (e,ag)$ and $started(start) = (ag_1,e_1,a_1)$ and $generated(gen) = (e,a_2)$ then $start \preceq gen$.
- If $actedFor(deleg) = (ag_2,ag_1,a)$ and $generated(gen) = (ag_1,a_1)$ and $invalidated(inv) = (ag_2,a_2)$ then $gen \preceq inv$.
- If $actedFor(deleg) = (ag_2,ag_1,a)$ and $started(start) = (ag_1,e_1,a_1)$ and $ended(end) = (ag_2,e_2,a_2)$ then $start \preceq end$.
- If $e \in Entity$ and $prov:emptyCollection \in value(e,prov:type)$ then $e \in Collections$ and $members(e) = \emptyset$.

These properties are called *axioms*, and they are
needed to ensure that the PROV-CONSTRAINTS inferences and
constraints hold in all structures.

Axioms 22 and 23 do not require that invalidation events originating from an activity follow the activity's start event(s) or precede its end event(s). This is because there is no such constraint in PROV-CONSTRAINTS. Arguably, there should be a constraint analogous to Constraint 34 that specifies that any invalidation event in which an activity participates must follow the activity's start event(s) and precede its end event(s).

Here, we exempt invalidations from axioms 22 and 23 in order to simplify the proof of weak completeness.

A *PROV structure* $W$ is a collection of sets, functions, and relations containing all of the above
described components and satisfying all of the associated properties
and axioms. 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.

Some features of PROV structures are relatively obvious or routine, corresponding directly to features of PROV and associated inferences. For example, the functions $used, generated, invalidated, started, ended$ mapping events to their associated entities or activities, and $communicated, associatedWith, attributedTo, actedFor$ associating other types of influences with appropriate data.

On the other hand, some features are more distinctive, and represent areas where formal modeling has been used to guide the development of PROV. Derivation paths are one such distinctive feature; they correspond to an intuition that derivations may describe one or multiple generation-use steps leading from one entity to another. Another distinctive feature is the use of $Things$, which correspond to changing, real-world things, as opposed to $Entities$, which correspond to limited views or perspectives on $Things$, with some fixed aspects. The semantic structures of $Things$ and $Entities$ provide a foundation for the $alternateOf$ and $specializationOf$ relations.

We need to link identifiers to the objects they denote. We do this using a function which we shall call an *interpretation*.
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 **not** change over time; only
$Objects$ can be denoted by $Identifiers$.

In what follows, let $W$ be a fixed structure with the associated sets and relations discussed in the previous section, and let $\rho$ 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 $\phi$, a structure $W$ and an interpretation $\rho$. 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:

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

In the semantics above, note that the domain of quantification is the set of $Objects$; that is, quantifiers range over entities, activities, agents, or influences (which are in turn further subdivided into types of influences). $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 $\{\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$.

We say that an object $obj$ matches attributes $[attr_1=val_1,...]$ in structure $W$ provided: for each attribute $attr_i$, we have $val_i \in W.value(obj,attr_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,\rho \models entity(id,attrs)$ holds if and only if:

- [WF] $id$ denotes an entity $ent = \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,\rho \models activity(id,st,et,attrs)$ holds if and only if:

- [WF] The identifier $id$ maps to an activity $act = \rho(id) \in Activities$.
- $\rho(st) \in Times$ is the activity's start time, that is: $startTime(act) = \rho(st)$.
- $\rho(et)$ is the activity's end time, that is: $endTime(act) = \rho(et)$.
- There exists $start,e,a$ such that $started(start) = (act,e,a)$, and for all such start events $startTime(act) = time(start).
- There exists $end,e',a'$ such that $ended(end) = (act,e',a')$, and for all such end events $endTime(act) = time(end)$.
- The attributes match: $match(W,act,attrs)$.

The above definition is complicated for two reasons. First, we need to ensure that every activity has a start and end event. Second, when an $activity$ formula is asserted, we need to make sure all of the associated start and end event times match.

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

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

- [WF] $id$ denotes an agent $ag = \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,\rho \models wasGeneratedBy(id,e,a,t,attrs)$ holds if and only if:

- [WF] The identifier $id$ denotes a generation event $evt = \rho(id) \in Generations$.
- [WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$.
- [WF] The identifier $a$ denotes an activity $act = \rho(a) \in Activities$.
- The event $evt$ occurred at time $\rho(t) \in Times$, i.e. $time(evt) = \rho(t)$.
- The activity $act$ generated $ent$ via $evt$, i.e. $generated(evt) = (ent,act)$.
- 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,\rho \models used(id,a,e,t,attrs)$ holds if and only if:

- [WF] The identifier $id$ denotes a usage event $evt = \rho(id) \in Usages$.
- [WF] The identifier $a$ denotes an activity $act = \rho(id) \in Activities$.
- [WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$.
- The event $evt$ occurred at time $\rho(t) \in Times$, i.e. $time(evt) = \rho(t)$.
- The activity $act$ used $obj$ via $evt$, i.e. $used(evt) = (act,ent)$.
- 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,\rho \models wasInvalidatedBy(id,e,a,t,attrs)$ holds if and only if:

- [WF] The identifier $id$ denotes an invalidation event $evt = \rho(id) \in Invalidations$.
- [WF] The identifier $e$ denotes an entity $ent = \rho(e) \in Entities$.
- [WF] The identifier $a$ denotes an activity $act = \rho(a) \in Activities$.
- The event $evt$ occurred at time $\rho(t) \in Times$, i.e. $time(evt) = \rho(t)$.
- The activity $act$ invalidated $ent$ via $evt$, i.e. $invalidated(evt) = (ent,act)$.
- The attribute values match: $match(W,evt,attrs)$.

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

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

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

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

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

A start formula $wasStartedBy(id,a_2,e,a_1,t,attrs)$ is interpreted as follows:

$W,\rho \models wasStartedBy(id,a_2,e,a_1,t,attrs)$ holds if and only if:

- [WF] $id$ denotes a start event $evt = \rho(id) \in Starts$.
- [WF] $a_2$ denotes an activity $act_2 = \rho(a_2) \in Activities$.
- [WF] $e$ denotes an entity $ent = \rho(e) \in Entities$.
- [WF] $a_1$ denotes an activity $act_1 = \rho(a_1) \in Activities$.
- The event happened at time $t$, that is, $\rho(t) = = time(evt)$.
- The activity $act_1$ started $act_2$ via entity $ent$: that is, $started(evt) = (act_2,ent,act_1)$.
- 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,\rho \models wasEndedBy(id,a_2,e,a_1,t,attrs)$ holds if and only if:

- [WF] $id$ denotes an end event $evt = \rho(id) \in Ends$.
- [WF] $a_2$ denotes an activity $act_2 = \rho(a_2)\in Activities$.
- [WF] $e$ denotes an entity $ent = \rho(e)\in Entities$.
- [WF] $a_1$ denotes an activity $act_1 = \rho(a_1)\in Activities$.
- The event happened at the end of $act_2$, that is, $\rho(t) = endTime(act_2) = time(evt)$.
- The activity $act_1$ ended $act_2$ via entity $ent$: that is, $ended(evt) = (act_2,ent,act_1)$.
- The attributes match: $match(W,evt,attrs)$.

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

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

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

A communication formula $wasInformedBy(id,a_2,a_2,attrs)$ is interpreted as follows:

$W,\rho \models wasInformedBy(id,a_2,a_1,attrs)$ holds if and only if:

- [WF] $id$ denotes a communication $comm = \rho(id) \in Communications$.
- [WF] $a_1,a_2$ denote activities $act_1 = \rho(a_1) \in Activities, act_2 = \rho(a_2)\in Activities$.
- There exist $gen,use,ent$ such that $communicated(comm) = (act_2,act_1)$ and $generated(gen) = (ent,act_1)$ and $used(use) = (act_2,ent)$.
- The attributes match: $match(W,comm,attrs)$.

The $actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$ relation is interpreted as follows:

$W,\rho \models actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$ holds if and only if:

- [WF] $id$ denotes a delegation $deleg=\rho(id) \in Delegations$.
- [WF] $a$ denotes an activity $act=\rho(a) \in Activities$.
- [WF] $ag_1,ag_2$ denote agents $agent_1=\rho(ag_1), agent_2=\rho(ag_2) \in Agents$.
- The agent $agent_2$ acted for the agent $agent_1$ with respect to the activity $act$, i.e. $actedFor(deleg) = (agent_2,agent_1,act)$.
- The attributes match: $match(W,deleg,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 this 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,\rho \models wasDerivedFrom(id,e_2,e_1,act,g,u,attrs)$ holds if and only if:

- [WF] $id$ denotes a derivation $deriv = \rho(id) \in Derivations$.
- [WF] $e_1,e_2$ denote entities $ent_1 = \rho(e_1), ent_2=\rho(e_2) \in Entities$.
- [WF] $a$ denotes an activity $act = \rho(a) \in Activities$.
- [WF] $g$ denotes a generation event $gen = \rho(g) \in Generations$.
- [WF] $u$ denotes a use event $use = \rho(u) \in Usages$.
- The derivation denotes a one-step derivation path linking the entities via the activity, generation and use: $derivationPath(deriv) = ent_2 \cdot gen \cdot act \cdot use \cdot ent_1$.
- The attribute values match: $match(W,deriv,attrs)$.

An imprecise derivation formula has the form $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$.

$W,\rho \models wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ holds if and only if:

- [WF] $id$ denotes a derivation $deriv = \rho(id) \in Derivations$.
- [WF] $e_1,e_2$ denote entities $ent_1 = \rho(e_1), ent_2=\rho(e_2) \in Entities$ .
- $derivationPath(deriv)= ent_2 \cdot w \cdot ent_1$ for some $w$.
- The attribute values match: $match(W,deriv,attrs)$.

$W,\rho \models wasInfluencedBy(id,o_2,o_1,attrs)$ holds if and only if at least one of the following hold:

- [WF] $id$ denotes an influence $inf = \rho(id) \in Influences$.
- [WF] $o_1$ and $o_2$ denote objects $obj_1 = \rho(o_1) \in Objects$ and $obj_2= \rho(o_2) \in Objects$.
- The influence $inf$ links $o_2$ with $o_1$; that is, $influenced(inf) = (o_2,o_1)$.
- The attribute values match: $match(W,deriv,attrs)$.

The $specializationOf(e_1,e_2)$ relation indicates when one entity formula presents more specific aspects of another.

$W,\rho \models specializationOf(e_1,e_2)$ holds if and only if:

- [WF] Both $e_1$ and $e_2$ are entity identifiers, denoting entities $ent_1 = \rho(e_1) \in Entities$ and $ent_2 = \rho(e_2) \in Entities$.
- The two entities present aspects of the same thing, that is, $thingOf(ent_1) = thingOf(ent_2)$.
- The events of $ent_1$ are contained in those of $ent_2$, i.e. $events(ent_1) \subseteq events(ent_2)$.
- For each attribute $attr$ we have $value(ent_1,attr) \supseteq value(ent_2,attr)$.
- At least one of these inclusions is strict: that is, either $events(ent_1) \subsetneq events(ent_2)$ or for some $attr$ we have $value(ent_1,attr) \supsetneq value(ent_2,attr)$.

The second criterion says that the two Entities present (possibly different) aspects of the same Thing. Note that the third criterion allows $ent_1$ and $ent_2$ to have the same events (or $events(ent_2)$ can be larger). The last criterion allows $ent_1$ to have more defined attributes than $ent_2$, but they must include the attributes defined by $ent_2$. Two different entities that have the same attributes can also be related by specialization. The fifth criterion (indirectly) ensures that specialization is irreflexive.

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,\rho \models alternateOf(e_1,e_2)$ holds if and only if:

- [WF] Both $e_1$ and $e_2$ are entity identifiers, denoting $ent_1 = \rho(e_1)$ and $ent_2 = \rho(e_2)$.
- The two objects refer to the same underlying Thing: $thingOf(ent_1) = thingOf(ent_2)$

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

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

- [WF] Both $e_1$ and $e_2$ are entity identifiers, denoting $coll = \rho(c) \in Collections$ and $ent = \rho(e) \in Entities$.
- The entity $ent$ is a member of the collection $coll$: that is, $ent \in members(coll)$.

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.

The precedes relation $x \precedes y$ holds between two events, one taking place before (or simultaneously with) another. Its meaning is defined in terms of the quasiordering on events specified by $\preceq$. The semantics of strictly precedes ($x \strictlyPrecedes y$) is similar, only $x$ must take place strictly before $y$. It is interpreted as $\prec$, which we recall is defined from $\preceq$ as $x \prec y \iff x \preceq y \text{ and } y \not\preceq x$.

- $W,\rho \models x \precedes y$ holds if and only if $\rho(x),\rho(y) \in Events$ and $\rho(x) \preceq\rho(y)$.
- $W,\rho \models x \strictlyPrecedes y$ holds if and only if $\rho(x),\rho(y) \in Events$ and $\rho(x) \prec \rho(y)$.

The ordering of time values associated to events is unrelated to the event ordering. 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 $gen_1 \precedes gen_2$ and $gen_2 \precedes gen_1$, but this does not imply anything about the relative orderings of the associated times, or vice versa.

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

$W,\rho\models notNull(e)$ holds if and only if $\rho(e) \neq \bot$.

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

- $W,\rho\models typeOf(e,entity)$ holds if and only if $\rho(e) \in Entities$.
- $W,\rho\models typeOf(a,activity)$ holds if and only if $\rho(a) \in Activities$.
- $W,\rho\models typeOf(ag,agent)$ holds if and only if $\rho(ag) \in Agents$.
- $W,\rho\models typeOf(c,Collection)$ holds if and only if $\rho(c) \in Collections$.
- $W,\rho\models typeOf(c,EmptyCollection)$ holds if and only if $\rho(c) \in Collections$ and $members(\rho(c)=\emptyset$.

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 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}[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}$

This follows immediately from the semantics of $wasInformedBy$.

$\begin{array}[t]{l}
\forall gen,e,a_1,t_1,attrs_1,use,a_2,t_2,attrs_2.~
\\
\qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(use,a_2,e,t_2,attrs_2)
\\
\quad\Rightarrow
\exists id.~wasInformedBy(id,a_2,a_1,[])
\end{array}$

This follows from the semantics of $wasInformedBy$ and Axiom 1.

$\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}$

This follows from Axiom 2, which requires that generation and invalidation events exist for each entity.

$\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}$

This follows from the semantics of activity formulas, specifically the requirement that start and end events exist for the activity.

$\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}$

This follows from Axiom 3.

$\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}$

This follows from Axiom 4.

$\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}$

This follows from the semantics of precise derivation steps.

$\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}$

This follows from the semantics of derivation steps (precise or imprecise) and Axiom 5.

$\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}$

This follows from the semantics of generation, association, and attribution, by Axiom 6.

$\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}$

This follows from the semantics of association and delegation, by Axiom 7.

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\begin{array}[t]{l} \forall id,e,ag,attrs.~ \\ \qquad wasAttributedTo(id,e,ag,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,e,ag,attrs) \end{array}$

$\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}$

$\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}$

$\begin{array}[t]{l}
\forall e.~
\\
\qquad entity(e)
\\
\quad\Rightarrow
alternateOf(e,e)
\end{array}$

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

$\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}$

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_1,e_3)$.

$\begin{array}[t]{l}
\forall e_1,e_2.~
\\
\qquad alternateOf(e_1,e_2)
\\
\quad\Rightarrow
alternateOf(e_2,e_1)
\end{array}$

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

$\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}$

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 $events(e_1) \subseteq events(e_2) \subseteq events(e_3)$. Moreover, $value(obj_2,attr) \supseteq value(obj_3,attr)$, and similarly $value(obj_1,attr)\supseteq value(obj_2,attr)$ so $value(obj_1,attr) \supseteq value(obj_3,attr)$. Finally, at least one of the inclusions between $obj_1$ and $obj_2$ is strict, so the same is the case for $obj_1$ and $obj_3$.

$\begin{array}[t]{l}
\forall e_1,e_2.~
\\
\qquad specializationOf(e_1,e_2)
\\
\quad\Rightarrow
alternateOf(e_1,e_2)
\end{array}$

If $ent_1=\rho(e_1)$ and $ent_2 = \rho(e_2)$ are specializations, then $thingOf(ent_1) = thingOf(ent_2)$.

$\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}$

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 $v \in value(ent_1,att)$. Thus $v \in value(ent_2,att)$ since $value(ent_2,att) \supseteq value(ent_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,\rho \models entity(e_2,attrs)$.

$\forall id,attrs_1,attrs_2. entity(id,attrs_1) \wedge entity(id,attrs_2) \Rightarrow entity(id,attrs_1\cup attrs_2)$

$\forall id,t_1,t_1',t_2,t_2',attrs_1,attrs_2.~ activity(id,t_1,t_2,attrs_1) \wedge activity(id,t_1',t_2',attrs_2) \Rightarrow activity(id,t_1,t_2,attrs_1\cup attrs_2) \wedge t_1=t_1' \wedge t_2=t_2'$

$\forall id,attrs_1,attrs_2. agent(id,attrs_1) \wedge agent(id,attrs_2) \Rightarrow agent(id,attrs_1\cup attrs_2)$.

These properties follow immediately from the definitions of the semantics of the respective assertions, because functions are used for the underlying data.

$\begin{array}[t]{l} \forall id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\ wasGeneratedBy(id,e,a,t,attrs) \wedge wasGeneratedBy(id,e',a',t',attrs_2) \\ \quad \Rightarrow wasGeneratedBy(id,e,a,t,attrs_1 \cup attrs_2) \wedge e=e' \wedge a=a' \wedge t = t'\end{array}$

$\begin{array}[t]{l}\forall id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\used(id,a,e,t,attrs) \wedge used(id,a',e',t',attrs_2)\\ \quad \Rightarrow used(id,a,e',t,attrs_1 \cup attrs_2) \wedge e=e' \wedge a=a' \wedge t = t' \end{array}$

$\begin{array}[t]{l}\forall id,a_1,a_2,a_1',a_2',attrs_1,attrs_2.~ \\wasInformedBy(id,a_1,a_2,attrs) \wedge wasInformedBy(id,a_1',a_2',attrs_2)\\ \Rightarrow wasInformedBy(id,a_1,a_2,attrs_1 \cup attrs_2) \wedge a_1=a_1' \wedge a_2=a_2' \end{array}$

$\begin{array}[t]{l}\forall id,e,e'a_1,a_2,a_1',a_2',t,t',attrs_1,attrs_2.~ \\wasStartedBy(id,a_2,e,a_1,t,attrs_1) \wedge wasStartedBy(id,a_2',e',a_1',t',attrs_2)\\ \Rightarrow wasStartedBy(id,a_2,e,a_1,t,attrs_1 \cup attrs_2) \wedge a_1=a_1' \wedge e=e' \wedge a_2=a_2' \wedge t = t' \end{array}$

$\begin{array}[t]{l}\forall id,e,e'a_1,a_2,a_1',a_2',t,t',attrs_1,attrs_2.~ \\wasEndedBy(id,a_2,e,a_1,t,attrs_1) \wedge wasEndedBy(id,a_2',e',a_1',t',attrs_2)\\ \Rightarrow wasEndedBy(id,a_2,e,a_1,t,attrs_1 \cup attrs_2) \wedge a_1=a_1' \wedge e=e' \wedge a_2=a_2' \wedge t = t' \end{array}$

$\begin{array}[t]{l}\forall id,e,e',a,a',t,t',attrs_1,attrs_2.~ \\wasInvalidatedBy(id,e,a,t,attrs_1) \wedge wasInvalidatedBy(id,e',a',t',attrs_2)\\ \Rightarrow wasInvalidatedBy(id,e,a,t,attrs_1 \cup attrs_2) \wedge e=e' \wedge a=a' \wedge t = t' \end{array}$

$\begin{array}[t]{l}\forall id,e_1,e_1',e_2,e_2',a,a',g,g',u,u',attrs_1,attrs_2.~ \\wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs_1) \wedge wasDerivedFrom(id,e_2',e_1',a',g_2',u_1',attrs_2)\\ \Rightarrow wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs_1 \cup attrs_2) \wedge e_1=e_1'\wedge e_2=e_2'\wedge a=a'\wedge g=g'\wedge u=u' \end{array}$

$\begin{array}[t]{l}\forall id,e,e',ag,ag',attrs_1,attrs_2.~ \\wasAttributedTo(id,e,ag,attrs_1) \wedge wasAttributedTo(id,e',ag',attrs_2)\\ \Rightarrow wasAttributedTo(id,e,ag,attrs_1 \cup attrs_2) \wedge e=e' \wedge ag = ag' \end{array}$-

$\begin{array}[t]{l}\forall id,a,a',ag,ag',pl,pl',attrs_1,attrs_2.~ \\wasAssociatedWith(id,a,ag,pl,attrs_1) \wedge wasAssociatedWith(id,a',ag',pl',attrs_2)\\ \Rightarrow wasAssociatedWith(id,a,ag,pl,attrs_1 \cup attrs_2) \wedge a=a' \wedge ag=ag' \wedge pl=pl' \end{array}$

$\begin{array}[t]{l}\forall id,ag_1,ag_1',ag_2,ag_2',a,a',attrs_1,attrs_2.~ \\actedOnBehalfOf(id,ag_2,ag_1,a,attrs_1) \wedge actedOnBehalfOf(id,ag_2',ag_1',a',attrs_2)\\ \Rightarrow actedOnBehalfOf(id,ag_2,ag_1,a,attrs_1 \cup attrs_2) \wedge ag_1=ag_1' \wedge ag_2 = ag_2' \wedge a = a' \end{array}$

$\begin{array}[t]{l}\forall id,o_1,o_2,o_1',o_2',attrs_1,attrs_2.~ \\wasInfluencedBy(id,o_2',o_1',attrs_1) \wedge wasInfluencedBy(id,o_2',o_1',attrs_2)\\ \Rightarrow wasInfluencedBy(id,o_2,o_1,attrs_1 \cup attrs_2) \wedge o_1=o_1' \wedge o_2=o_2' \end{array}$

These properties follow immediately from the definitions of the semantics of the respective assertions, again because functions are used for the underlying data.

$\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}$

This follows from Axiom 18.

$\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}$

This follows from Axiom 19.

$\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}$

This follows from Axiom 20.

$\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}$

This follows from Axiom 21.

$\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}$

This follows from the semantics of $wasStartedBy$, since the start times must both match that of the activity.

$\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}$

This follows from the semantics of $wasEndedBy$, since the end times must both match that of the activity.

$\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 \precedes end
\end{array}$

This follows from Axiom 22.

$\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 \precedes start_2
\end{array}$

This follows from Axiom 22.

$\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 \precedes end_2
\end{array}$

This follows from Axiom 23.

$\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 \precedes use \end{array}$

$\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 \precedes end \end{array}$

$\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 \precedes gen \end{array}$

$\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 \precedes end \end{array}$

$\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 \precedes end
\end{array}$

This follows from the semantics of $wasInformedBy$, Axiom 24, and the previous two constraints, because $wasInformedBy$ implies the existence of intermediate generation and usage events linking $a_1$ and $a_2$ through an entity $e$. The generation of $e$ must precede its use.

$\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 \precedes inv
\end{array}$

This follows from Axiom 24.

$\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 \precedes use
\end{array}$

This follows from Axiom 24.

$\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 \precedes inv
\end{array}$

This follows from Axiom 25.

$\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 \precedes gen_2
\end{array}$

This follows from Axiom 24.

$\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 \precedes inv_2
\end{array}$

This follows from Axiom 25.

$\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 \precedes gen_2
\end{array}$

This follows from Axiom 26.

$\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 \strictlyPrecedes gen_2
\end{array}$

This follows from Axiom 27.

$\begin{array}[t]{l} \forall gen,start,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasStartedBy(start,a,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow gen \precedes start \end{array}$

$\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 \precedes inv \end{array}$

$\begin{array}[t]{l} \forall gen,end,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow gen \precedes end \end{array}$

$\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 \precedes inv \end{array}$

$\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 \precedes gen_2
\end{array}$

This follows from Axiom 24 and the fact that if $e_2$ specializes $e_1$ then all of the events of $e_2$ are events of $e_1$. Thus, the generation of $e_1$ precedes all events of $e_2$.

$\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 \precedes inv_2
\end{array}$

This follows from Axiom 25 and the fact that if $e_2$ specializes $e_1$ then all of the events of $e_2$ are events of $e_1$. Thus, the invalidation of $e_1$ follows all events of $e_2$.

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

$\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 \precedes inv_2 \end{array}$

$\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 \precedes end_2 \end{array}$

$\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 \precedes end_2 \end{array}$

$\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 \precedes end_2 \end{array}$

$\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 \precedes gen_2 \end{array}$

$\begin{array}[t]{l} \forall att,start_1,gen_2,e,e_1,a_1,a_2,ag,t_1,t_2,attrs,attrs_1,attrs_2.~ \\ \qquad wasAttributedTo(att,e,ag,attrs) \wedge wasStartedBy(start_1,ag,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow start_1 \precedes gen_2 \end{array}$

$\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 \precedes inv_2 \end{array}$

$\begin{array}[t]{l} \forall del,start_1,end_2,ag_1,ag_2,a,a_1,a_2,e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2.~ \\ \qquad actedOnBehalfOf(del,ag_2,ag_1,a,attrs) \wedge wasStartedBy(start_1,ag_1,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,ag_2,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow start_1 \precedes end_2 \end{array}$

$\begin{array}[t]{l} \forall e,attrs.~ \\ \qquad entity(e,attrs) \\ \quad\Rightarrow typeOf(e,entity) \end{array}$

$\begin{array}[t]{l} \forall ag,attrs.~ \\ \qquad agent(ag,attrs) \\ \quad\Rightarrow typeOf(ag,agent) \end{array}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\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}$

$\begin{array}[t]{l} \forall c,e.~ \\ \qquad hadMember(c,e) \\ \quad\Rightarrow typeOf(c,Collection) \wedge typeOf(e,entity) \end{array}$

$\begin{array}[t]{l} \forall c.~ \\ \qquad entity(c,[prov:type = prov:emptyCollection])) \\ \quad\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. The final constraint requires Axiom 36.

$\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}$

$\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}$

$\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}$

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 $\bot$) or none of them are.

$\begin{array}[t]{l}
\forall e.~
\\
\qquad specializationOf(e,e)
\\
\quad\Rightarrow
False
\end{array}$

This follows from the fact that in the semantics of $specializationOf$, the requirement that one of the inclusions is strict implies that the two entities cannot be the same.

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}[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}$This follows from the assumption that the different kinds of influences are disjoint sets, characterized by their types. Note that generic influences are allowed to overlap with more specific kinds of influence.

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

$\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}$This follows from the assumption that influences are distinct from other objects (entities, activities or agents).

$\begin{array}[t]{l}
\forall id.~
\\
\qquad typeOf(id,entity) \wedge typeOf(id,activity)
\\
\quad\Rightarrow
False
\end{array}$

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

$\begin{array}[t]{l}
\forall c,e.~
\\
\qquad hasMember(c,e) \wedge typeOf(c,EmptyCollection)
\\
\quad\Rightarrow
False
\end{array}$

This follows from the definition of the semantics of $typeOf(c,EmptyCollection)$, which requires that there are no members of the collection denoted by $c$.

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

Our main soundness result is:

Let $W$ be a PROV structure, that is, a structure providing all of the components above and satisfying all of the axioms.

- If $I$ is an instance and $W \models I$ and $I'$ is obtained from $I$ by applying one of the PROV inferences, then $W \models I'$.
- If $I$ is an instance and $W \models I$ and $I'$ is obtained from $I$ by applying one of the PROV key or uniqueness constraints, then $W \models I'$.
- If $I$ is an instance and $W \models I$ then $I$ has a normal form $I'$ and $ W \models I'$.
- 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, if $W \models I$ then since $W$ satisfies the logical forms of all uniqueness and key constraints, constraint application cannot fail on $I$ and $W \models I'$.

For part 3, proceed by induction on a terminating sequence of inference or uniqueness constraint steps: if $I$ is in normal form then 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 use part 2.

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

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

In this section we give a translation from valid PROV instances to
structures, and show that a valid PROV instance has a model. We
call this property *weak completeness*.

The term *weak* refers to the fact that
there are still some inferences that are sound in the semantics but not
enforced by validation. For example, consider the following
(valid) PROV instance fragment:

entity(e,[a=1]) agent(e,[b=2])

This instance is valid and has a model, but in every model satisfying the instance, it is also true that:

entity(e,[a=1,b=2]) agent(e,[a=1,b=2])

Thus, weak completeness captures the fact that every valid instance has a model, but does not imply that a valid instance satisfies all of the deductions possible in that model.

Let $I$ be a valid PROV instance that is in normal form. We define a structure $M(I)$ as follows, by giving the sets, functions and relations specified in the components in Section 3, and finally verifying that the axioms hold.

First, without loss of generality, we assume that all times specified in activity or event formulas in $I$ are ground values. If not, set each variable in such a position to some dummy value. This is justified by the following fact:

If $I$ is valid then $S(I)$ is valid, where $S$ is any substitution that maps time variables to time constants.

First, consider a substitution $S = [t:=c]$ that maps a single time variable to a constant. It is straightforward to check that if $I$ is in normal form, then $S(I)$ is in normal form, since none of the inferences or uniqueness constraints can be enabled by changing a time variable uniformly in $I$. Similarly, the remaining constraints are insensitive to the time values, so $S(I)$ is in normal form and satisfies all of the remaining constraints just as $I$ does. The general case of a substitution that replaces multiple time variables with constants is a straightforward generalization since we can view such a substitution as a composition of single-variable substitutions.

The sets of structure $M(I)$ are:

\[ \begin{eqnarray*} Entities &=& \{id \mid I \models typeOf(id,entity)\}\\ Plans &=& \{pl \mid \exists id,ag,ac,attrs.~ wasAssociatedWith(id,ag,act,pl,attrs) \in I, pl \neq -\}\\ Collections &=& \{c \mid I \models typeOf(c,prov:Collection) \text{ or } I \models typeOf(c,prov:EmptyCollection)\} \\ Activities &=& \{id \mid I \models typeOf(id, activity)\}\\ &\cup& \{a_{id},a'_{id} \mid id \in Entities\}\\ &\cup& \{a_{id} \mid \exists id,e_2,e_1.~wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\ Agents &=& \{id \mid I \models typeOf(id,agent)\}\\ \\ Usages &=& \{id \mid \exists a,e,t,attrs.~used(id,a,e,t,attrs) \in I\}\\ &\cup& \{u_{id} \mid \exists id,e_2,e_1,attrs.~wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\ Generations &=& \{id \mid \exists e,a,t,attrs.~wasGeneratedBy(id,e,a,t,attrs) \in I\}\\ &\cup& \{g_{id} \mid \exists id,e_2,e_1,attrs.~wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\}\\ & \cup & \{g_{id} \mid id \in Entities\}\\ Invalidations &=& \{id \mid \exists e,a,t,attrs.~wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\ & \cup & \{i_{id} \mid id \in Entities\}\\ Starts &=& \{id \mid \exists a,e,a',t,attrs.~wasStartedBy(id,a,e,a',t,attrs) \in I\}\\ Ends &=& \{id \mid \exists a,e,a',t,attrs.~wasEndedBy(id,a,e,a',t,attrs) \in I\}\\ Events &=& Usages \cup Generations \cup Invalidations \cup Starts \cup Ends\\ \\ Associations &=& \{id \mid \exists ag,act,pl,attrs.~ wasAssociatedWith(id,ag,act,pl,attrs) \in I\}\\ Attributions &=& \{id \mid \exists e,ag,attrs.~wasAttributedTo(id,e,ag,attrs) \in I\}\\ Delegations &=& \{id \mid \exists ag_2,ag_1,attrs.~ actedOnBehalfOf(id,ag_2,ag_1,act,attrs) \in I\}\\ Communications &=& \{id \mid \exists a_2,a_1,attrs.~wasInformedBy(id,a_2,a_1,attrs) \in I\}\\ Derivations &=& \{id \mid \exists e_2,e_1,a,g,u,attrs.~wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \in I\}\\ \\ Influences &=& Events \cup Associations \cup Attributions \cup Communications \cup Delegations\\ &\cup & \{id \mid \exists o_2,o_1,attrs.~ wasInfluencedBy(id,o_2,o_1,attrs) \in I\}\\ \\ Objects &=& Entities \cup Activities \cup Agents \cup Influences\\ \end{eqnarray*} \]In the definitions of $Entities$, $Collections$, $Activities$ and $Agents$ we use the notation $I \models typeOf(id,t)$ to indicate that $id$ must have type $t$ in $I$ according to the typing constraints. For example, for entities, this means that the set $Entities$ contains all identifiers $e,e'$ appearing in the $entity(e,attrs)$, $alternateOf(e,e')$, or $specializationOf(e,e')$ formulas, as well as all tose appearing in the appropriate positions of other formulas, as specified in the typing constraints.

In the definitions of $Activities$, $Generations$, $Invalidations$, and $Usages$ we write $a_{id}$, $g_{id}$, $i_{id}$ and $u_{id}$ respectively to indicate additional activities, generations and usages added for imprecise derivations or entities.

In addition, to define the set of $Things$, we introduce an equivalence relation on $Entities$ as follows:

\[e_1 \equiv e_2 \iff alternateOf(e_1,e_2) \in I\]The fact that this is an equivalence relation follows from the
fact that $I$ is in normal form, since the constraints on
$alternateOf$ ensure that it is an equivalence relation. Recall
that given an equivalence relation $\equiv$ on some set $X$, the
*equivalence class* of $x \in X$ is the set $[x]_\equiv = \{y
\in X \mid x
\equiv y\}$. The *quotient* of $X$ by an equivalence
relation on $X$ is the set of equivalence classes, $X_\equiv =
\{[x]_\equiv \mid x \in X\}$. Now we
define the set of $Things$ as the quotient of $\equiv$-equivalence classes of $Entities$.

Observe that since $I$ is normalized and valid, entities and activities are disjoint, the influences are disjoint from entities, activities, and agents, and the different subsets of events and influences are pairwise disjoint, as required.

First, we consider the functions associated with $Entities$.

\[ \begin{eqnarray*} events'(e) &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\ &\cup& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\ &\cup& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\ &\cup& \{id \mid wasStartedBy(id,a,e,a',t,attrs) \in I\}\\ &\cup& \{id \mid wasEndedBy(id,a,e,a',t,attrs) \in I\}\\ &\cup& \{g_e,i_e\}\\ events(e) &=& events'(e) \cup \bigcup_{specializationOf(e',e) \in I} events'(e')\\ value'(e,a) &=& \{v \mid entity(e,attrs) \in I, (a=v) \in attrs\} \quad (a \neq uniq)\\ value'(e,uniq) &=&\{ uniq_{e}\}\\ value(e,a) &=& value'(e) \cup \bigcup_{specializationOf(e,e') \in I} value'(e')\\ thingOf(e) &=& [e]_\equiv \end{eqnarray*} \]Above, we introduce a fresh attribute name $uniq$, not already in use in $I$, along with a fresh value $e$ and for each entity $e$ we add a value $uniq_e$ to $values(e,uniq)$. This construction ensures that if an entity is a specialization of another in $I$ then the specialization relationship will hold in $M(I)$. We also define the set of all events involved in $e$ as the set of events immediately involved in $e$ or any specialization of $e$. Similarly, the values of attributes of $e$ are those immediately declared for $e$ along with those of any $e'$ that $e$ specializes. We also introduce dummy generation and invalidation events for each entity $e$, along with activities $a_e,a'_e$ to perform them.

Similarly, for $Things$, we employ an auxiliary function $events:Things \to P(Events)$ that collects the set of all events in which one of the entities constituting the thing participated.

\[ \begin{eqnarray*} events(T) &=& \bigcup_{e \in T} events(e)\\ value(T,a,evt) &=& \bigcup_{e \in T, evt \in events(e)} value(e,a)\\ \end{eqnarray*} \]The functions $events$, $startTime$ and $endTime$ mapping activities to their start and end times are defined as follows:

\[\begin{eqnarray*} events(a) &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\ &\cup& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\ &\cup& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\ &\cup& \{id \mid wasStartedBy(id,a,e,a',t,attrs) \in I\}\\ &\cup& \{id \mid wasEndedBy(id,a,e,a',t,attrs) \in I\}\\ &\cup& \{g_e,i_e\}\\ startTime(id) &=& t_1 \text{ where } activity(a,t_1,t_2,attrs) \in I\\ endTime(id) &=& t_2 \text{ where } activity(a,t_1,t_2,attrs) \in I\\ \end{eqnarray*} \]The start and end times are arbitrary (say, some zero value) for activities with no $activity$ formula declaring the times. The above definitions of $startTime$ and $endTime$ ignore any start times asserted in $wasStartedBy$ or $wasEndedBy$ formulas. If both $activity$ and $wasStartedBy/wasEndedBy$ statements are present, then they must match, but PROV-CONSTRAINTS does not require that the times of multiple start or end events match for an activity with no $activity$ statement.

The following valid instance exemplifies the above discussion, when $t_1 \neq t_2$:

wasStartedBy(id1;a,e1,a1,t1,[]) wasStartedBy(id2;a,e2,a2,t2,[])

This instance becomes invalid if we add an $activity(a,[])$ statement, because it expands to $activity(a,T_1,T_2,[])$ where $T_1,T_2$ are existential variables, and uniqueness constraints require that $t_1 = T_1 = t_2$, which leads to uniqueness constraint failure.

For other $Objects$ besides $Entities$ and $Activities$, the associated sets of $Events$ are defined to be empty. (An $Agent$ that happens to be an $Entity$ or $Activity$ will have the set of events defined above for the appropriate kind of object. Note that since $Entities$ and $Activities$ are disjoint, this definition is unambiguous.)

The function $time$ mapping $Events$ to their $Times$ is defined as follows:

\[\begin{eqnarray*} time(id) &=& t \text{ where } used(id,a,e,t,attrs) \in I\\ time(id) &=& t \text{ where } wasGeneratedBy(id,e,a,t,attrs) \in I\\ time(id) &=& t\text{ where } wasInvalidatedBy(id,e,a,t,attrs) \in I\\ time(id) &=& t \text{ where } wasStartedBy(id,a,e,a',t,attrs) \in I\\ time(id) &=& t \text{ where }wasEndedBy(id,a,e,a',t,attrs) \in I\\ \end{eqnarray*} \]This definition is deterministic because the sets of identifiers of different $Events$ are disjoint, and the associated times are unique.

The functions giving the interpretations of the different identified influences are as follows:

\[\begin{eqnarray*} used(id) &=& (a,e) \text{ where } used(id,a,e,t,attrs) \in I\\ used(u_{id}) &=& (a_{id},e_1) \text{ where } wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\\ generated(id) &=& (e,a) \text{ where } wasGeneratedBy(id,e,a,t,attrs) \in I\\ generated(g_{id}) &=& (e_2,a_{id}) \text{ where } wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\\ generated(g_e) &=& (e,a_e) \text{ where } e \in Entities\\ invalidated(id) &=& (e,a) \text{ where } wasInvalidatedBy(id,e,a,t,attrs) \in I\\ invalidated(i_e) &=& (e,a'_e) \text{ where } e \in Entities\\ started(id) &=& (a,e,a') \text{ where } wasStartedBy(id,a,e,a',t,attrs) \in I\\ ended(id) &=& (a,e,a') \text{ where }wasEndedBy(id,a,e,a',t,attrs) \in I\\ \\ associatedWith(id) &=& (ag,act,pl) \text{ where } wasAssociatedWith(id,ag,act,pl,attrs) \in I\\ attributedTo(id) &=& (e,ag) \text{ where } wasAttributedTo(id,e,ag,attrs) \in I\\ actedFor (id) &=& (ag_2,ag_1,act) \text{ where } actedOnBehalfOf(id,ag_2,ag_1,act,attrs) \in I\\ communicated(id) &=& (a_2,a_1) \text{ where } wasInformedBy(id,a_2,a_1,attrs)\in I\\ derivationPath(id) &=& e_2\cdot g \cdot a \cdot u \cdot e_1 \text{ where } wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \in I\\ derivationPath(id) &=& e_2\cdot g_{id} \cdot a_{id} \cdot u_{id} \cdot e_1 \text{ where } wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\\ \end{eqnarray*} \]Note that since $I$ is normalized and valid, by the uniqueness constraints these functions are all well-defined. In the case for imprecise derivations, we generate additional activities, generations and usages linking $e_2$ to $e_1$.

The definition of the $influenced$ function is more involved, and is as follows:

\[\begin{eqnarray*} influenced(id) &=& used(id) \cup generated(id) \cup invalidated(id)\\ &\cup& \{(a,e) \mid (a,e,a') \in started(id)\}\\ &\cup& \{(a,e) \mid (a,e,a') \in ended(id)\}\\ &\cup & \{(ag,act) \mid (ag,act,pl) \in associatedWith(id)\}\\ &\cup& attributedTo(id) \\ &\cup & \{(ag_2,ag_1) \mid (ag_2,ag_1,act) \in actedFor(id)\}\\ &\cup& communicated(id)\\ &\cup& \{(e_2,e_1) \mid e_2 \cdot w \cdot e_1 \in derivationPath(id)\}\\ &\cup& \{(o_2,o_1) \mid wasInfluencedBy(id,o_2,o_1) \in I\} \end{eqnarray*} \]This definition ensures that by construction $influenced(id)$ contains all of the other associated relationships. For any specific $id$, however, most of the above sets will be empty, and the final line will often be redundant. It is not always redundant, because it is possible to assert an unspecified influence in $I$.

It is straightforward to verify (by their definitions) that the event sets associated with entities and activities satisfy the side-conditions in Component 9.

Finally, the collection membership function $members$ is defined as follows:

\[members(c) = \{e \mid hadMember(c,e) \in I\]We introduced a relation $\equiv$ corresponding to $alternateOf$ above, in defining $Things$, but this relation is not a component of the semantics.

The event ordering relation is defined as follows:

\[evt \preceq evt' \iff (evt,evt') \in G_I\]closed under reflexivity and transitivity. Here, we are using a slight abuse of notation: we write $G_I$ for the directed graph that is used during validation of $I$ to test for cycles among event ordering constraints. See Sec. 7.1 of PROV-CONSTRAINTS [[PROV-CONSTRAINTS]].

To verify that the construction of $M(I)$ yields a PROV structure, we must ensure that all of the axioms and side-conditions in the components are satisfied. As noted above, the disjointness constraints are satisfied by construction.

For each axiom we give the corresponding justification:

- Axiom 1 follows because $I$ is normalized with respect to Inference 6.
- Axiom 2 follows from the construction, since we add dummy generation and invalidation events for every entity.
- Axioms 3 and 4 follow because $I$ is normalized with respect to Inference 9 and 10 respectively.
- Axiom 5 follows because $I$ is normalized with respect to Inference 12.
- Axioms 6 and 7 follow because $I$ is normalized with respect to Inference 13 and 14 respectively.
- Axioms 8 through 17 follow because $I$ is normalized with respect to Inference 15.
- Axioms 18 through 21 follow because $I$ is normalized with respect to uniqueness constraints 24 through 27.
- Axiom 22 follows because constraints 30, 31, 33, 34 ensure that a start event for an activity precedes any other start, end, usage or generation events involving that activity.
- Axiom 23 follows because constraints 30, 32, 33, 34 ensure that an end event for an activity follows any other events involving that activity.
- Axiom 24 follows because constraints 34, 36, 37, 39 ensure that a generation event for an entity precedes any other events involving that entity.
- Axiom 25 follows because constraints 36, 38, 40, 43, 44 ensure that an invalidation event for an entity follows any other generation, usage, or invalidation events involving that entity.
- Axiom 26 follows from constraint 41.
- Axiom 27 follows from constraint 42 and from the fact that the event ordering constraint graph $G_I$ associated with a valid instance $I$ cannot have any cycles involving a strict precedence edge.
- Axioms 28 through 31 follow from Constraint 47.
- Axioms 32 and 33 follow from Constraint 48.
- Axioms 34 and 35 follow from Constraint 49.
- Axiom 36 follows from Constraint 50, part 19, and the semantics of $typeof$.

The main results of this section are that if a valid PROV instance $I$ has a model $M \models I$ that satisfies all of the inferences and constraints. Thus, a form of completeness holds: every valid PROV instance has a model.

Suppose $J$ is a valid PROV instance. Then there exists a PROV structure $M$ such that $M \models J$.

First, we consider the case where $J$ itself is a valid, normalized PROV instance $I$, with no existential variables, and let $M(I)$ be the corresponding structure. Then $M(I)$ is a PROV structure, satisfying all of the axioms (and hence all of the inferences and constraints) stated above.

Moreover, $M(I) \models I$, as can be verified on a case-by-case basis for each type of formula by considering its semantics and the definition of the construction of $M$. Most cases are straightforward; we consider the cases of $alternateOf$ and $specializationOf$ since they are among the most interesting.

- Suppose $alternateOf(e_1,e_2) \in I$. We wish to show that $M(I) \models alternateOf(e_1,e_2)$. Since there are no existential variables in $I$, we know that $e_1,e_2 \in M(I).Entities$. Moreover, $e_1 \equiv e_2$ according to the equivalence relation defined above, and so $thingOf(e_1) = [e_1]_\equiv = [e_2]_\equiv = thingOf(e_2)$, so we can conclude that $M(I) \models alternateOf(e_1,e_2)$.
- Suppose $specializationOf(e_1,e_2) \in I$. We wish to show that $M(I) \models specializationOf(e_1,e_2)$. Again, clearly $e_1,e_2 \in Entities$, and since $I$ satisfies all inferences, we know that $alternateOf(e_1,e_2)\in I$ so clearly $thingOf(e_2) = thingOf(e_1)$ as argued above. Next, \[\begin{eqnarray*} events(e_1) &=& events'(e_1) \cup \bigcup_{specializationOf(e',e_1) \in I} events'(e') \\ &\subseteq& events'(e_2) \cup \bigcup_{specializationOf(e',e_2) \in I} events'(e_2)\\ &=& events(e_2) \end{eqnarray*} \] because $specializationOf(e_1,e_2) \in I$ and all $e'$ that are specializations of $e_1$ are also specializations of $e_2$. Furthermore, for each $attr$, \[\begin{eqnarray*} value(e_1,attr) &=& value'(e_1,attr) \cup \bigcup_{specializationOf(e_1,e') \in I} value'(e',attr)\\ &\supseteq& value'(e_2,attr) \cup \bigcup_{specializationOf(e_2,e')\in I}value'(e',attr)\\ &=& value(e_2,attr) \end{eqnarray*} \] for the same reason. Finally, by construction $uniq_{e_1} \in value(e_1,uniq) $ and $uniq_{e_1} \notin value(e_2,uniq)$ so the inclusion is strict for the special attribute $uniq$. Thus, we have verified all of the conditions necessary to conclude $M(I) \models specializationOf(e_1,e_2)$.

Next, we show how to handle a normalized, valid $I$ contains existential variables $x_1,\ldots,x_n$. Choose fresh constants $c_1,\ldots,c_n$ of appropriate types for the existential variables and define $\rho(x_i) = c_i$. Then $M(\rho(I)) \models \rho(I)$ by the above argument. Moreover, $M(\rho(I)),\rho \models I$. So $M(\rho(I))$ is itself the desired model.

Finally, to handle the case where $J$ is an arbitrary valid instance, we need to show that if $J$ is not in normal form, and normalizes to some $I$ such that $M \models I$, then $M \models J$. We can prove this by induction on the length of the sequence of normalization steps. The base case, when $J = I$, is established already. Suppose $J$ normalizes in $n+1$ steps and we can perform one normalization step on it to obtain $J'$, which normalizes to $I$ in $n$ steps. By induction, we know that $M \models J'$. For each possible normalization step, we must show that if $M \models J'$ then $M \models J$.

First consider inference steps. These add information, that is, $J' \supseteq J$. Hence it is immediate that $M \models J$ since every formula in $J$ is in $J'$, and all formulas of $J'$ are satisfied in $M$.

Next consider uniqueness constraint steps, which may involve merging formulas. That is, $J = J_0 \cup \{r(id,a_1,\ldots,a_n,attrs_1), r(id,b_1,\ldots,b_n,attrs_2)\}$ and $J' = S(J_0) \cup \{r(id,S(a_1),\ldots,S(a_n),attrs_1\cup attrs_2)\}$, where $S$ is a unifying substitution making $S(a_i) = S(b_i)$ for each $i \in \{1,\ldots,n\}$. Since $M \models J'$, we must have $M,\rho \models J'$ for some $\rho$, and therefore we must also have that $M,\rho \models S(J_0)$ and $M,\rho \models r(id,S(a_1),\ldots,S(a_n),attrs_1\cup attrs_2)$. We can extend $\rho$ to a valuation $\rho'$ such that $M,\rho' \models S(x_1) = x_1 \wedge \cdots \wedge S(x_k) = x_k$ where $dom(S) = \{x_1,\ldots,x_k\}$. Also, $M,\rho' \models J_0$ and $M,\rho' \models r(id,a_1,\ldots,a_n,attrs_1\cup attrs_2)$. Moreover, since $S$ is a unifier, we also have $M,\rho' \models r(id,b_1,\ldots,b_n,attrs_1\cup attrs_2)$. Finally, since we can always remove attributes from an atomic formula without damaging its satisfiability, we can conclude that $M,\rho' \models r(id,a_1,\ldots,a_n,attrs_1) \wedge r(id,b_1,\ldots,b_n, attrs_2)$. To conclude, we have shown $M \models J_0 \cup \{ r(id,a_1,\ldots,a_n,attrs_1), r(id,b_1,\ldots,b_n, attrs_2)\}$, that is, $M \models J$, as desired.

This document has been produced by the PROV Working Group, and its contents reflect extensive discussion within the Working Group as a whole as well as feedback and comments from external reviewers. Thanks specifically to Khalid Belhajjame, Tom De Nies, Paolo Missier, Simon Miles, Luc Moreau, Satya Sahoo, Jan van den Bussche, Joachim Van Herwegen, and Antoine Zimmermann for detailed feedback.

We would also like to acknowledge Schloss Dagstuhl - Leibniz Center for Informatics, because significant progress was made on this document at Dagstuhl Seminar 12091 (Principles of Provenance) that took place from February 26 to March 2, 2012.

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 Provenance 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 (iMinds - Ghent University), David Corsar (University of Aberdeen, Computing Science), Stephen Cresswell (The National Archives), Tom De Nies (iMinds - Ghent University), 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).