Semantics of the PROV Data Model

Abstract

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

This document presents a model-theoretic semantics for the PROV data model (called the naive semantics), viewing PROV-DM statements as atomic formulas in the sense of first-order logic, and viewing the constraints and inferences specified in PROV-CONSTRAINTS as a first-order theory. It is shown that the first-order theory is sound with respect to the naive semantics. This information may be useful to researchers or users of PROV to understand the intended meaning and use of PROV for modeling information about the actual history, derivation or evolution of Web resources. It may also be useful for development of additional constraints or inferences for reasoning about PROV or integration of PROV with other Semantic Web vocabularies. It is not proposed as a canonical or required semantics of PROV and does not place any constraints on the use of PROV.

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

3. Structures and Interpretations

3.1 Things

Note

TODO: Add semantic structure for collections and membership.

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

To model this, a structure $W$ includes:

Component 1 (things)

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

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

Note that this description does not say what the structure of a $Thing$ is, only how it may be described in terms of its time interval and attribute values. A thing could be a record of fixed attribute values; it could be a bear; it could be the Royal Society; it could be a transcendental number like $\pi$ . All that matters from our point of view is that we know how to map the $Thing$ to its time interval and attribute mapping.

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

3.2 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 lifetime.

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

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

Component 2 (objects)

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

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

As with Things, the range of $value$ is sets of values, making $value$ effectively a multivalued function. It is also possible to have two different objects that are indistinguishable by their attributes and time intervals. Objects are not things, and the sets of $Objects$ and $Things$ are disjoint; however, certain objects, namely entities, are associated with things.

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

3.2.1 Entities

An entity is a kind of object that describes a time-slice of a thing, during which some of the thing's attributes are fixed. We assume:

Component 3 (entities)

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

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

Furthermore, all of the attribute values of the entity must be present in the associated thing throughout the lifetime of the entity. For example, suppose $value(thingOf(e),a,t)$ is $\{1\}$ at some time in $lifetime(e)$ and $value(thingOf(e),a,t') = \{2\}$ at some other time $t'$ . 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,t)$ whenever $t \in lifetime(e)$ . Intuitively, this means that if we are talking about a $Thing$ indirectly by describing an $Entity$ , then any attributes we ascribe to the $Entity$ must also describe the associated $Thing$ during their common lifetime. Attributes of both $Entities$ and $Things$ are multi-valued, so there is no inconsistency in saying that an entity has two different values for some attribute. In some situations, further uniqueness constraints or range constraints could be imposed on attributes, for example by extending the PROV-O ontology.

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

3.2.1.1 Plans

We identify a specific subset of the entities called plans:

Component 4 (plans)

A set $Plans \subseteq Entities$ of plans.

3.2.2 Activities

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

Component 5 (activities)

A set $Activities \subseteq Objects$ of activities.
Activities are disjoint from Entities: $Entities\cap Activities = \emptyset$ .

3.2.3 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:

Component 6 (agents)

A set $Agents \subseteq Objects$ of agents.

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

3.2.4 Interactions

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

Component 7 (interactions)

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

3.2.4.1 Events

An Event is an interaction whose lifetime is a single time instant, and relates an activity to an entity (which could be an agent). Events have types including usage, generation, invalidation, starting and ending. Events are instantaneous. We introduce:

Component 8 (events)

A set $Events \subseteq Interactions$ of events, such that $type(evt) \in \{start,end,generation,usage,invalidation\}$ if and only if $evt \in Events$ .
A function $time : Events \to Times$ giving the time of each event; i.e. $lifetime(evt) = \{time(evt)\}$ .
The derived ordering on events given by $evt_1 \leq evt_2 \iff time(evt_1) \leq time(evt_2)$

3.2.4.2 Associations

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

Component 9 (associations)

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

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

3.2.4.3 Communications

Note

TODO

3.2.4.4 Delegations

Note

TODO

3.2.4.5 Derivations

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

Component 10 (derivations)

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

See below for the associated derivation path and DerivedFrom relation.

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

3.3 Relations

Simple relations

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

A relation $Used \subseteq Events \times Entities$ saying when an event used an entity. An event can use at most one entity, and if $(evt,e)\in Used$ then $time(evt) \in lifetime(e)$ and $type(evt) = usage$ must hold.
A relation $Generated \subseteq Events \times Entities$ saying when an event generated an entity. An event can generate at most one entity, and if $(evt,e)\in Generated$ then $min(lifetime(e)) = time(evt)$ and $type(evt) = generation$ must hold.
A relation $Invalidated \subseteq Events \times Entities$ saying when an event invalidated an entity. An event can invalidate at most one entity, and if $(evt,e)\in Invalidated$ then $max(lifetime(e)) = time(evt)$ and $type(evt) = invalidation$ must hold.
A relation $EventActivity \subseteq Events \times Activities$ associating activities with events, such that $(act,evt) \in EventActivity$ implies $time(evt) \in lifetime(act)$ .
A relation $AssociatedWith \subseteq Associations \times Agents \times Activities \times Plans_\bot$ indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan.
A relation $ActsFor \subseteq Delegations \times Agents \times Agents \times Activities$ indicating when one agent acts on behalf of another with respect to a given activity.

