Semantics of the PROV Data Model

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.

Structures and Interpretations

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

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

Objects

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

Entities

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.

Plans

We identify a specific subset of the entities called plans:

A set $Plans \subseteq Entities$ of plans.

Collections

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.

Activities

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

Agents

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.

Influences

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.

Events

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

Associations

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

Attributions

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

Communications

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

Delegations

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$

Derivations

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

$$ent_n\cdot g_n\cdot act_n\cdot u_n\cdot ent_{n-1}\cdot ...\cdot ent_1\cdot g_1\cdot act_1\cdot u_1\cdot ent_0$$

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.

Additional axioms

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.

Putting it all together

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.

Interpretations

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

Semantics

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.

Satisfaction

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

Attribute matching

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

Semantics of Element Formulas

Entity

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])

Activity

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.

Agent

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

Semantics of Relations

Generation

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

Use

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

Invalidation

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

Association

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

Start

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

End

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

Attribution

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

Communication

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

Delegation

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

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.

Precise

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

Imprecise

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

Influence

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

Specialization

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.

Alternate

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

Membership

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

Semantics of Auxiliary Formulas

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.

Precedes and Strictly Precedes

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.

notNull

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

typeOf

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

Inferences and Constraints

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.

Inferences

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

This follows via Axioms 8 through 17.

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

Constraints

Uniqueness constraints

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

Ordering constraints

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

Part 1 follows from Axiom 22 and part 2 follows from Axiom 23.

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

Part 1 follows from Axiom 22 and part 2 follows from Axiom 23.

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

Part 1 follows from Axiom 24. Part 2 follows from Axiom 25.

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

Part 1 follows from Axiom 24. Part 2 follows from Axiom 25.

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

The four parts follow from Axiom 28 through Axiom 31 respectively.

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

These properties follow from Axiom 32 and Axiom 33.

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

These properties follow from Axiom 34 and Axiom 35.

Typing constraints

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

Impossibility constraints

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

Soundness and Completeness

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.

Soundness

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.

Weak Completeness

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.

Sets

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

\[Things = Entities /_{\equiv} = \{[e]_\equiv \mid e \in 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.

Functions

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\]

Relations

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

Axioms

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

Main results

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.

PROV Family of Documents

Implementations Encouraged

Please Send Comments

Introduction

Purpose of this document

Structure of this document

Audience

Basics

Identifiers

Attributes and Values

Times

Atomic Formulas

First-Order Formulas

Structures and Interpretations

Things

Objects

Entities

Plans

Collections

Activities

Agents

Influences

Events

Associations

Attributions

Communications

Delegations

Derivations

Additional axioms

Putting it all together

Interpretations

Semantics

Satisfaction

Attribute matching

Semantics of Element Formulas

Entity

Activity

Agent

Semantics of Relations

Generation

Use

Invalidation

Association

Start

End

Attribution

Communication

Delegation

Derivation

Precise

Imprecise

Influence

Specialization

Alternate

Membership

Semantics of Auxiliary Formulas

Precedes and Strictly Precedes

notNull

typeOf

Inferences and Constraints

Inferences

Constraints

Uniqueness constraints

Ordering constraints

Typing constraints

Impossibility constraints

Soundness and Completeness

Soundness

Weak Completeness

Sets

Functions

Relations

Axioms

Main results

Acknowledgements