Note

TODO: Communication, start, end relations

Note

TODO: Specialization relation

Note

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

3.3.1 Derivation paths and DerivedFrom

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

e n t_{n} \cdot g_{n} \cdot a c t_{n} \cdot u_{n} \cdot e n t_{n - 1} \cdot . . . \cdot e n t_{1} \cdot g_{1} \cdot a c t_{1} \cdot u_{1} \cdot e n t_{0}

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

D e r i v a t i o n P a t h s = E n t i t i e s \cdot (E v e n t s \cdot A c t i v i t i e s \cdot E v e n t s \cdot E n t i t i e s)^{+}

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

with the constraints that for each derivation path:

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

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

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

Note

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

The reason why we need paths and not just individual derivation steps is that

w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, -, -, -, a t t r s)

$wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$ formulas can represent multiple derivation steps.

3.4 Putting it all together

A structure $W$ is a structure containing all of the above described data. If we need to talk about the objects or relations of more than one structure then we may write $W_1.Objects$ , $W_1.Things$ , etc.; otherwise, to decrease notational clutter, when we consider a fixed structure then the names of the sets, relations and functions above refer to the components of that model.

Note

TODO: Highlight the distinctive vs obvious/routine features.

3.5 Interpretations

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

4. Semantics

In what follows, let $W$ be a fixed structure with the associated sets and relations discussed in the previous section, and let $I$ be an interpretation of identifiers as objects in $W$ . The annotations [WF] refer to well-formedness constraints that correspond to typing constraints.

4.1 Satisfaction

Consider a formula $\phi$ , a structure $W$ and an interpretation $I$ . We define notation $W,\rho \models \phi$ which means that $\phi$ is satisfied in $W,\rho$ . For atomic formulas, the definition of the satisfaction relation is given in the next few subsections. We give the standard definition of the semantics of the other formulas:

Semantics 11 (first-order-logic-semantics)

$W,\rho \models True$ always holds.
$W,\rho \models False$ never holds.
$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,i\models \psi$ .
$W,\rho \models \phi \vee \psi$ holds if either $W,\rho \models \phi$ or $W,\rho \models \psi$ holds.
$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 interactions (which are in turn further subdivided into types of interactions). $Things$ and relations cannot be referenced directly by identifiers.

A PROV instance $I$ consists of a set of statements, each of which can be translated to an atomic formula following the definitional rules in PROV-CONSTRAINTS, possibly by introducing fresh existential variables. Thus, we can view an instance $I$ as a set of atomic formulas $\{\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$ .

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

4.3 Semantics of Element Formulas

4.3.1 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:

Semantics 12 (entity-semantics)

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

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

Semantics 13 (activity-semantics)

$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: $min(lifetime(id)) = \rho(st)$
$\rho(et)$ is the activity's end time, that is: $max(lifetime(id)) = \rho(et)$
The attributes match: $match(W,act,attrs)$ .

4.3.3 Agent

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

Semantics 14 (agent-semantics)

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

4.4 Semantics of Relations

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

Semantics 15 (generation-semantics)

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

[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$ .
[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$ is involved in $act$ , that is, $(evt,act) \in EventActivity$ .
The type of $evt$ is $generation$ , i.e. $type(evt) = generation$ .
The event $evt$ occurred at time $\rho(t) \in Times$ , i.e. $time(evt) = \rho(t)$ .
The event $evt$ generated $ent$ , i.e. $(evt,ent) \in Generated$ .
The attribute values match: $match(W,evt,attrs)$ .

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

Semantics 16 (usage-semantics)

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

[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$ .
[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$ is part of $act$ , i.e. $(evt,act) \in EventActivity$ .
The type of $evt$ is $use$ , i.e., $type(evt) = use$ .
The event $evt$ occurred at time $\rho(t) \in Times$ , i.e. $time(evt) = \rho(t)$ .
The event $evt$ used $obj$ , i.e. $(evt,ent) \in Used$ .
The attribute values match: $match(W,evt,attrs)$ .

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

Semantics 17 (invalidation-semantics)

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

[WF] The identifier $id$ denotes an event $evt = \rho(id) \in Events$ .
[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$ is involved in $act$ , that is, $(evt,act) \in EventActivity$ .
The type of $evt$ is $invalidation$ , i.e. $type(evt) = invalidation$ .
The event $evt$ occurred at time $\rho(t) \in Times$ , i.e. $time(evt) = \rho(t)$ .
The event $evt$ invalidated $ent$ , i.e. $(evt,ent) \in Invalidated$ .
The attribute values match: $match(W,evt,attrs)$ .

4.4.4 Association

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

Semantics 18 (association-plan-semantics)

$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. $(assoc,agent,act,plan) \in AssociatedWith$ .
The attributes match: $match(W,assoc,attrs)$ .

Semantics 19 (assocation-semantics)

$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 plan, i.e. $(assoc,agent,act,\bot) \in AssociatedWith$ .
The attributes match: $match(W,assoc,attrs)$ .

4.4.5 Start Formulas

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

Semantics 20 (start-semantics)

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

[WF] $id$ denotes an event $evt = \rho(id) \in Events$ .
[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 $evt$ has type $start$ , i.e. $type(evt) = start$ .
The event happened at the start of $act_2$ , that is, $(evt,act_2) \in EventsActivities$ , and $\rho(t) = min(lifetime(act_2)) = time(evt)$ .
TODO: The entity $e$ was generated by $act_1$ and started $act_2$ .
The event happened during $act_1$ , that is, $(evt,act_1) \in EventsActivities$ .
The attributes match: $match(W,evt,attrs)$ .

4.4.6 End

An activity end formula $wasEndedBy(id,a_2,e,a_1,t,attrs)$ is interpreted as follows:

Semantics 21 (end-semantics)

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

[WF] $id$ denotes an event $evt = \rho(id) \in Events$ .
[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 $evt$ has type $end$ , i.e. $type(evt) = end$ .
The event happened at the end of $act_2$ , that is, $(evt,act_2) \in EventsActivities$ , and $\rho(t) = max(lifetime(act_2)) = time(evt)$ .
TODO: The entity $e$ was generated by $act_1$ and ended $act_2$ .
The event happened during $act_1$ , that is, $(evt,act_1) \in EventActivity.
The attributes match: $match(W,evt,attrs)$ .

4.4.7 Attribution

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

Semantics 22 (attribution-semantics)

$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. $(assoc,ent,agent) \in AttributedTo$ .
The attributes match: $match(W,evt,attrs)$ .

4.4.8 Communication

Note

TODO: Communication

4.4.9 Delegation

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

Semantics 23 (delegation-semantics)

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

[WF] $id$ denotes an association $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$ acts for the agent $agent_1$ with respect to the activity $act$ , i.e. $(deleg,agent_2,agent_1,act) \in ActsFor$ .
The attributes match: $match(W,assoc,attrs)$ .

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

4.4.10.1 Precise

A precise derivation formula has the form $wasDerivedFrom(id,e_2,e_1,a,g,u,attrs)$ .

Semantics 24 (derivation-precise-semantics)

$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 Events$ and $type(\rho(g)) = generation$ .
[WF] $u$ denotes a use event $\rho(u) \in Events$ and $type(\rho(u)) = use$ .
The derivation denotes a one-step derivation $derivationPath(deriv) = ent_2 \cdot gen \cdot act \cdot use \cdot ent_1$ .
The attribute values match: $match(W,deriv,attrs)$ .

4.4.10.2 Imprecise

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

Semantics 25 (derivation-imprecise-semantics)

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

4.4.11 Influence

Note

TODO: Define influence semantics.

4.4.12 Specialization

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

Note

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

Semantics 26 (specialization-semantics)

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

[WF] Both $e_1$ and $e_2$ are entity identifiers, denoting distinct entities $ent_1 = \rho(e_1) \in Entities$ and $ent_2 = \rho(e_2) \in Entities$ , where $ent_1 \neq ent_2$ .
The two Entities refer to the same Thing, that is, $thingOf(ent_1) = thingOf(ent_2)$ .
The lifetime of $ent_1$ is contained in that of $ent_2$ , i.e. $lifetime(ent_1) \subseteq lifetime(ent_2)$ .
For each attribute $attr$ we have $value(ent_1,attr) \supseteq 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 lifetime (or that of $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$ .

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

Semantics 27 (alternate-semantics)

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

4.4.14 Membership

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

Semantics 28 (membership-semantics)

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

Note

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

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

4.5.1 Equals

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

Semantics 29 (equals-semantics)

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

4.5.2 Precedes and Strictly Precedes

The precedes relation $x \preceq y$ holds between two events, one taking place before (or simultaneously with) another. Since the naive semantics assumes that times are linearly ordered and event times are mapped to a single time line, this amounts to comparing the event times. The semantics of strictly precedes ( $x \prec y$ is similar, only $x$ must take place strictly before $y$ ).

Semantics 30 (precedes-semantics)

$W,\rho \models x \preceq y$ holds if and only if $\rho(x),\rho(y) \in Events$ and $time(\rho(x)) \leq time(\rho(y))$ .
$W,\rho \models x \prec y$ holds if and only if $\rho(x),\rho(y) \in Events$ and $time(\rho(x)) < time(\rho(y))$ .

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

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

This instance is valid, and must satisfy precedence constraints $gen_1 \preceq gen_2$ and $gen_2 \preceq gen_1$ , but $time(gen_1)=

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

Semantics 31 (notNull-semantics)

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

4.5.3.1 typeOf

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

Semantics 32 (typeOf-semantics)

$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 TODO.
$W,\rho\models typeOf(c,EmptyCollection)$ holds if and only if TODO.

Note

TODO Collections

4.6 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 naive semantics. We exclude the definitional rules in PROV-CONSTRAINTS because they are only needed for expanding the abbreviated forms of PROV-N statements to the logical formulas used here.

4.6.1 Inferences

Inference 5 (communication-generation-use-inference)

\begin{array}{l} \forall i d, a_{2}, a_{1}, a t t r s . \\ w a s I n f o r m e d B y (i d, a_{2}, a_{1}, a t t r s) \\ \Rightarrow \exists e, g e n, t_{1}, u s e, t_{2} . w a s G e n e r a t e d B y (g e n, e, a_{1}, t_{1}, []) \land u s e d (u s e, a_{2}, e, t_{2}, []) \end{array}

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

Inference 6 (generation-use-communication-inference)

\begin{array}{l} \forall g e n, e, a_{1}, t_{1}, a t t r s_{1}, i d_{2}, a_{2}, t_{2}, a t t r s_{2} . \\ w a s G e n e r a t e d B y (g e n, e, a_{1}, t_{1}, a t t r s_{1}) \land u s e d (i d_{2}, a_{2}, e, t_{2}, a t t r s_{2}) \\ \Rightarrow \exists i d . w a s I n f o r m e d B y (i d, a_{2}, a_{1}, []) \end{array}

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

Inference 7 (entity-generation-invalidation-inference)

\begin{array}{l} \forall e, a t t r s . \\ e n t i t y (e, a t t r s) \\ \Rightarrow \exists g e n, a_{1}, t_{1}, i n v, a_{2}, t_{2} . w a s G e n e r a t e d B y (g e n, e, a_{1}, t_{1}, []) \land w a s I n v a l i d a t e d B y (i n v, e, a_{2}, t_{2}, []) \end{array}

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

Inference 8 (activity-start-end-inference)

\begin{array}{l} \forall a, t_{1}, t_{2}, a t t r s . \\ a c t i v i t y (a, t_{1}, t_{2}, a t t r s) \\ \Rightarrow \exists s t a r t, e_{1}, a_{1}, e n d, a_{2}, e_{2} . w a s S t a r t e d B y (s t a r t, a, e_{1}, a_{1}, t_{1}, []) \land w a s E n d e d B y (e n d, a, e_{2}, a_{2}, t_{2}, []) \end{array}

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

Inference 9 (wasStartedBy-inference)

\begin{array}{l} \forall i d, a, e_{1}, a_{1}, t, a t t r s . \\ w a s S t a r t e d B y (i d, a, e_{1}, a_{1}, t, a t t r s) \\ \Rightarrow \exists g e n, t_{1} . w a s G e n e r a t e d B y (g e n, e_{1}, a_{1}, t_{1}, []) \end{array}

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

Inference 10 (wasEndedBy-inference)

\begin{array}{l} \forall i d, a, e_{1}, a_{1}, t, a t t r s . \\ w a s E n d e d B y (i d, a, e_{1}, a_{1}, t, a t t r s) \\ \Rightarrow \exists g e n, t_{1} . w a s G e n e r a t e d B y (g e n, e_{1}, a_{1}, t_{1}, []) \end{array}

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

Inference 11 (derivation-generation-use-inference)

In this inference, none of $a$ , $gen_2$ , or $use_1$ can be placeholders -.

\begin{array}{l} \forall i d, e_{2}, e_{1}, a, g e n_{2}, u s e_{1}, a t t r s . \\ n o t N u l l (a) \land n o t N u l l (g e n_{2}) \land n o t N u l l (u s e_{1}) \land w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g e n_{2}, u s e_{1}, a t t r s) \\ \Rightarrow \exists t_{1}, t_{2} . u s e d (u s e_{1}, a, e_{1}, t_{1}, []) \land w a s G e n e r a t e d B y (g e n_{2}, e_{2}, a, t_{2}, []) \end{array}

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

Inference 12 (revision-is-alternate-inference)

In this inference, any of $a$ , $gen_2$ , or $use_1$ can be placeholders -.

\begin{array}{l} \forall i d, e_{1}, e_{2}, a, g, u . \\ w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g, u, [p r o v : t y p e = p r o v : R e v i s i o n])) \\ \Rightarrow a l t e r n a t e O f (e_{2}, e_{1}) \end{array}

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

Inference 13 (attribution-inference)

\begin{array}{l} \forall a t t, e, a g, a t t r s . \\ w a s A t t r i b u t e d T o (a t t, e, a g, a t t r s) \\ \Rightarrow \exists a, t, g e n, a s s o c, p l . w a s G e n e r a t e d B y (g e n, e, a, t, []) \land w a s A s s o c i a t e d W i t h (a s s o c, a, a g, p l, []) \end{array}

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

Inference 14 (delegation-inference)

\begin{array}{l} \forall i d, a g_{1}, a g_{2}, a, a t t r s . \\ a c t e d O n B e h a l f O f (i d, a g_{1}, a g_{2}, a, a t t r s) \\ \Rightarrow \exists i d_{1}, p l_{1}, i d_{2}, p l_{2} . w a s A s s o c i a t e d W i t h (i d_{1}, a, a g_{1}, p l_{1}, []) \land w a s A s s o c i a t e d W i t h (i d_{2}, a, a g_{2}, p l_{2}, []) \end{array}

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

Inference 15 (influence-inference)

$\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}$
In this rule, $a$ , $g$ , or $u$ may be placeholders -.
$\begin{array}[t]{l} \forall id,e,ag,attrs.~ \\ \qquad wasAttributedTo(id,e,ag,attrs) \\ \quad\Rightarrow wasInfluencedBy(id,e,ag,attrs) \end{array}$
In this rule, $pl$ may be a placeholder -.
$\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}$

Inference 16 (alternate-reflexive)

\begin{array}{l} \forall e . \\ e n t i t y (e) \\ \Rightarrow a l t e r n a t e O f (e, e) \end{array}

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

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

Inference 17 (alternate-transitive)

\begin{array}{l} \forall e_{1}, e_{2}, e_{3} . \\ a l t e r n a t e O f (e_{1}, e_{2}) \land a l t e r n a t e O f (e_{2}, e_{3}) \\ \Rightarrow a l t e r n a t e O f (e_{1}, e_{3}) \end{array}

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

Inference 18 (alternate-symmetric)

\begin{array}{l} \forall e_{1}, e_{2} . \\ a l t e r n a t e O f (e_{1}, e_{2}) \\ \Rightarrow a l t e r n a t e O f (e_{2}, e_{1}) \end{array}

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

Inference 19 (specialization-transitive)

\begin{array}{l} \forall e_{1}, e_{2}, e_{3} . \\ s p e c i a l i z a t i o n O f (e_{1}, e_{2}) \land s p e c i a l i z a t i o n O f (e_{2}, e_{3}) \\ \Rightarrow s p e c i a l i z a t i o n O f (e_{1}, e_{3}) \end{array}

$\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 $lifetime(e_1) \subseteq lifetime(e_2) \subseteq lifetime(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)$ . (TODO: How do we know $e_3 \neq e_1$ ? Need strict ordering on entities in semantics.)

Inference 20 (specialization-alternate-inference)

\begin{array}{l} \forall e_{1}, e_{2} . \\ s p e c i a l i z a t i o n O f (e_{1}, e_{2}) \\ \Rightarrow a l t e r n a t e O f (e_{1}, e_{2}) \end{array}

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

Inference 21 (specialization-attributes-inference)

\begin{array}{l} \forall e_{1}, a t t r s, e_{2} . \\ e n t i t y (e_{1}, a t t r s) \land s p e c i a l i z a t i o n O f (e_{2}, e_{1}) \\ \Rightarrow e n t i t y (e_{2}, a t t r s) \end{array}

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

4.6.2 Constraints

4.6.2.1 Uniqueness constraints

Constraint 22 (key-object)

The identifier field $id$ is a for the $entity(id,attrs)$ statement.
The identifier field $id$ is a for the $activity(id,t_1,t_2,attrs)$ statement.
The identifier field $id$ is a for the $agent(id,attrs)$ statement.

Constraint 23 (key-properties)

The identifier field $id$ is a for the $wasGeneratedBy(id,e,a,t,attrs)$ statement.
The identifier field $id$ is a for the $used(id,a,e,t,attrs)$ statement.
The identifier field $id$ is a for the $wasInformedBy(id,a_2,a_1,attrs)$ statement.
The identifier field $id$ is a for the $wasStartedBy(id,a_2,e,a_1,t,attrs)$ statement.
The identifier field $id$ is a for the $wasEndedBy(id,a_2,e,a_1,t,attrs)$ statement.
The identifier field $id$ is a for the $wasInvalidatedBy(id,e,a,t,attrs)$ statement.
The identifier field $id$ is a for the $wasDerivedFrom(id,e_2,e_1,a,g_2,u_1,attrs)$ statement.
The identifier field $id$ is a for the $wasAttributedTo(id,e,ag,attrs)$ statement.
The identifier field $id$ is a for the $wasAssociatedWith(id,a,ag,pl,attrs)$ statement.
The identifier field $id$ is a for the $actedOnBehalfOf(id,ag_2,ag_1,a,attrs)$ statement.
The identifier field $id$ is a for the $wasInfluencedBy(id,o2,o1,attrs)$ statement.

Constraint 24 (unique-generation)

\begin{array}{l} \forall g e n_{1}, g e n_{2}, e, a, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s G e n e r a t e d B y (g e n_{1}, e, a, t_{1}, a t t r s_{1}) \land w a s G e n e r a t e d B y (g e n_{2}, e, a, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n_{1} = g e n_{2} \end{array}

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

Constraint 25 (unique-invalidation)

\begin{array}{l} \forall i n v_{1}, i n v_{2}, e, a, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s I n v a l i d a t e d B y (i n v_{1}, e, a, t_{1}, a t t r s_{1}) \land w a s I n v a l i d a t e d B y (i n v_{2}, e, a, t_{2}, a t t r s_{2}) \\ \Rightarrow i n v_{1} = i n v_{2} \end{array}

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

Constraint 26 (unique-wasStartedBy)

\begin{array}{l} \forall s t a r t_{1}, s t a r t_{2}, a, e_{1}, e_{2}, a_{0}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s S t a r t e d B y (s t a r t_{1}, a, e_{1}, a_{0}, t_{1}, a t t r s_{1}) \land w a s S t a r t e d B y (s t a r t_{2}, a, e_{2}, a_{0}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t_{1} = s t a r t_{2} \end{array}

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

Constraint 27 (unique-wasEndedBy)

\begin{array}{l} \forall e n d_{1}, e n d_{2}, a, e_{1}, e_{2}, a_{0}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s E n d e d B y (e n d_{1}, a, e_{1}, a_{0}, t_{1}, a t t r s_{1}) \land w a s E n d e d B y (e n d_{2}, a, e_{2}, a_{0}, t_{2}, a t t r s_{2}) \\ \Rightarrow e n d_{1} = e n d_{2} \end{array}

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

Constraint 28 (unique-startTime)

\begin{array}{l} \forall s t a r t, a_{1}, a_{2}, t, t_{1}, t_{2}, e, a t t r s, a t t r s_{1} . \\ a c t i v i t y (a_{2}, t_{1}, t_{2}, a t t r s) \land w a s S t a r t e d B y (s t a r t, a_{2}, e, a_{1}, t, a t t r s_{1}) \\ \Rightarrow t_{1} = t \end{array}

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

Constraint 29 (unique-endTime)

\begin{array}{l} \forall e n d, a_{1}, a_{2}, t, t_{1}, t_{2}, e, a t t r s, a t t r s_{1} . \\ a c t i v i t y (a_{2}, t_{1}, t_{2}, a t t r s) \land w a s E n d e d B y (e n d, a_{2}, e, a_{1}, t, a t t r s_{1}) \\ \Rightarrow t_{2} = t \end{array}

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

4.6.2.2 Ordering constraints

Constraint 30 (start-precedes-end)

\begin{array}{l} \forall s t a r t, e n d, a, e_{1}, e_{2}, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s S t a r t e d B y (s t a r t, a, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \land w a s E n d e d B y (e n d, a, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t ⪯ e n d \end{array}

$\begin{array}[t]{l} \forall start,end,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow start \preceq end \end{array}$

Constraint 31 (start-start-ordering)

\begin{array}{l} \forall s t a r t_{1}, s t a r t_{2}, a, e_{1}, e_{2}, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s S t a r t e d B y (s t a r t_{1}, a, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \land w a s S t a r t e d B y (s t a r t_{2}, a, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t_{1} ⪯ s t a r t_{2} \end{array}

$\begin{array}[t]{l} \forall start_1,start_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasStartedBy(start_1,a,e_1,a_1,t_1,attrs_1) \wedge wasStartedBy(start_2,a,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow start_1 \preceq start_2 \end{array}$

Constraint 32 (end-end-ordering)

\begin{array}{l} \forall e n d_{1}, e n d_{2}, a, e_{1}, e_{2}, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s E n d e d B y (e n d_{1}, a, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \land w a s E n d e d B y (e n d_{2}, a, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow e n d_{1} ⪯ e n d_{2} \end{array}

$\begin{array}[t]{l} \forall end_1,end_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasEndedBy(end_1,a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2,a,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow end_1 \preceq end_2 \end{array}$

Constraint 33 (usage-within-activity)

$\begin{array}[t]{l} \forall start,use,a,e_1,e_2,a_1,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasStartedBy(start,a,e_1,a_1,t_1,attrs_1) \wedge used(use,a,e_2,t_2,attrs_2) \\ \quad\Rightarrow start \preceq use \end{array}$
$\begin{array}[t]{l} \forall use,end,a,e_1,e_2,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad used(use,a,e_1,t_1,attrs_1) \wedge wasEndedBy(end,a,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow use \preceq end \end{array}$

Constraint 34 (generation-within-activity)

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

Constraint 35 (wasInformedBy-ordering)

\begin{array}{l} \forall i d, s t a r t, e n d, a_{1}, a_{1}^{'}, a_{2}, a_{2}^{'}, e_{1}, e_{2}, t_{1}, t_{2}, a t t r s, a t t r s_{1}, a t t r s_{2} . \\ w a s I n f o r m e d B y (i d, a_{2}, a_{1}, a t t r s) \land w a s S t a r t e d B y (s t a r t, a_{1}, e_{1}, a_{1}^{'}, t_{1}, a t t r s_{1}) \land w a s E n d e d B y (e n d, a_{2}, e_{2}, a_{2}^{'}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t ⪯ e n d \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 \preceq end \end{array}$

Constraint 36 (generation-precedes-invalidation)

\begin{array}{l} \forall g e n, i n v, e, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s G e n e r a t e d B y (g e n, e, a_{1}, t_{1}, a t t r s_{1}) \land w a s I n v a l i d a t e d B y (i n v, e, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n ⪯ i n v \end{array}

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

Constraint 37 (generation-precedes-usage)

\begin{array}{l} \forall g e n, u s e, e, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s G e n e r a t e d B y (g e n, e, a_{1}, t_{1}, a t t r s_{1}) \land u s e d (u s e, a_{2}, e, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n ⪯ u s e \end{array}

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

Constraint 38 (usage-precedes-invalidation)

\begin{array}{l} \forall u s e, i n v, a_{1}, a_{2}, e, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ u s e d (u s e, a_{1}, e, t_{1}, a t t r s_{1}) \land w a s I n v a l i d a t e d B y (i n v, e, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow u s e ⪯ i n v \end{array}

$\begin{array}[t]{l} \forall use,inv,a_1,a_2,e,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad used(use,a_1,e,t_1,attrs_1) \wedge wasInvalidatedBy(inv,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow use \preceq inv \end{array}$

Constraint 39 (generation-generation-ordering)

\begin{array}{l} \forall g e n_{1}, g e n_{2}, e, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s G e n e r a t e d B y (g e n_{1}, e, a_{1}, t_{1}, a t t r s_{1}) \land w a s G e n e r a t e d B y (g e n_{2}, e, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n_{1} ⪯ g e n_{2} \end{array}

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

Constraint 40 (invalidation-invalidation-ordering)

\begin{array}{l} \forall i n v_{1}, i n v_{2}, e, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ w a s I n v a l i d a t e d B y (i n v_{1}, e, a_{1}, t_{1}, a t t r s_{1}) \land w a s I n v a l i d a t e d B y (i n v_{2}, e, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow i n v_{1} ⪯ i n v_{2} \end{array}

$\begin{array}[t]{l} \forall inv_1,inv_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad wasInvalidatedBy(inv_1,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e,a_2,t_2,attrs_2) \\ \quad\Rightarrow inv_1 \preceq inv_2 \end{array}$

Constraint 41 (derivation-usage-generation-ordering)

In this constraint, $a$ , $gen_2$ , or $use_1$ must not be placeholders -.

\begin{array}{l} \forall d, e_{1}, e_{2}, a, g e n_{2}, u s e_{1}, a t t r s . \\ n o t N u l l (a) \land n o t N u l l (g e n_{2}) \land n o t N u l l (u s e_{1}) \land w a s D e r i v e d F r o m (d, e_{2}, e_{1}, a, g e n_{2}, u s e_{1}, a t t r s) \\ \Rightarrow u s e_{1} ⪯ g e n_{2} \end{array}

$\begin{array}[t]{l} \forall d,e_1,e_2,a,gen_2,use_1,attrs.~ \\ \qquad notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(d,e_2,e_1,a,gen_2,use_1,attrs) \\ \quad\Rightarrow use_1 \preceq gen_2 \end{array}$

Constraint 42 (derivation-generation-generation-ordering)

In this constraint, any of $a$ , $g$ , or $u$ may be placeholders -.

\begin{array}{l} \forall d, g e n_{1}, g e n_{2}, e_{1}, e_{2}, a, a_{1}, a_{2}, g, u, t_{1}, t_{2}, a t t r s, a t t r s_{1}, a t t r s_{2} . \\ w a s D e r i v e d F r o m (d, e_{2}, e_{1}, a, g, u, a t t r s) \land w a s G e n e r a t e d B y (g e n_{1}, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \land w a s G e n e r a t e d B y (g e n_{2}, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n_{1} ≺ g e n_{2} \end{array}

$\begin{array}[t]{l} \forall d,gen_1,gen_2,e_1,e_2,a,a_1,a_2,g,u,t_1,t_2,attrs,attrs_1,attrs_2.~ \\ \qquad wasDerivedFrom(d,e_2,e_1,a,g,u,attrs) \wedge wasGeneratedBy(gen_1,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow gen_1 \prec gen_2 \end{array}$

Constraint 43 (wasStartedBy-ordering)

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

Constraint 44 (wasEndedBy-ordering)

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

Constraint 45 (specialization-generation-ordering)

\begin{array}{l} \forall g e n_{1}, g e n_{2}, e_{1}, e_{2}, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ s p e c i a l i z a t i o n O f (e_{2}, e_{1}) \land w a s G e n e r a t e d B y (g e n_{1}, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \land w a s G e n e r a t e d B y (g e n_{2}, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n_{1} ⪯ g e n_{2} \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 \preceq gen_2 \end{array}$

Constraint 46 (specialization-invalidation-ordering)

\begin{array}{l} \forall i n v_{1}, i n v_{2}, e_{1}, e_{2}, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ s p e c i a l i z a t i o n O f (e_{1}, e_{2}) \land w a s I n v a l i d a t e d B y (i n v_{1}, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \land w a s I n v a l i d a t e d B y (i n v_{2}, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow i n v_{1} ⪯ i n v_{2} \end{array}

$\begin{array}[t]{l} \forall inv_1,inv_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ \\ \qquad specializationOf(e_1,e_2) \wedge wasInvalidatedBy(inv_1,e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2,e_2,a_2,t_2,attrs_2) \\ \quad\Rightarrow inv_1 \preceq inv_2 \end{array}$

Constraint 47 (wasAssociatedWith-ordering)

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

Constraint 48 (wasAttributedTo-ordering)

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

Constraint 49 (actedOnBehalfOf-ordering)

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

4.6.2.3 Typing constraints

Constraint 50 (typing)

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

4.6.2.4 Impossibility constraints

Constraint 51 (impossible-unspecified-derivation-generation-use)

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

Constraint 52 (impossible-specialization-reflexive)

\begin{array}{l} \forall e . \\ s p e c i a l i z a t i o n O f (e, e) \\ \Rightarrow F a l s e \end{array}

$\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 two entities denoted by the first and second arguments are required to be distinct.

Constraint 53 (impossible-property-overlap)

For each $r$ and $s \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$ such that $r$ and $s$ are different relation names, the following constraint holds:

\begin{array}{l} \forall i d, a_{1}, \dots, a_{m}, b_{1}, \dots, b_{n} . \\ r (i d, a_{1}, \dots, a_{m}) \land s (i d, b_{1}, \dots, b_{n}) \\ \Rightarrow F a l s e \end{array}

$\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 classes of interactions are disjoint sets, characterized by their types.

Constraint 54 (impossible-object-property-overlap)

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

\begin{array}{l} \forall i d, a_{1}, \dots, a_{m}, b_{1}, \dots, b_{n} . \\ p (i d, a_{1}, \dots, a_{m}) \land r (i d, b_{1}, \dots, b_{n}) \\ \Rightarrow F a l s e \end{array}

$\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 interactions are distinct from other objects (entities, activities or agents).

Constraint 55 (entity-activity-disjoint)

\begin{array}{l} \forall i d . \\ t y p e O f (i d, e n t i t y) \land t y p e O f (i d, a c t i v i t y) \\ \Rightarrow F a l s e \end{array}

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

Constraint 56 (membership-empty-collection)

\begin{array}{l} \forall c, e . \\ h a s M e m b e r (c, e) \land t y p e O f (c, E m p t y C o l l e c t i o n) \\ \Rightarrow F a l s e \end{array}

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

4.7 Soundness

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

Theorem 33 (soundness-theorem)

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$ 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, proceed by induction on a terminating sequence of inference or uniqueness constraint steps: if $I$ is in normal form them we are done. If $I$ is not in normal form then if an inference is applicable, then use part 1; if a uniqueness constraint is applicable, then from $W \models I$ the uniqueness constraint cannot fail on $I$ and $W \models I'$ .

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

Finally, for part 4, suppose $W \models I$ . Then $W \models I'$ 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.

4.7.1 Syntactic Models and Completeness

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

Note

Explain how to translate PROV formulas to purely relational formulas.

4.8 Acknowledgements

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

Thanks also to Robin Berjon for the ReSPec.js specification writing tool and to MathJax for their LaTeX-to-HTML conversion tools, both of which aided in the preparation of this document.

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

Semantics of the PROV Data Model

W3C Working Draft 12 March 2013

Abstract

Status of This Document

PROV Family of Documents

Table of Contents

1. Introduction

1.1 Purpose of this document

1.2 Structure of this document

1.3 Audience

2. Basics

2.1 Identifiers

2.2 Times and Intervals

2.3 Attributes and Values

2.4 Atomic Formulas

2.5 First-Order Formulas

3. Structures and Interpretations

3.1 Things

3.2 Objects

3.2.1 Entities

3.2.1.1 Plans

3.2.2 Activities

3.2.3 Agents

3.2.4 Interactions

3.2.4.1 Events

3.2.4.2 Associations

3.2.4.3 Communications

3.2.4.4 Delegations

3.2.4.5 Derivations

3.3 Relations

Simple relations

3.3.1 Derivation paths and DerivedFrom

3.4 Putting it all together

3.5 Interpretations

4. Semantics

4.1 Satisfaction

4.2 Attribute matching

4.3 Semantics of Element Formulas

4.3.1 Entity

4.3.2 Activity

4.3.3 Agent

4.4 Semantics of Relations

4.4.1 Generation

4.4.2 Use

4.4.3 Invalidation

4.4.4 Association

4.4.5 Start Formulas

4.4.6 End

4.4.7 Attribution

4.4.8 Communication

4.4.9 Delegation

4.4.10 Derivation

4.4.10.1 Precise

4.4.10.2 Imprecise

4.4.11 Influence

4.4.12 Specialization

4.4.13 Alternate

4.4.14 Membership

4.5 Auxiliary formulas

4.5.1 Equals

4.5.2 Precedes and Strictly Precedes

4.5.3 notNull

4.5.3.1 typeOf

4.6 Inferences and Constraints

4.6.1 Inferences

4.6.2 Constraints

4.6.2.1 Uniqueness constraints

4.6.2.2 Ordering constraints

4.6.2.3 Typing constraints

4.6.2.4 Impossibility constraints

4.7 Soundness

4.7.1 Syntactic Models and Completeness

4.8 Acknowledgements

A. References

A.1 Informative references