Movatterモバイル変換

3. Structures and Interpretations

In this section we define mathematical structures $W$ that can be used tointerpret PROV formulas and instances. A structure consists of acollection of sets, functions and relations. The components of astructure $W$ are given in the rest of the section incomponents, 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.

3.1 Things

Things is a set of things in the situation being modeled.Each thing has an associated set of $E v e n t s$ and attributes whosevalues can change over time. Different kinds of $E v e n t s$ are specified further below.

To model this, a structure $W$ includes:

Component 1 (things)

a set $T h i n g s$ of things
a set $E v e n t s$ of events
a function $e v e n t s : T h i n g s \to P (E v e n t s)$ from things toassociated sets of events.
a function $v a l u e : T h i n g s \times A t t r i b u t e s \times E v e n t s \to P (V a l u e s)$ giving the possible values of each attribute of a $T h i n g$ at the instant of a given event.
Attributes are only defined during the events of a thing, thatis, $v a l u e (T, a, e v t) \neq \emptyset$ implies $e v t \in e v e n t s (T)$ .

The range of $v a l u e$ is the set $P (V a l u e s)$ , indicating that $v a l u e$ is essentially a multi-valued function that returns a set of values (possibly empty). When $v a l u e (x, a, e v t) = \emptyset$ , we say that attribute $a$ is undefined for $x$ at event $e v t$ .

Note that this description does not say what the structure of a $T h i n g$ is, only how it may be described in terms of its eventsand attribute values. A thing could be a record of fixedattribute values; it could be a bear; it could be the Royal Society;it could be a transcendental number like $π$ . All that matters fromour point of view is that we know how to map the $T h i n g$ to its events and attribute mapping.

The identity of a Thing is not observable through its attributes orevents, so it is possible for two different $T h i n g s$ to be indistinguishable by theirattribute values and events. That is, if the set of $T h i n g s = {T_{0}, T_{1}}$ and the attributes arespecified as $v a l u e (T_{0}, a, e v t) = v a l u e (T_{1}, a, e v t)$ for each $e v t \in E v e n t s$ and $a \in A t t r i b u t e s$ , this does not imply that $T_{0} = T_{1}$ .

$T h i n g s$ are associated with certain kinds of $O b j e c t s$ called $E n t i t i e s$ , defined inthe next subsection. Specifically, the function $t h i n g O f$ associatesan $E n t i t y$ to a $T h i n g$ .

3.2 Objects

$T h i n g s$ are things in the world that have attributes that can change over time. $T h i n g s$ may not have distinguishing features that are readily observable and permanent. In PROV, we do not talk explicitly about $T h i n g s$ , but instead we talk about various objects that have discrete, fixed features, and relationships among these objects. Some objects, called $E n t i t i e s$ , are associated with $T h i n g s$ , and their fixed attributes need to match those of the associated $T h i n g$ during their common events. Others correspond to agents, activities, or identifiable interactions among them.

In this section, we detail the different subsets of $O b j e c t s$ , andgive disjointness constraints and associated functions. Generally, these constraints are necessary to validatedisjointness constraints from PROV-CONSTRAINTS [PROV-CONSTRAINTS].

AnObject is described by a set of events and attributes withfixed values. Objects encompass entities, activities, agents, andinteractions (i.e., usage, generation, and other events or influence relations).To model this, a structure includes:

Component 2 (objects)

a set $O b j e c t s$
a function $e v e n t s : O b j e c t s \to P (E v e n t s)$ from objects to associated sets of events.
a function $v a l u e : O b j e c t s \times A t t r i b u t e s \to P (V a l u e s)$ .

Intuitively, $e v e n t s (e)$ is the set of events in which $e$ participated. The set $v a l u e (e, a)$ is the set of values of attribute $a$ during the object's events.

As withThings, the range of $v a l u e$ is sets of values,making $v a l u e$ effectively a multivalued function. It is alsopossible to have two different objects that are indistinguishable bytheir attributes and associated events. Objects are not things, and thesets of $O b j e c t s$ and $T h i n g s$ are disjoint; however, certain objects,namely entities, are associated with things.

Disjointness between $O b j e c t s$ and $T h i n g s$ is not necessary but is assumed in order to avoid confusion between the different categories (time-varying $T h i n g s$ vs fixed $O b j e c t s$ ).

3.2.1 Entities

Anentity is a kind of object that fixes some aspects of a thing. We assume:

Component 3 (entities)

a set $E n t i t i e s \subseteq O b j e c t s$ of entities, disjoint from $A c t i v i t i e s$ below.
a function $t h i n g O f : E n t i t i e s \to T h i n g s$ that associates each $E n t i t y$ $e$ with a $T h i n g$ , such that $e v e n t s (e) \subseteq e v e n t s (t h i n g O f (e))$ and for each $e v t \in e v e n t s (e)$ and for each attribute $a$ we have $v a l u e (e, a) \subseteq v a l u e (t h i n g O f (e), a, e v t)$ .

Although both entities and things can have undefined or multiple attribute values, their meaning is slightly different: for a thing, $v a l u e (x, a, e v t) = \emptyset$ means that the attribute $a$ has no value at event $e v t$ , whereas for an entity, $v a l u e (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 $v a l u e (t h i n g O f (e), a, e v t) = \emptyset$ when $e v t \in e v e n t s (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 $v a l u e (t h i n g O f (e), a, e v t)$ is ${1}$ at some event $e v t \in e v e n t s (e)$ and $v a l u e (t h i n g O f (e), a, e v t^{'}) = {2}$ at some other event $e v t^{'}$ . Then $v a l u e (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 $E n t i t i e s$ relate to $T h i n g s$ , we require $v a l u e (e, a) \subseteq v a l u e (t h i n g O f (e), a, e v t)$ whenever $e v t \in e v e n t s (e)$ . Intuitively, this means that if we are talking about a $T h i n g$ indirectly by describing an $E n t i t y$ , then any attributes we ascribe to the $E n t i t y$ must also describe the associated $T h i n g$ during their common events. Attributes of both $E n t i t i e s$ and $T h i n g s$ 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 $E n t i t i e s$ are associated with $T h i n g s$ , and this association is necessary to provide an interpretation for the $a l t e r n a t e O f$ and $s p e c i a l i z a t i o n O f$ relations. It might also make sense to associate $A g e n t s$ , $A c t i v i t i e s$ , and $I n t e r a c t i o n s$ with $T h i n g s$ , 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 calledplans:

Component 4 (plans)

A set $P l a n s \subseteq E n t i t i e s$ of plans.

3.2.1.2Collections

We identify another specific subset of the entities calledcollections, with the following associated structure:

Component 5 (collections)

A set $C o l l e c t i o n s \subseteq E n t i t i e s$
A membership function $m e m b e r s : C o l l e c t i o n s \to P (E n t i t i e s)$ mapping each collection to its set of members.

3.2.2 Activities

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

Component 6 (activities)

A set $A c t i v i t i e s \subseteq O b j e c t s$ of activities.
Functions $s t a r t T i m e : A c t i v i t i e s \to T i m e s$ and $e n d T i m e : A c t i v i t i e s \to T i m e s$ giving the start and end time of each activity.
Activities are disjoint from Entities: $E n t i t i e s \cap A c t i v i t i e s = \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 7 (agents)

A set $A g e n t s \subseteq O b j e c t s$ of agents.

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

3.2.4 Influences

We consider a set $I n f l u e n c e s \subseteq O b j e c t s$ which has disjoint subsets $E v e n t s$ connecting entities and activities, $A s s o c i a t i o n s$ between agents and activities, $A t t r i b u t i o n s$ between entities and agents, $C o m m u n i c a t i o n s$ between pairs of activities, $D e l e g a t i o n s$ between pairs of agents, and $D e r i v a t i o n s$ that describe chains of generation and usage steps. These kinds of influences are discussed further below. Influences are disjoint from entities, activities and agents.

Component 8 (influences)

A set $I n f l u e n c e s = E v e n t s \cup A s s o c i a t i o n s \cup C o m m u n i c a t i o n s \cup D e l e g a t i o n s \cup D e r i v a t i o n s \subseteq O b j e c t s$
The sets $E v e n t s$ , $A s s o c i a t i o n s$ , $C o m m u n i c a t i o n s$ , $D e l e g a t i o n s$ and $D e r i v a t i o n s$ are all pairwise disjoint.
Influences are disjoint from entities, agents andactivities: $I n f l u e n c e s \cap (E n t i t i e s \cup A c t i v i t i e s \cup A g e n t s) = \emptyset$
An associated function $i n f l u e n c e d : I n f l u e n c e s \to O b j e c t s \times O b j e c t s$ giving the source and target of each influence.

3.2.4.1 Events

An $E v e n t$ is an instantaneous influence that relates an activityto an entity (either of which could also be anagent). Events have types including usage, generation, invalidation, starting and ending. Events are instantaneous. We introduce:

Component 9 (events)

A set $E v e n t s \subseteq I n f l u e n c e s$ of events, partitioned into disjoint subsets $S t a r t s, E n d s, G e n e r a t i o n s, U s a g e s, I n v a l i d a t i o n s$ .
A function $t i m e : E v e n t s \to T i m e s$ .
A quasi-ordering on events $⪯\subset E v e n t s \times E v e n t s$ . We write $e ≺ e^{'}$ when $e ⪯ e^{'}$ and $e^{'} ⪯̸ e$ hold.
A function $s t a r t e d : S t a r t s \to A c t i v i t i e s \times E n t i t i e s \times A c t i v i t i e s$ , such that $s t a r t e d (s t a r t) = (a, e, a^{'})$ implies $s t a r t \in e v e n t s (a) \cap e v e n t s (e) \cap e v e n t s (a^{'})$ .
A function $e n d e d : E n d s \to A c t i v i t i e s \times E n t i t i e s \times A c t i v i t i e s$ , such that $e n d e d (e n d) = (a, e, a^{'})$ implies $e n d \in e v e n t s (a) \cap e v e n t s (e) \cap e v e n t s (a^{'})$ .
A function $u s e d : U s a g e s \to A c t i v i t i e s \times E n t i t i e s$ suchthat $u s e d (u s e) = (a, e)$ implies $u s e \in e v e n t s (a) \cap e v e n t s (e)$ .
A function $g e n e r a t e d : G e n e r a t i o n s \to E n t i t i e s \times A c t i v i t i e s$ such that $g e n e r a t e d (g e n) = (a, e)$ implies $g e n \in e v e n t s (a) \cap e v e n t s (e)$ .
A function $i n v a l i d a t e d : I n v a l i d a t i o n s \to E n t i t i e s \times A c t i v i t i e s$ such that $i n v a l i d a t e d (i n v) = (a, e)$ implies $i n v \in e v e n t s (a) \cap e v e n t s (e)$ .

3.2.4.2 Associations

An $A s s o c i a t i o n$ is an influence relating an agent to an activityand optional plan. To model associations, we introduce:

Component 10 (associations)

A set $A s s o c i a t i o n s \subseteq I n f l u e n c e s$ with associated function $a s s o c i a t e d W i t h : A s s o c i a t i o n s \to A g e n t s \times A c t i v i t i e s \times P l a n s_{⊥}$ .

3.2.4.3 Attributions

An $A t t r i b u t i o n$ is an influence relating an entity to an agent. To model attributions, we introduce:

Component 11 (attributions)

A set $A t t r i b u t i o n s \subseteq I n f l u e n c e s$ with associated function $a t t r i b u t e d T o : A t t r i b u t i o n s \to E n t i t i e s \times A g e n t s$ .

3.2.4.4Communications

A $C o m m u n i c a t i o n$ is an influence indicating exchange of information between activities. To model communications, we introduce:

Component 12 (communications)

A set $C o m m u n i c a t i o n s \subseteq I n f l u e n c e s$ with associated function $c o m m u n i c a t e d : C o m m u n i c a t i o n s \to A c t i v i t i e s \times A c t i v i t i e s$ .

3.2.4.5Delegations

A $D e l e g a t i o n$ is an influence relating two agents. To model delegations, we introduce:

Component 13 (delegations)

A set $D e l e g a t i o n s \subseteq I n f l u e n c e s$ and associated function $a c t e d F o r : D e l e g a t i o n s \to A g e n t s \times A g e n t s \times A c t i v i t i e s$

3.2.4.6 Derivations

A $D e r i v a t i o n$ is an influence chaining one or more generation and use steps. To model derivations, we introduce an auxiliary notion ofderivation path. These paths are 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}

where the $e n t_{i}$ are entities, $a c t_{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 (G e n e r a t i o n s \cdot A c t i v i t i e s \cdot U s a g e s \cdot E n t i t i e s)^{+}

with the constraints that for each derivation path:

for each substring $e n t \cdot g \cdot a c t$ we have $g e n e r a t e d (g) = (e n t, a c t)$ , and
for each substring $a c t \cdot u \cdot e n t$ we have $u s e d (u) = (a c t, e n t)$ .

Component 14 (derivations)

A set $D e r i v a t i o n s \subseteq I n f l u e n c e s$ with an associated function $d e r i v a t i o n P a t h : D e r i v a t i o n s \to D e r i v a t i o n P a t h s$ linking each derivation to a derivation path.

The $d e r i v a t i o n P a t h$ function links each $d \in D e r i v a t i o n s$ to a derivation path. A derivation has exactly one associated derivation path. However, if the PROV-N statementwasDerivedFrom(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 D e r i v a t i o n s$ .

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

3.3Additional axioms

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

Component 15 (axioms)

If $g e n e r a t e d (g) = (e, a_{1})$ and $u s e d (u) = (a_{2}, e)$ then there exists $c \in C o m m u n i c a t i o n s$ such that $c o m m u n i c a t e d (c) = (a_{2}, a_{1})$ .
If $e \in E n t i t i e s$ then there exist $g e n, i n v, a, a^{'}$ such that $g e n e r a t e d (g e n) = (e, a)$ and $i n v a l i d a t e d (i n v) = (e, a^{'})$ .
If $s t a r t e d (s t a r t) = (a_{2}, e, a_{1})$ then there exists $g e n$ such that $g e n e r a t e d (g e n) = (e, a_{1})$ .
If $e n d e d (e n d) = (a_{2}, e, a_{1})$ then there exists $g e n$ such that $g e n e r a t e d (g e n) = (e, a_{1})$ .
If $d \in D e r i v a t i o n s$ and $p r o v : R e v i s i o n \in v a l u e (d, p r o v : t y p e)$ and there exists $w \in (G e n e r a t i o n s \cup A c t i v i t i e s \cup U s e s \cup E n t i t i e s)^{*}$ such that $d e r i v a t i o n P a t h (d e r i v) = e_{2} \cdot w \cdot e_{1} \in D e r i v a t i o n P a t h s$ then $t h i n g O f (e_{1}) = t h i n g O f (e_{2})$ .
If $a t t r i b u t e d T o (a t t) = (e, a g)$ then there exist $g e n$ , $a s s o c$ and $a$ such that $g e n e r a t e d (g e n) = (e, a)$ and $a s s o c i a t e d W i t h (a s s o c) = (a, a g)$ .
If $a c t e d F o r (d e l e g) = (a g_{2}, a g_{1}, a c t)$ then there exist $a s s o c_{1}, a s s o c_{2}, p l_{1}, p l_{2}$ such that $a s s o c i a t e d W i t h (a s s o c_{1}) = (a g_{1}, a c t, p l_{1})$ and $a s s o c i a t e d W i t h (a s s o c_{2}) = (a g_{2}, a c t, p l_{2})$ .
If $g e n e r a t e d (i d) = (e, a)$ then $i n f l u e n c e d (i d) = (e, a)$ .
If $u s e d (i d) = (e, a)$ then $i n f l u e n c e d (i d) = (e, a)$ .
If $c o m m u n i c a t e d (i d) = (a_{2}, a_{1})$ then $i n f l u e n c e d (i d) = (a_{2}, a_{1})$ .
If $s t a r t e d (i d) = (a_{2}, e, a_{1})$ then $i n f l u e n c e d (i d) = (a_{2}, e)$ .
If $e n d e d (i d) = (a_{2}, e, a_{1})$ then $i n f l u e n c e d (i d) = (a_{2}, e)$ .
If $i n v a l i d a t e d (i d) = (e, a)$ then $i n f l u e n c e d (i d) = (e, a)$ .
If $d e r i v a t i o n P a t h (i d) = e_{2} \cdot w \cdot e_{1}$ then $i n f l u e n c e d (i d) = (e_{2}, e_{1})$ .
If $a t t r i b u t e d T o (i d) = (e, a g)$ then $i n f l u e n c e d (i d) = (e, a g)$ .
If $a s s o c i a t e d W i t h (i d) = (a, a g, p l)$ then $i n f l u e n c e d (i d) = (a, a g)$ .
If $a c t e d F o r (i d) = (a g_{2}, a g_{1})$ then $i n f l u e n c e d (i d) = (a g_{2}, a g_{1})$ .
If $g e n e r a t e d (g e n) = (e, a) = g e n e r a t e d (g e n^{'})$ then $g e n = g e n^{'}$ .
If $i n v a l i d a t e d (i n v) = (e, a) = i n v a l i d a t e d (i n v^{'})$ then $i n v = i n v^{'}$ .
If $s t a r t e d (s t) = (a, e_{1}, a^{'})$ and $s t a r t e d (s t^{'}) = (a, e_{2}, a^{'})$ then $s t = s t^{'}$ .
If $e n d e d (e n d) = (a, e_{1}, a^{'})$ and $e n d e d (e n d^{'}) = (a, e_{2}, a^{'})$ then $e n d = e n d^{'}$ .
If $s t a r t e d (s t) = (a, e, a^{'})$ then $s t ⪯ e v t$ for all $e v t \in e v e n t s (a) - I n v a l i d a t i o n s$ .
If $e n d e d (e n d) = (a, e, a^{'})$ then $e v t ⪯ e n d$ for all $e v t \in e v e n t s (a) - I n v a l i d a t i o n s$ .
If $g e n e r a t e d (g e n) = (e, a)$ then $g e n ⪯ e v t$ for all $e v t \in e v e n t s (e)$ .
If $i n v a l i d a t e d (i n v) = (e, a)$ then $e v t ⪯ i n v$ for all $e v t \in e v e n t s (e)$ .
For any derivation $d e r i v$ , with path $d e r i v a t i o n P a t h (d e r i v) = w$ , if $e_{2} \cdot g \cdot a \cdot u \cdot e_{1}$ is a substring of $w$ where $e_{1}, e_{2} \in E n t i t i e s$ , $g \in G e n e r a t i o n s$ , $u \in U s a g e s$ and $a \in A c t i v i t i e s$ then $u ⪯ g$ .
For any derivation $d e r i v$ , with path $d e r i v a t i o n P a t h (d e r i v) = e_{2} \cdot w \cdot e_{1}$ , if $g e n e r a t e d (g e n_{1}) = (e_{1}, a_{1})$ and $g e n e r a t e d (g e n_{2}) = (e_{2}, a_{2})$ then $g e n_{1} ≺ g e n_{2}$ .
If $a s s o c i a t e d W i t h (a s s o c) = (a, a g, p l)$ and $s t a r t e d (s t a r t) = (a, e_{1}, a_{1})$ and $i n v a l i d a t e d (i n v) = (a g, a_{2})$ then $s t a r t ⪯ i n v$ .
If $a s s o c i a t e d W i t h (a s s o c) = (a, a g, p l)$ and $g e n e r a t e d (g e n) = (a g, a_{1})$ and $e n d e d (e n d) = (a, e_{2}, a_{2})$ then $g e n ⪯ e n d$ .
If $a s s o c i a t e d W i t h (a s s o c) = (a, a g, p l)$ and $s t a r t e d (s t a r t) = (a, e_{1}, a_{1})$ and $e n d e d (e n d) = (a g, e_{2}, a_{2})$ then $s t a r t ⪯ e n d$ .
If $a s s o c i a t e d W i t h (a s s o c) = (a, a g, p l)$ and $s t a r t e d (s t a r t) = (a g, e_{1}, a_{1})$ and $e n d e d (e n d) = (a, e_{2}, a_{2})$ then $s t a r t ⪯ e n d$ .
If $a t t r i b u t e d T o (a t t r i b) = (e, a g)$ and $g e n e r a t e d (g e n_{1}) = (a g_{1}, a_{1})$ and $g e n e r a t e d (g e n_{2}) = (e, a_{2})$ then $g e n_{1} ⪯ g e n_{2}$ .
If $a t t r i b u t e d T o (a t t r i b) = (e, a g)$ and $s t a r t e d (s t a r t) = (a g_{1}, e_{1}, a_{1})$ and $g e n e r a t e d (g e n) = (e, a_{2})$ then $s t a r t ⪯ g e n$ .
If $a c t e d F o r (d e l e g) = (a g_{2}, a g_{1}, a)$ and $g e n e r a t e d (g e n) = (a g_{1}, a_{1})$ and $i n v a l i d a t e d (i n v) = (a g_{2}, a_{2})$ then $g e n ⪯ i n v$ .
If $a c t e d F o r (d e l e g) = (a g_{2}, a g_{1}, a)$ and $s t a r t e d (s t a r t) = (a g_{1}, e_{1}, a_{1})$ and $e n d e d (e n d) = (a g_{2}, e_{2}, a_{2})$ then $s t a r t ⪯ e n d$ .
If $e \in E n t i t y$ and $p r o v : e m p t y C o l l e c t i o n \in v a l u e (e, p r o v : t y p e)$ then $e \in C o l l e c t i o n s$ and $m e m b e r s (e) = \emptyset$ .

These properties are calledaxioms, 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.

3.4 Putting it all together

APROV structure $W$ is a collection of sets, functions, and relations containing all of the abovedescribed components and satisfying all of the associated propertiesand axioms. If we need to talk about the objects or relations ofmore than one structure then we may write $W_{1} . O b j e c t s$ , $W_{1} . T h i n g s$ ,etc.; otherwise, todecrease 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 $u s e d, g e n e r a t e d, i n v a l i d a t e d, s t a r t e d, e n d e d$ mapping events to their associated entities or activities, and $c o m m u n i c a t e d, a s s o c i a t e d W i t h, a t t r i b u t e d T o, a c t e d F o r$ associatingother types of influences with appropriate data.

On the other hand,some features are more distinctive, and represent areas where formalmodeling has been used to guide the development of PROV. Derivationpaths are one such distinctive feature; they correspond to anintuition that derivations may describe one or multiple generation-usesteps leading from one entity to another. Another distinctive featureis the use of $T h i n g s$ , which correspond to changing, real-worldthings, as opposed to $E n t i t i e s$ , which correspond to limited views orperspectives on $T h i n g s$ , with some fixed aspects. The semanticstructures of $T h i n g s$ and $E n t i t i e s$ provide a foundation for the $a l t e r n a t e O f$ and $s p e c i a l i z a t i o n O f$ relations.

3.5 Interpretations

We need to link identifiers to the objects they denote. We do this using a function which we shall call aninterpretation. An interpretation is a function $ρ : I d e n t i f i e r s \to O b j e c t s$ describingwhich object is the target of each identifier. The mapping from identifiers to objects maynot change over time; only $O b j e c t s$ can be denoted by $I d e n t i f i e r s$ .

4. Semantics

In what follows, let $W$ be a fixed structure with the associated sets and relations discussed in the previous section, and let $ρ$ 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 $ϕ$ , a structure $W$ and an interpretation $ρ$ .We define notation $W, ρ ⊨ ϕ$ which means that $ϕ$ is satisfied in $W, ρ$ . 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 16 (first-order-logic-semantics)

$W, ρ ⊨ T r u e$ always holds.
$W, ρ ⊨ F a l s e$ never holds.
$W, ρ ⊨ x = y$ holds if and only if $ρ (x) = ρ (y)$ .
$W, ρ ⊨ \neg ϕ$ holds if and only if $W, ρ ⊨ ϕ$ does not hold.
$W, ρ ⊨ ϕ \land ψ$ holds if and only if $W, ρ ⊨ ϕ$ and $W, ρ ⊨ ψ$ .
$W, ρ ⊨ ϕ \lor ψ$ holds if either $W, ρ ⊨ ϕ$ or $W, ρ ⊨ ψ$ .
$W, ρ ⊨ ϕ \Rightarrow ψ$ holds if $W, ρ ⊨ ϕ$ implies $W, ρ ⊨ ψ$ .
$W, ρ ⊨ \exists x . ϕ$ holds if there exists some $o b j \in O b j e c t s$ such that $W, ρ [x := o b j] ⊨ ϕ$ .
$W, ρ ⊨ \forall x . ϕ$ holds if there for every $o b j \in O b j e c t s$ we have $W, ρ [x := o b j] ⊨ ϕ$ .

In the semantics above, note that the domain of quantification is the set of $O b j e c t s$ ; that is, quantifiers range over entities, activities, agents, or influences (which are in turn further subdivided into types of influences). $T h i n g s$ 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 ${ϕ_{1}, \dots, ϕ_{n}}$ , or equivalently a single formula $\exists x_{1}, \dots, x_{k} . ϕ_{1} \land \dots \land ϕ_{n}$ , where $x_{1}, \dots, x_{k}$ are the existential variables of $I$ .

4.2 Attribute matching

We say that an object $o b j$ matches attributes $[a t t r_{1} = v a l_{1}, . . .]$ in structure $W$ provided:for each attribute $a t t r_{i}$ , we have $v a l_{i} \in W . v a l u e (o b j, a t t r_{i})$ .This is sometimes abbreviated as: $m a t c h (W, o b j, a t t r s)$ .

4.3 Semantics of Element Formulas

4.3.1 Entity

An entity formula is of the form $e n t i t y (i d, a t t r s)$ where $i d$ denotes an entity.

Entity formulas $e n t i t y (i d, a t t r s)$ can be interpreted as follows:

Semantics 17 (entity-semantics)

$W, ρ ⊨ e n t i t y (i d, a t t r s)$ holds if and only if:

[WF] $i d$ denotes an entity $e n t = ρ (i d) \in E n t i t i e s$ .
the attributes match: $m a t c h (W, e n t, a t t r s)$ .

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 $v a l u e (e, a) = {4, 5}, v a l u e (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 formulasto a single one:

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

4.3.2 Activity

An activity formula is of the form $a c t i v i t y (i d, s t, e t, a t t r s)$ where $i d$ is a identifier referring to the activity, $s t$ is a starttime and $e t$ is an end time, and $a t t r s$ are the attributes ofactivity $i d$ .

Semantics 18 (activity-semantics)

$W, ρ ⊨ a c t i v i t y (i d, s t, e t, a t t r s)$ holds if and only if:

[WF] The identifier $i d$ maps to an activity $a c t = ρ (i d) \in A c t i v i t i e s$ .
$ρ (s t) \in T i m e s$ is the activity's start time, that is: $s t a r t T i m e (a c t) = ρ (s t)$ .
$ρ (e t)$ is the activity's end time, that is: $e n d T i m e (a c t) = ρ (e t)$ .
There exists $s t a r t, e, a$ such that $s t a r t e d (s t a r t) = (a c t, e, a)$ ,and for all such start events $startTime(act) = time(start).
There exists $e n d, e^{'}, a^{'}$ such that $e n d e d (e n d) = (a c t, e^{'}, a^{'})$ , andfor all such end events $e n d T i m e (a c t) = t i m e (e n d)$ .
The attributes match: $m a t c h (W, a c t, a t t r s)$ .

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 $a c t i v i t y$ formula is asserted, we need to make sure all of the associated start and end event times match.

4.3.3 Agent

An agent formula is of the form $a g e n t (i d, a t t r s)$ where $i d$ denotes the agent and $a t t r s$ describes additional attributes.

Semantics 19 (agent-semantics)

$W, ρ ⊨ a g e n t (i d, a t t r s)$ holds if and only if:

[WF] $i d$ denotes an agent $a g = ρ (i d) \in A g e n t s$ .
The attributes match: $m a t c h (W, a g, a t t r s)$ .

4.4 Semantics of Relations

4.4.1 Generation

The generation formula is of the form $w a s G e n e r a t e d B y (i d, e, a, t, a t t r s)$ where $i d$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $a t t r s$ isa set of attribute-value pairs, and $t$ is a time.

Semantics 20 (generation-semantics)

$W, ρ ⊨ w a s G e n e r a t e d B y (i d, e, a, t, a t t r s)$ holds if and only if:

[WF] The identifier $i d$ denotes a generation event $e v t = ρ (i d) \in G e n e r a t i o n s$ .
[WF] The identifier $e$ denotes an entity $e n t = ρ (e) \in E n t i t i e s$ .
[WF] The identifier $a$ denotes an activity $a c t = ρ (a) \in A c t i v i t i e s$ .
The event $e v t$ occurred at time $ρ (t) \in T i m e s$ , i.e. $t i m e (e v t) = ρ (t)$ .
The activity $a c t$ generated $e n t$ via $e v t$ , i.e. $g e n e r a t e d (e v t) = (e n t, a c t)$ .
The attribute values match: $m a t c h (W, e v t, a t t r s)$ .

4.4.2 Use

The use formula is of the form $u s e d (i d, a, e, t, a t t r s)$ where $i d$ denotes an event, $a$ is an activity identifier, $e$ is an objectidentifier, $a t t r s$ is a set of attribute-value pairs, and $t$ is a time.

Semantics 21 (usage-semantics)

$W, ρ ⊨ u s e d (i d, a, e, t, a t t r s)$ holds if and only if:

[WF] The identifier $i d$ denotes a usage event $e v t = ρ (i d) \in U s a g e s$ .
[WF] The identifier $a$ denotes an activity $a c t = ρ (i d) \in A c t i v i t i e s$ .
[WF] The identifier $e$ denotes an entity $e n t = ρ (e) \in E n t i t i e s$ .
The event $e v t$ occurred at time $ρ (t) \in T i m e s$ ,i.e. $t i m e (e v t) = ρ (t)$ .
The activity $a c t$ used $o b j$ via $e v t$ , i.e. $u s e d (e v t) = (a c t, e n t)$ .
The attribute values match: $m a t c h (W, e v t, a t t r s)$ .

4.4.3 Invalidation

The invalidation formula is of the form $w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s)$ where $i d$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $a t t r s$ is a set of attribute-value pairs, and $t$ is a time.

Semantics 22 (invalidation-semantics)

An invalidation formula $W, ρ ⊨ w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s)$ holds if and only if:

[WF] The identifier $i d$ denotes an invalidation event $e v t = ρ (i d) \in I n v a l i d a t i o n s$ .
[WF] The identifier $e$ denotes an entity $e n t = ρ (e) \in E n t i t i e s$ .
[WF] The identifier $a$ denotes an activity $a c t = ρ (a) \in A c t i v i t i e s$ .
The event $e v t$ occurred at time $ρ (t) \in T i m e s$ , i.e. $t i m e (e v t) = ρ (t)$ .
The activity $a c t$ invalidated $e n t$ via $e v t$ , i.e. $i n v a l i d a t e d (e v t) = (e n t, a c t)$ .
The attribute values match: $m a t c h (W, e v t, a t t r s)$ .

4.4.4 Association

An association formula has the form $w a s A s s o c i a t e d W i t h (i d, a, a g, p l, a t t r s)$ .

Semantics 23 (association-plan-semantics)

$W, ρ ⊨ w a s A s s o c i a t e d W i t h (i d, a, a g, p l, a t t r s)$ holds if and only if:

[WF] $a s s o c$ denotes an association $a s s o c = ρ (i d) \in A s s o c i a t i o n s$ .
[WF] $a$ denotes an activity $a c t = ρ (a) \in A c t i v i t i e s$ .
[WF] $a g$ denotes an agent $a g e n t = ρ (a g) \in A g e n t s$ .
[WF] $p l$ denotes a plan $p l a n = ρ (p l) \in P l a n s$ .
The association associates the agent with the activity and plan, i.e. $a s s o c i a t e d W i t h (a s s o c) = (a g e n t, a c t, p l a n)$ .
The attributes match: $m a t c h (W, a s s o c, a t t r s)$ .

Semantics 24 (assocation-semantics)

$W, ρ ⊨ w a s A s s o c i a t e d W i t h (i d, a, a g, -, a t t r s)$ holds if and only if:

[WF] $a s s o c$ denotes an association $a s s o c = ρ (i d) \in A s s o c i a t i o n s$ .
[WF] $a$ denotes an activity $a c t = ρ (a) \in A c t i v i t i e s$ .
[WF] $a g$ denotes an agent $a g e n t = ρ (a g) \in A g e n t s$ .
The association associates the agent with the activity and no plan, i.e. $a s s o c i a t e d W i t h (a s s o c) = (a g e n t, a c t, ⊥)$ .
The attributes match: $m a t c h (W, a s s o c, a t t r s)$ .

4.4.5 Start

A start formula $w a s S t a r t e d B y (i d, a_{2}, e, a_{1}, t, a t t r s)$ is interpreted as follows:

Semantics 25 (start-semantics)

$W, ρ ⊨ w a s S t a r t e d B y (i d, a_{2}, e, a_{1}, t, a t t r s)$ holds if and only if:

[WF] $i d$ denotes a start event $e v t = ρ (i d) \in S t a r t s$ .
[WF] $a_{2}$ denotes an activity $a c t_{2} = ρ (a_{2}) \in A c t i v i t i e s$ .
[WF] $e$ denotes an entity $e n t = ρ (e) \in E n t i t i e s$ .
[WF] $a_{1}$ denotes an activity $a c t_{1} = ρ (a_{1}) \in A c t i v i t i e s$ .
The event happened at time $t$ , that is, $ρ (t) == t i m e (e v t)$ .
The activity $a c t_{1}$ started $a c t_{2}$ via entity $e n t$ : that is, $s t a r t e d (e v t) = (a c t_{2}, e n t, a c t_{1})$ .
The attributes match: $m a t c h (W, e v t, a t t r s)$ .

4.4.6 End

An activity end formula $w a s E n d e d B y (i d, a_{2}, e, a_{1}, t, a t t r s)$ is interpreted as follows:

Semantics 26 (end-semantics)

$W, ρ ⊨ w a s E n d e d B y (i d, a_{2}, e, a_{1}, t, a t t r s)$ holds if and only if:

[WF] $i d$ denotes an end event $e v t = ρ (i d) \in E n d s$ .
[WF] $a_{2}$ denotes an activity $a c t_{2} = ρ (a_{2}) \in A c t i v i t i e s$ .
[WF] $e$ denotes an entity $e n t = ρ (e) \in E n t i t i e s$ .
[WF] $a_{1}$ denotes an activity $a c t_{1} = ρ (a_{1}) \in A c t i v i t i e s$ .
The event happened at the end of $a c t_{2}$ , that is, $ρ (t) = e n d T i m e (a c t_{2}) = t i m e (e v t)$ .
The activity $a c t_{1}$ ended $a c t_{2}$ via entity $e n t$ : that is, $e n d e d (e v t) = (a c t_{2}, e n t, a c t_{1})$ .
The attributes match: $m a t c h (W, e v t, a t t r s)$ .

4.4.7 Attribution

An attribution formula $w a s A t t r i b u t e d T o (i d, e, a g, a t t r s)$ is interpreted as follows:

Semantics 27 (attribution-semantics)

$W, ρ ⊨ w a s A t t r i b u t e d T o (i d, e, a g, a t t r s)$ holds if and only if:

[WF] $i d$ denotes an association $a s s o c = ρ (i d) \in A s s o c i a t i o n s$ .
[WF] $e$ denotes an entity $e n t = ρ (e) \in E n t i t i e s$ .
[WF] $a g$ denotes an agent $a g e n t = ρ (a g) \in A g e n t s$ .
The entity was attributed to the agent, i.e. $a t t r i b u t e d T o (a s s o c) = (e n t, a g e n t)$ .
The attributes match: $m a t c h (W, a s s o c, a t t r s)$ .

4.4.8Communication

A communication formula $w a s I n f o r m e d B y (i d, a_{2}, a_{2}, a t t r s)$ isinterpreted as follows:

Semantics 28 (communication-semantics)

$W, ρ ⊨ w a s I n f o r m e d B y (i d, a_{2}, a_{1}, a t t r s)$ holds if and only if:

[WF] $i d$ denotes a communication $c o m m = ρ (i d) \in C o m m u n i c a t i o n s$ .
[WF] $a_{1}, a_{2}$ denote activities $a c t_{1} = ρ (a_{1}) \in A c t i v i t i e s, a c t_{2} = ρ (a_{2}) \in A c t i v i t i e s$ .
There exist $g e n, u s e, e n t$ such that $c o m m u n i c a t e d (c o m m) = (a c t_{2}, a c t_{1})$ and $g e n e r a t e d (g e n) = (e n t, a c t_{1})$ and $u s e d (u s e) = (a c t_{2}, e n t)$ .
The attributes match: $m a t c h (W, c o m m, a t t r s)$ .

4.4.9 Delegation

The $a c t e d O n B e h a l f O f (i d, a g_{2}, a g_{1}, a c t, a t t r s)$ relation is interpreted as follows:

Semantics 29 (delegation-semantics)

$W, ρ ⊨ a c t e d O n B e h a l f O f (i d, a g_{2}, a g_{1}, a c t, a t t r s)$ holds if and only if:

[WF] $i d$ denotes a delegation $d e l e g = ρ (i d) \in D e l e g a t i o n s$ .
[WF] $a$ denotes an activity $a c t = ρ (a) \in A c t i v i t i e s$ .
[WF] $a g_{1}, a g_{2}$ denote agents $a g e n t_{1} = ρ (a g_{1}), a g e n t_{2} = ρ (a g_{2}) \in A g e n t s$ .
The agent $a g e n t_{2}$ acted for the agent $a g e n t_{1}$ with respect to the activity $a c t$ , i.e. $a c t e d F o r (d e l e g) = (a g e n t_{2}, a g e n t_{1}, a c t)$ .
The attributes match: $m a t c h (W, d e l e g, a t t r s)$ .

4.4.10 Derivation

Derivation formulas can be of one of two forms:

$w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g, u, a t t r s)$ , which specifies an activity, generation and usage event. For convenience we call this aprecise derivation.
and $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)$ , which does not specify an activity, generation and usage event. For convenience we call this animprecise derivation.

4.4.10.1 Precise

A precise derivation formula has the form $w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g, u, a t t r s)$ .

Semantics 30 (derivation-precise-semantics)

$W, ρ ⊨ w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a c t, g, u, a t t r s)$ holds if and only if:

[WF] $i d$ denotes a derivation $d e r i v = ρ (i d) \in D e r i v a t i o n s$ .
[WF] $e_{1}, e_{2}$ denote entities $e n t_{1} = ρ (e_{1}), e n t_{2} = ρ (e_{2}) \in E n t i t i e s$ .
[WF] $a$ denotes an activity $a c t = ρ (a) \in A c t i v i t i e s$ .
[WF] $g$ denotes a generation event $g e n = ρ (g) \in G e n e r a t i o n s$ .
[WF] $u$ denotes a use event $u s e = ρ (u) \in U s a g e s$ .
The derivation denotes a one-step derivation path linking theentities via the activity, generation and use: $d e r i v a t i o n P a t h (d e r i v) = e n t_{2} \cdot g e n \cdot a c t \cdot u s e \cdot e n t_{1}$ .
The attribute values match: $m a t c h (W, d e r i v, a t t r s)$ .

4.4.10.2 Imprecise

An imprecise derivation formula has the form $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)$ .

Semantics 31 (derivation-imprecise-semantics)

$W, ρ ⊨ 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)$ holds if and only if:

[WF] $i d$ denotes a derivation $d e r i v = ρ (i d) \in D e r i v a t i o n s$ .
[WF] $e_{1}, e_{2}$ denote entities $e n t_{1} = ρ (e_{1}), e n t_{2} = ρ (e_{2}) \in E n t i t i e s$ .
$d e r i v a t i o n P a t h (d e r i v) = e n t_{2} \cdot w \cdot e n t_{1}$ for some $w$ .
The attribute values match: $m a t c h (W, d e r i v, a t t r s)$ .

4.4.11Influence

Semantics 32 (influence-semantics)

$W, ρ ⊨ w a s I n f l u e n c e d B y (i d, o_{2}, o_{1}, a t t r s)$ holds if and only if at least one of the following hold:

[WF] $i d$ denotes an influence $i n f = ρ (i d) \in I n f l u e n c e s$ .
[WF] $o_{1}$ and $o_{2}$ denote objects $o b j_{1} = ρ (o_{1}) \in O b j e c t s$ and $o b j_{2} = ρ (o_{2}) \in O b j e c t s$ .
The influence $i n f$ links $o_{2}$ with $o_{1}$ ; that is, $i n f l u e n c e d (i n f) = (o_{2}, o_{1})$ .
The attribute values match: $m a t c h (W, d e r i v, a t t r s)$ .

4.4.12 Specialization

The $s p e c i a l i z a t i o n O f (e_{1}, e_{2})$ relation indicates when one entity formula presents more specific aspects of another.

Semantics 33 (specialization-semantics)

$W, ρ ⊨ s p e c i a l i z a t i o n O f (e_{1}, e_{2})$ holds if and only if:

[WF] Both $e_{1}$ and $e_{2}$ are entity identifiers, denoting entities $e n t_{1} = ρ (e_{1}) \in E n t i t i e s$ and $e n t_{2} = ρ (e_{2}) \in E n t i t i e s$ .
The two entities present aspects of the same thing, that is, $t h i n g O f (e n t_{1}) = t h i n g O f (e n t_{2})$ .
The events of $e n t_{1}$ are contained in those of $e n t_{2}$ , i.e. $e v e n t s (e n t_{1}) \subseteq e v e n t s (e n t_{2})$ .
For each attribute $a t t r$ we have $v a l u e (e n t_{1}, a t t r) \supseteq v a l u e (e n t_{2}, a t t r)$ .
At least one of these inclusions is strict: that is, either $e v e n t s (e n t_{1}) ⊊ e v e n t s (e n t_{2})$ or for some $a t t r$ we have $v a l u e (e n t_{1}, a t t r) ⊋ v a l u e (e n t_{2}, a t t r)$ .

The second criterion says that the two Entities present (possibly different) aspects ofthe same Thing. Note that the third criterion allows $e n t_{1}$ and $e n t_{2}$ to have the same events (or $e v e n t s (e n t_{2})$ can be larger).The last criterion allows $e n t_{1}$ to have more defined attributes than $e n t_{2}$ , but they must include the attributes defined by $e n t_{2}$ . Two different entities that have the same attributes can also be related by specialization. The fifth criterion (indirectly) ensures that specialization is irreflexive.

4.4.13 Alternate

The $a l t e r n a t e O f$ 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 34 (alternate-semantics)

$W, ρ ⊨ a l t e r n a t e O f (e_{1}, e_{2})$ holds if and only if:

[WF] Both $e_{1}$ and $e_{2}$ are entity identifiers, denoting $e n t_{1} = ρ (e_{1})$ and $e n t_{2} = ρ (e_{2})$ .
The two objects refer to the same underlying Thing: $t h i n g O f (e n t_{1}) = t h i n g O f (e n t_{2})$

4.4.14 Membership

The $h a d M e m b e r$ relation relates a collection to an element of the collection.

Semantics 35 (membership-semantics)

$W, ρ ⊨ h a d M e m b e r (c, e)$ holds if and only if:

[WF] Both $e_{1}$ and $e_{2}$ are entity identifiers, denoting $c o l l = ρ (c) \in C o l l e c t i o n s$ and $e n t = ρ (e) \in E n t i t i e s$ .
The entity $e n t$ is a member of the collection $c o l l$ : that is, $e n t \in m e m b e r s (c o l l)$ .

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

4.5.1Precedes 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 $⪯$ . The semantics of strictly precedes ( $x strictlyPrecedes y$ ) is similar, only $x$ must take place strictly before $y$ . It is interpreted as $≺$ , which we recall is defined from $⪯$ as $x ≺ y ⟺ x ⪯ y and y ⪯̸ x$ .

Semantics 36 (precedes-semantics)

$W, ρ ⊨ x precedes y$ holds if and only if $ρ (x), ρ (y) \in E v e n t s$ and $ρ (x) ⪯ ρ (y)$ .
$W, ρ ⊨ x strictlyPrecedes y$ holds if and only if $ρ (x), ρ (y) \in E v e n t s$ and $ρ (x) ≺ ρ (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 $g e n_{1} precedes g e n_{2}$ and $g e n_{2} precedes g e n_{1}$ , but this does not imply anything about the relative orderings of the associated times, or vice versa.

4.5.2notNull

The $n o t N u l l (x)$ formula is used to specify that a value may not be the null value $⊥$ . The symbol " $-$ " always denotes the null value (i.e. $ρ (-) = ⊥$ ).

Semantics 37 (notNull-semantics)

$W, ρ ⊨ n o t N u l l (e)$ holds if and only if $ρ (e) \neq ⊥$ .

4.5.3typeOf

The typing formula $t y p e O f (x, t)$ constrains the type of the value of $x$ .

Semantics 38 (typeOf-semantics)

$W, ρ ⊨ t y p e O f (e, e n t i t y)$ holds if and only if $ρ (e) \in E n t i t i e s$ .
$W, ρ ⊨ t y p e O f (a, a c t i v i t y)$ holds if and only if $ρ (a) \in A c t i v i t i e s$ .
$W, ρ ⊨ t y p e O f (a g, a g e n t)$ holds if and only if $ρ (a g) \in A g e n t s$ .
$W, ρ ⊨ t y p e O f (c, C o l l e c t i o n)$ holds if and only if $ρ (c) \in C o l l e c t i o n s$ .
$W, ρ ⊨ t y p e O f (c, E m p t y C o l l e c t i o n)$ holds if and only if $ρ (c) \in C o l l e c t i o n s$ and $m e m b e r s (ρ (c) = \emptyset$ .

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

5.1Inferences

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}

This follows immediately from the semantics of $w a s I n f o r m e d B y$ .

Inference 6 (generation-use-communication-inference)

\begin{array}{l} \forall g e n, e, a_{1}, t_{1}, a t t r s_{1}, u s e, 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 (u s e, 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}

This follows from the semantics of $w a s I n f o r m e d B y$ andAxiom 1.

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}

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

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}

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

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}

This follows fromAxiom 3.

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}

This follows fromAxiom 4.

Inference 11 (derivation-generation-use-inference)

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

This follows from the semantics of precise derivation steps.

Inference 12 (revision-is-alternate-inference)

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

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

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}

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

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}

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

Inference 15 (influence-inference)

$\begin{array}{l} \forall i d, e, a, t, a t t r s . \\ w a s G e n e r a t e d B y (i d, e, a, t, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, e, a, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, a, e, t, a t t r s . \\ u s e d (i d, a, e, t, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, a, e, a t t r s) \end{array}$
$\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 w a s I n f l u e n c e d B y (i d, a_{2}, a_{1}, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, a_{2}, e, a_{1}, t, a t t r s . \\ w a s S t a r t e d B y (i d, a_{2}, e, a_{1}, t, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, a_{2}, e, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, a_{2}, e, a_{1}, t, a t t r s . \\ w a s E n d e d B y (i d, a_{2}, e, a_{1}, t, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, a_{2}, e, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, e, a, t, a t t r s . \\ w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, e, a, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, e_{2}, e_{1}, a, g, u, a t t r s . \\ w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g, u, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, e_{2}, e_{1}, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, e, a g, a t t r s . \\ w a s A t t r i b u t e d T o (i d, e, a g, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, e, a g, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, a, a g, p l, a t t r s . \\ w a s A s s o c i a t e d W i t h (i d, a, a g, p l, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, a, a g, a t t r s) \end{array}$
$\begin{array}{l} \forall i d, a g_{2}, a g_{1}, 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_{2}, a g_{1}, a, a t t r s) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, a g_{2}, a g_{1}, a t t r s) \end{array}$

This follows viaAxioms 8 through17.

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}

Suppose $e n t = ρ (e)$ . Clearly $e n t \in E n t i t i e s$ and $t h i n g O f (e n t) = t h i n g O f (e n t)$ , so $W, ρ ⊨ a l t e r n a t e O f (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}

Suppose $e n t_{1} = ρ (e_{1})$ and $e n t_{2} = ρ (e_{2})$ and $e n t_{3} = ρ (e_{3})$ . Then by assumption $e n t_{1}$ , $e n t_{2}$ , and $e n t_{3}$ are in $E n t i t i e s$ and $t h i n g O f (e_{1}) = t h i n g O f (e_{2})$ and $t h i n g O f (e_{2}) = t h i n g O f (e_{3})$ , so $t h i n g O f (e_{1}) = t h i n g O f (e_{3})$ , as required to conclude $W, ρ ⊨ a l t e r n a t e O f (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}

Suppose $e n t_{1} = ρ (e_{1})$ and $e n t_{2} = ρ (e_{2})$ . Then by assumption both $e n t_{1}$ and $e n t_{2}$ are in $E n t i t i e s$ and $t h i n g O f (e_{1}) = t h i n g O f (e_{2})$ , as required to conclude $W, ρ ⊨ a l t e r n a t e O f (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}

Suppose the conditions for specialization hold of $e n t_{1}$ and $e n t_{2}$ and for $e n t_{2}$ and $e n t_{3}$ , where $e n t_{1} = ρ (e_{1})$ and $e n t_{2} = ρ (e_{2})$ and $e n t_{3} = ρ (e_{3})$ . Then $e v e n t s (e_{1}) \subseteq e v e n t s (e_{2}) \subseteq e v e n t s (e_{3})$ . Moreover, $v a l u e (o b j_{2}, a t t r) \supseteq v a l u e (o b j_{3}, a t t r)$ , and similarly $v a l u e (o b j_{1}, a t t r) \supseteq v a l u e (o b j_{2}, a t t r)$ so $v a l u e (o b j_{1}, a t t r) \supseteq v a l u e (o b j_{3}, a t t r)$ . Finally, at least one of the inclusions between $o b j_{1}$ and $o b j_{2}$ is strict, so the same is the case for $o b j_{1}$ and $o b j_{3}$ .

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}

If $e n t_{1} = ρ (e_{1})$ and $e n t_{2} = ρ (e_{2})$ are specializations, then $t h i n g O f (e n t_{1}) = t h i n g O f (e n t_{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}

Suppose $e n t_{1} = ρ (e_{1})$ and $e n t_{2} = ρ (e_{2})$ . Suppose $(a t t, v)$ is an attribute-value pair in $a t t r s$ . Since $e n t i t y (e_{1}, a t t r s)$ holds, we know that $v \in v a l u e (e n t_{1}, a t t)$ . Thus $v \in v a l u e (e n t_{2}, a t t)$ since $v a l u e (e n t_{2}, a t t) \supseteq v a l u e (e n t_{1}, a t t)$ . Since this is the case for all attribute-value pairs in $a t t r s$ , and since $e_{2}$ obviously denotes an entity, we can conclude $W, ρ ⊨ e n t i t y (e_{2}, a t t r s)$ .

5.2Constraints

5.2.1Uniqueness constraints

Constraint 22 (key-object)

$\forall i d, a t t r s_{1}, a t t r s_{2} . e n t i t y (i d, a t t r s_{1}) \land e n t i t y (i d, a t t r s_{2}) \Rightarrow e n t i t y (i d, a t t r s_{1} \cup a t t r s_{2})$
$\forall i d, t_{1}, t_{1}^{'}, t_{2}, t_{2}^{'}, a t t r s_{1}, a t t r s_{2} . a c t i v i t y (i d, t_{1}, t_{2}, a t t r s_{1}) \land a c t i v i t y (i d, t_{1}^{'}, t_{2}^{'}, a t t r s_{2}) \Rightarrow a c t i v i t y (i d, t_{1}, t_{2}, a t t r s_{1} \cup a t t r s_{2}) \land t_{1} = t_{1}^{'} \land t_{2} = t_{2}^{'}$
$\forall i d, a t t r s_{1}, a t t r s_{2} . a g e n t (i d, a t t r s_{1}) \land a g e n t (i d, a t t r s_{2}) \Rightarrow a g e n t (i d, a t t r s_{1} \cup a t t r s_{2})$ .

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

Constraint 23 (key-properties)

$\begin{array}{l} \forall i d, e, e^{'}, a, a^{'}, t, t^{'}, 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 (i d, e, a, t, a t t r s) \land w a s G e n e r a t e d B y (i d, e^{'}, a^{'}, t^{'}, a t t r s_{2}) \\ \Rightarrow w a s G e n e r a t e d B y (i d, e, a, t, a t t r s_{1} \cup a t t r s_{2}) \land e = e^{'} \land a = a^{'} \land t = t^{'} \end{array}$
$\begin{array}{l} \forall i d, e, e^{'}, a, a^{'}, t, t^{'}, a t t r s_{1}, a t t r s_{2} . \\ u s e d (i d, a, e, t, a t t r s) \land u s e d (i d, a^{'}, e^{'}, t^{'}, a t t r s_{2}) \\ \Rightarrow u s e d (i d, a, e^{'}, t, a t t r s_{1} \cup a t t r s_{2}) \land e = e^{'} \land a = a^{'} \land t = t^{'} \end{array}$
$\begin{array}{l} \forall i d, a_{1}, a_{2}, a_{1}^{'}, a_{2}^{'}, 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_{1}, a_{2}, a t t r s) \land w a s I n f o r m e d B y (i d, a_{1}^{'}, a_{2}^{'}, a t t r s_{2}) \\ \Rightarrow w a s I n f o r m e d B y (i d, a_{1}, a_{2}, a t t r s_{1} \cup a t t r s_{2}) \land a_{1} = a_{1}^{'} \land a_{2} = a_{2}^{'} \end{array}$
$\begin{array}{l} \forall i d, e, e^{'} a_{1}, a_{2}, a_{1}^{'}, a_{2}^{'}, t, t^{'}, a t t r s_{1}, a t t r s_{2} . \\ w a s S t a r t e d B y (i d, a_{2}, e, a_{1}, t, a t t r s_{1}) \land w a s S t a r t e d B y (i d, a_{2}^{'}, e^{'}, a_{1}^{'}, t^{'}, a t t r s_{2}) \\ \Rightarrow w a s S t a r t e d B y (i d, a_{2}, e, a_{1}, t, a t t r s_{1} \cup a t t r s_{2}) \land a_{1} = a_{1}^{'} \land e = e^{'} \land a_{2} = a_{2}^{'} \land t = t^{'} \end{array}$
$\begin{array}{l} \forall i d, e, e^{'} a_{1}, a_{2}, a_{1}^{'}, a_{2}^{'}, t, t^{'}, a t t r s_{1}, a t t r s_{2} . \\ w a s E n d e d B y (i d, a_{2}, e, a_{1}, t, a t t r s_{1}) \land w a s E n d e d B y (i d, a_{2}^{'}, e^{'}, a_{1}^{'}, t^{'}, a t t r s_{2}) \\ \Rightarrow w a s E n d e d B y (i d, a_{2}, e, a_{1}, t, a t t r s_{1} \cup a t t r s_{2}) \land a_{1} = a_{1}^{'} \land e = e^{'} \land a_{2} = a_{2}^{'} \land t = t^{'} \end{array}$
$\begin{array}{l} \forall i d, e, e^{'}, a, a^{'}, t, t^{'}, 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 d, e, a, t, a t t r s_{1}) \land w a s I n v a l i d a t e d B y (i d, e^{'}, a^{'}, t^{'}, a t t r s_{2}) \\ \Rightarrow w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s_{1} \cup a t t r s_{2}) \land e = e^{'} \land a = a^{'} \land t = t^{'} \end{array}$
$\begin{array}{l} \forall i d, e_{1}, e_{1}^{'}, e_{2}, e_{2}^{'}, a, a^{'}, g, g^{'}, u, u^{'}, 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 (i d, e_{2}, e_{1}, a, g_{2}, u_{1}, a t t r s_{1}) \land w a s D e r i v e d F r o m (i d, e_{2}^{'}, e_{1}^{'}, a^{'}, g_{2}^{'}, u_{1}^{'}, a t t r s_{2}) \\ \Rightarrow w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g_{2}, u_{1}, a t t r s_{1} \cup a t t r s_{2}) \land e_{1} = e_{1}^{'} \land e_{2} = e_{2}^{'} \land a = a^{'} \land g = g^{'} \land u = u^{'} \end{array}$
$\begin{array}{l} \forall i d, e, e^{'}, a g, a g^{'}, a t t r s_{1}, a t t r s_{2} . \\ w a s A t t r i b u t e d T o (i d, e, a g, a t t r s_{1}) \land w a s A t t r i b u t e d T o (i d, e^{'}, a g^{'}, a t t r s_{2}) \\ \Rightarrow w a s A t t r i b u t e d T o (i d, e, a g, a t t r s_{1} \cup a t t r s_{2}) \land e = e^{'} \land a g = a g^{'} \end{array}$
$\begin{array}{l} \forall i d, a, a^{'}, a g, a g^{'}, p l, p l^{'}, a t t r s_{1}, a t t r s_{2} . \\ w a s A s s o c i a t e d W i t h (i d, a, a g, p l, a t t r s_{1}) \land w a s A s s o c i a t e d W i t h (i d, a^{'}, a g^{'}, p l^{'}, a t t r s_{2}) \\ \Rightarrow w a s A s s o c i a t e d W i t h (i d, a, a g, p l, a t t r s_{1} \cup a t t r s_{2}) \land a = a^{'} \land a g = a g^{'} \land p l = p l^{'} \end{array}$
$\begin{array}{l} \forall i d, a g_{1}, a g_{1}^{'}, a g_{2}, a g_{2}^{'}, a, a^{'}, a t t r s_{1}, a t t r s_{2} . \\ a c t e d O n B e h a l f O f (i d, a g_{2}, a g_{1}, a, a t t r s_{1}) \land a c t e d O n B e h a l f O f (i d, a g_{2}^{'}, a g_{1}^{'}, a^{'}, a t t r s_{2}) \\ \Rightarrow a c t e d O n B e h a l f O f (i d, a g_{2}, a g_{1}, a, a t t r s_{1} \cup a t t r s_{2}) \land a g_{1} = a g_{1}^{'} \land a g_{2} = a g_{2}^{'} \land a = a^{'} \end{array}$
$\begin{array}{l} \forall i d, o_{1}, o_{2}, o_{1}^{'}, o_{2}^{'}, a t t r s_{1}, a t t r s_{2} . \\ w a s I n f l u e n c e d B y (i d, o_{2}^{'}, o_{1}^{'}, a t t r s_{1}) \land w a s I n f l u e n c e d B y (i d, o_{2}^{'}, o_{1}^{'}, a t t r s_{2}) \\ \Rightarrow w a s I n f l u e n c e d B y (i d, o_{2}, o_{1}, a t t r s_{1} \cup a t t r s_{2}) \land o_{1} = o_{1}^{'} \land 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.

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}

This follows fromAxiom 18.

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}

This follows fromAxiom 19.

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}

This follows fromAxiom 20.

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}

This follows fromAxiom 21.

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}

This follows from the semantics of $w a s S t a r t e d B y$ , since the start times must both match that of the activity.

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}

This follows from the semantics of $w a s E n d e d B y$ , since the end times must both match that of the activity.

5.2.2Ordering 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 precedes e n d \end{array}

This follows fromAxiom 22.

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} precedes s t a r t_{2} \end{array}

This follows fromAxiom 22.

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} precedes e n d_{2} \end{array}

This follows fromAxiom 23.

Constraint 33 (usage-within-activity)

$\begin{array}{l} \forall s t a r t, u s e, a, e_{1}, e_{2}, a_{1}, 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 u s e d (u s e, a, e_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t precedes u s e \end{array}$
$\begin{array}{l} \forall u s e, e n d, a, e_{1}, e_{2}, a_{2}, t_{1}, t_{2}, a t t r s_{1}, a t t r s_{2} . \\ u s e d (u s e, a, e_{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 u s e precedes e n d \end{array}$

Part 1 follows fromAxiom 22 and part 2 follows fromAxiom 23.

Constraint 34 (generation-within-activity)

$\begin{array}{l} \forall s t a r t, g e n, e_{1}, e_{2}, a, a_{1}, 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 G e n e r a t e d B y (g e n, e_{2}, a, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t precedes g e n \end{array}$
$\begin{array}{l} \forall g e n, e n d, e, e_{1}, a, a_{1}, t, t_{1}, a t t r s, a t t r s_{1} . \\ w a s G e n e r a t e d B y (g e n, e, a, t, a t t r s) \land w a s E n d e d B y (e n d, a, e_{1}, a_{1}, t_{1}, a t t r s_{1}) \\ \Rightarrow g e n precedes e n d \end{array}$

Part 1 follows fromAxiom 22 and part 2 follows fromAxiom 23.

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 precedes e n d \end{array}

This follows from the semantics of $w a s I n f o r m e d B y$ ,Axiom 24, and the previous two constraints, because $w a s I n f o r m e d B y$ 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.

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 precedes i n v \end{array}

This follows fromAxiom 24.

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 precedes u s e \end{array}

This follows fromAxiom 24.

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 precedes i n v \end{array}

This follows fromAxiom 25.

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} precedes g e n_{2} \end{array}

This follows fromAxiom 24.

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} precedes i n v_{2} \end{array}

This follows fromAxiom 25.

Constraint 41 (derivation-usage-generation-ordering)

\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} precedes g e n_{2} \end{array}

This follows fromAxiom 26.

Constraint 42 (derivation-generation-generation-ordering)

\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} strictlyPrecedes g e n_{2} \end{array}

This follows fromAxiom 27.

Constraint 43 (wasStartedBy-ordering)

$\begin{array}{l} \forall g e n, s t a r t, e, a, 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 S t a r t e d B y (s t a r t, a, e, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n precedes s t a r t \end{array}$
$\begin{array}{l} \forall s t a r t, i n v, e, a, 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, 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 s t a r t precedes i n v \end{array}$

Part 1 follows fromAxiom 24. Part 2 follows fromAxiom 25.

Constraint 44 (wasEndedBy-ordering)

$\begin{array}{l} \forall g e n, e n d, e, a, 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 E n d e d B y (e n d, a, e, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n precedes e n d \end{array}$
$\begin{array}{l} \forall e n d, i n v, e, a, 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, a, 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 e n d precedes i n v \end{array}$

Part 1 follows fromAxiom 24. Part 2 follows fromAxiom 25.

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} precedes g e n_{2} \end{array}

This follows fromAxiom 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}$ .

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} precedes i n v_{2} \end{array}

This follows fromAxiom 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}$ .

Constraint 47 (wasAssociatedWith-ordering)

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

$\begin{array}{l} \forall a s s o c, s t a r t_{1}, i n v_{2}, a g, 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 A s s o c i a t e d W i t h (a s s o c, a, a g, p l, a t t r s) \land 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 I n v a l i d a t e d B y (i n v_{2}, a g, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t_{1} precedes i n v_{2} \end{array}$
$\begin{array}{l} \forall a s s o c, g e n_{1}, e n d_{2}, a g, 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 A s s o c i a t e d W i t h (a s s o c, a, a g, p l, a t t r s) \land w a s G e n e r a t e d B y (g e n_{1}, a g, 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 g e n_{1} precedes e n d_{2} \end{array}$
$\begin{array}{l} \forall a s s o c, s t a r t_{1}, e n d_{2}, a g, 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 A s s o c i a t e d W i t h (a s s o c, a, a g, p l, a t t r s) \land 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 E n d e d B y (e n d_{2}, a g, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t_{1} precedes e n d_{2} \end{array}$
$\begin{array}{l} \forall a s s o c, s t a r t_{1}, e n d_{2}, a g, 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 A s s o c i a t e d W i t h (a s s o c, a, a g, p l, a t t r s) \land w a s S t a r t e d B y (s t a r t_{1}, a g, 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 s t a r t_{1} precedes e n d_{2} \end{array}$

The four parts follow fromAxiom 28 throughAxiom 31 respectively.

Constraint 48 (wasAttributedTo-ordering)

$\begin{array}{l} \forall a t t, g e n_{1}, g e n_{2}, e, a_{1}, a_{2}, t_{1}, t_{2}, a g, a t t r s, a t t r s_{1}, a t t r s_{2} . \\ 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) \land w a s G e n e r a t e d B y (g e n_{1}, a g, 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} precedes g e n_{2} \end{array}$
$\begin{array}{l} \forall a t t, s t a r t_{1}, g e n_{2}, e, e_{1}, a_{1}, a_{2}, a g, t_{1}, t_{2}, a t t r s, a t t r s_{1}, a t t r s_{2} . \\ 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) \land w a s S t a r t e d B y (s t a r t_{1}, a g, 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, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t_{1} precedes g e n_{2} \end{array}$

These properties follow fromAxiom 32 andAxiom 33.

Constraint 49 (actedOnBehalfOf-ordering)

$\begin{array}{l} \forall d e l, g e n_{1}, i n v_{2}, a g_{1}, a g_{2}, a, a_{1}, a_{2}, t_{1}, t_{2}, a t t r s, a t t r s_{1}, a t t r s_{2} . \\ a c t e d O n B e h a l f O f (d e l, a g_{2}, a g_{1}, a, a t t r s) \land w a s G e n e r a t e d B y (g e n_{1}, a g_{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}, a g_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow g e n_{1} precedes i n v_{2} \end{array}$
$\begin{array}{l} \forall d e l, s t a r t_{1}, e n d_{2}, a g_{1}, a g_{2}, a, a_{1}, 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} . \\ a c t e d O n B e h a l f O f (d e l, a g_{2}, a g_{1}, a, a t t r s) \land w a s S t a r t e d B y (s t a r t_{1}, a g_{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_{2}, a g_{2}, e_{2}, a_{2}, t_{2}, a t t r s_{2}) \\ \Rightarrow s t a r t_{1} precedes e n d_{2} \end{array}$

These properties follow fromAxiom 34 andAxiom 35.

5.2.3Typing constraints

Constraint 50 (typing)

$\begin{array}{l} \forall e, a t t r s . \\ e n t i t y (e, a t t r s) \\ \Rightarrow t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall a g, a t t r s . \\ a g e n t (a g, a t t r s) \\ \Rightarrow t y p e O f (a g, a g e n t) \end{array}$
$\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 t y p e O f (a, a c t i v i t y) \end{array}$
$\begin{array}{l} \forall u, a, e, t, a t t r s . \\ u s e d (u, a, e, t, a t t r s) \\ \Rightarrow t y p e O f (a, a c t i v i t y) \land t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall g, a, e, t, a t t r s . \\ w a s G e n e r a t e d B y (g, e, a, t, a t t r s) \\ \Rightarrow t y p e O f (a, a c t i v i t y) \land t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall i n f, a_{2}, a_{1}, t, a t t r s . \\ w a s I n f o r m e d B y (i n f, a_{2}, a_{1}, t, a t t r s) \\ \Rightarrow t y p e O f (a_{1}, a c t i v i t y) \land t y p e O f (a_{2}, a c t i v i t y) \end{array}$
$\begin{array}{l} \forall s t a r t, a_{2}, e, a_{1}, t, a t t r s . \\ 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) \\ \Rightarrow t y p e O f (a_{1}, a c t i v i t y) \land t y p e O f (a_{2}, a c t i v i t y) \land t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall e n d, a_{2}, e, a_{1}, t, a t t r s . \\ w a s E n d e d B y (e n d, a_{2}, e, a_{1}, t, a t t r s) \\ \Rightarrow t y p e O f (a_{1}, a c t i v i t y) \land t y p e O f (a_{2}, a c t i v i t y) \land t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall i n v, a, e, t, a t t r s . \\ w a s I n v a l i d a t e d B y (i n v, e, a, t, a t t r s) \\ \Rightarrow t y p e O f (a, a c t i v i t y) \land t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall i d, e_{2}, e_{1}, a, g_{2}, u_{1}, a t t r s . \\ n o t N u l l (a) \land n o t N u l l (g_{2}) \land n o t N u l l (u_{1}) \land w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g_{2}, u_{1}, a t t r s) \\ \Rightarrow t y p e O f (e_{2}, e n t i t y) \land t y p e O f (e_{1}, a c t i v i t y) \land t y p e O f (a, a c t i v i t y) \end{array}$
$\begin{array}{l} \forall i d, e_{2}, e_{1}, a t t r s . \\ 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) \\ \Rightarrow t y p e O f (e_{2}, e n t i t y) \land t y p e O f (e_{1}, a c t i v i t y) \end{array}$
$\begin{array}{l} \forall i d, e, a g, a t t r s . \\ w a s A t t r i b u t e d T o (i d, e, a g, a t t r s) \\ \Rightarrow t y p e O f (e, e n t i t y) \land t y p e O f (a g, a g e n t) \end{array}$
$\begin{array}{l} \forall i d, a, a g, p l, a t t r s . \\ n o t N u l l (p l) \land w a s A s s o c i a t e d W i t h (i d, a, a g, p l, a t t r s) \\ \Rightarrow t y p e O f (a, a c t i v i t y) \land t y p e O f (a g, a g e n t) \land t y p e O f (p l, e n t i t y) \end{array}$
$\begin{array}{l} \forall i d, a, a g, a t t r s . \\ w a s A s s o c i a t e d W i t h (i d, a, a g, -, a t t r s) \\ \Rightarrow t y p e O f (a, a c t i v i t y) \land t y p e O f (a g, a g e n t) \end{array}$
$\begin{array}{l} \forall i d, a g_{2}, a g_{1}, 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_{2}, a g_{1}, a, a t t r s) \\ \Rightarrow t y p e O f (a g_{2}, a g e n t) \land t y p e O f (a g_{1}, a g e n t) \land t y p e O f (a, a c t i v i t y) \end{array}$
$\begin{array}{l} \forall e_{2}, e_{1} . \\ a l t e r n a t e O f (e_{2}, e_{1}) \\ \Rightarrow t y p e O f (e_{2}, e n t i t y) \land t y p e O f (e_{1}, e n t i t y) \end{array}$
$\begin{array}{l} \forall e_{2}, e_{1} . \\ s p e c i a l i z a t i o n O f (e_{2}, e_{1}) \\ \Rightarrow t y p e O f (e_{2}, e n t i t y) \land t y p e O f (e_{1}, e n t i t y) \end{array}$
$\begin{array}{l} \forall c, e . \\ h a d M e m b e r (c, e) \\ \Rightarrow t y p e O f (c, C o l l e c t i o n) \land t y p e O f (e, e n t i t y) \end{array}$
$\begin{array}{l} \forall c . \\ e n t i t y (c, [p r o v : t y p e = p r o v : e m p t y C o l l e c t i o n])) \\ \Rightarrow t y p e O f (c, e n t i t y) \land t y p e O f (c, C o l l e c t i o n) \land t y p e O f (c, E m p t y C o l l e c t i o n) \end{array}$

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

5.2.4Impossibility constraints

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

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

Each part follows from the fact that the semantics of $w a s D e r i v e d F r o m$ only allows formulas to hold when either all three of $a, g, u$ are " $-$ " (denoting $⊥$ ) 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}

This follows from the fact that in the semantics of $s p e c i a l i z a t i o n O f$ , the requirement that one of the inclusions is strict implies that the two entities cannot be the same.

Constraint 53 (impossible-property-overlap)

For each $r$ and $s \in {u s e d, w a s G e n e r a t e d B y, w a s I n v a l i d a t e d B y, w a s S t a r t e d B y, w a s E n d e d B y, w a s I n f o r m e d B y, w a s A t t r i b u t e d T o, w a s A s s o c i a t e d W i t h, a c t e d O n B e h a l f O f}$ 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}

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.

Constraint 54 (impossible-object-property-overlap)

For each $p \in {e n t i t y, a c t i v i t y, a g e n t}$ and each $r \in {u s e d, w a s G e n e r a t e d B y, w a s I n v a l i d a t e d B y, w a s S t a r t e d B y, w a s E n d e d B y, w a s I n f o r m e d B y, w a s A t t r i b u t e d T o, w a s A s s o c i a t e d W i t h, a c t e d O n B e h a l f O f, w a s I n f l u e n c e d B y}$ , 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}

This follows from the assumption that influences 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}

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}

This follows from the definition of the semantics of $t y p e O f (c, E m p t y C o l l e c t i o n)$ , which requires that there are no members of the collection denoted by $c$ .

6.Soundness and Completeness

Above we have presented arguments for the soundness of theconstraints and inferences with respect to the semantics.Here, we relate the notions ofvalidity andnormalform defined in PROV-CONSTRAINTS to the semantics.

6.1Soundness

Our main soundness result is:

Theorem 39 (soundness-theorem)

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 ⊨ I$ and $I^{'}$ is obtained from $I$ by applying one of the PROV inferences, then $W ⊨ I^{'}$ .
If $I$ is an instance and $W ⊨ I$ and $I^{'}$ is obtained from $I$ by applying one of the PROV key or uniqueness constraints, then $W ⊨ I^{'}$ .
If $I$ is an instance and $W ⊨ I$ then $I$ has a normal form $I^{'}$ and $W ⊨ I^{'}$ .
If $I$ is a normal form and $W ⊨ I$ then $I$ satisfies all of the ordering, typing and impossibility constraints.
If $W ⊨ I$ then $I$ is valid.

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

For part 2, if $W ⊨ I$ then since $W$ satisfies the logical forms of all uniqueness and key constraints, constraint application cannot fail on $I$ and $W ⊨ 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 ⊨ I$ . Then $W ⊨ 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.

6.2Weak 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 propertyweak completeness.

The termweak 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 inSection 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:

Lemma 40 (time-grounding)

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.

6.2.1Sets

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

\begin{array}{rcl} E n t i t i e s & = & {i d ∣ I ⊨ t y p e O f (i d, e n t i t y)} \\ P l a n s & = & {p l ∣ \exists i d, a g, a c, a t t r s . w a s A s s o c i a t e d W i t h (i d, a g, a c t, p l, a t t r s) \in I, p l \neq -} \\ C o l l e c t i o n s & = & {c ∣ I ⊨ t y p e O f (c, p r o v : C o l l e c t i o n) or I ⊨ t y p e O f (c, p r o v : E m p t y C o l l e c t i o n)} \\ A c t i v i t i e s & = & {i d ∣ I ⊨ t y p e O f (i d, a c t i v i t y)} \\ \cup & {a_{i d}, a_{i d}^{'} ∣ i d \in E n t i t i e s} \\ \cup & {a_{i d} ∣ \exists i d, e_{2}, e_{1} . 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) \in I} \\ A g e n t s & = & {i d ∣ I ⊨ t y p e O f (i d, a g e n t)} \\ U s a g e s & = & {i d ∣ \exists a, e, t, a t t r s . u s e d (i d, a, e, t, a t t r s) \in I} \\ \cup & {u_{i d} ∣ \exists i d, e_{2}, e_{1}, a t t r s . 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) \in I} \\ G e n e r a t i o n s & = & {i d ∣ \exists e, a, t, a t t r s . w a s G e n e r a t e d B y (i d, e, a, t, a t t r s) \in I} \\ \cup & {g_{i d} ∣ \exists i d, e_{2}, e_{1}, a t t r s . 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) \in I} \\ \cup & {g_{i d} ∣ i d \in E n t i t i e s} \\ I n v a l i d a t i o n s & = & {i d ∣ \exists e, a, t, a t t r s . w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s) \in I} \\ \cup & {i_{i d} ∣ i d \in E n t i t i e s} \\ S t a r t s & = & {i d ∣ \exists a, e, a^{'}, t, a t t r s . w a s S t a r t e d B y (i d, a, e, a^{'}, t, a t t r s) \in I} \\ E n d s & = & {i d ∣ \exists a, e, a^{'}, t, a t t r s . w a s E n d e d B y (i d, a, e, a^{'}, t, a t t r s) \in I} \\ E v e n t s & = & U s a g e s \cup G e n e r a t i o n s \cup I n v a l i d a t i o n s \cup S t a r t s \cup E n d s \\ A s s o c i a t i o n s & = & {i d ∣ \exists a g, a c t, p l, a t t r s . w a s A s s o c i a t e d W i t h (i d, a g, a c t, p l, a t t r s) \in I} \\ A t t r i b u t i o n s & = & {i d ∣ \exists e, a g, a t t r s . w a s A t t r i b u t e d T o (i d, e, a g, a t t r s) \in I} \\ D e l e g a t i o n s & = & {i d ∣ \exists a g_{2}, a g_{1}, a t t r s . a c t e d O n B e h a l f O f (i d, a g_{2}, a g_{1}, a c t, a t t r s) \in I} \\ C o m m u n i c a t i o n s & = & {i d ∣ \exists 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) \in I} \\ D e r i v a t i o n s & = & {i d ∣ \exists e_{2}, e_{1}, a, g, u, a t t r s . w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g, u, a t t r s) \in I} \\ I n f l u e n c e s & = & E v e n t s \cup A s s o c i a t i o n s \cup A t t r i b u t i o n s \cup C o m m u n i c a t i o n s \cup D e l e g a t i o n s \\ \cup & {i d ∣ \exists o_{2}, o_{1}, a t t r s . w a s I n f l u e n c e d B y (i d, o_{2}, o_{1}, a t t r s) \in I} \\ O b j e c t s & = & E n t i t i e s \cup A c t i v i t i e s \cup A g e n t s \cup I n f l u e n c e s \end{array}

In the definitions of $E n t i t i e s$ , $C o l l e c t i o n s$ , $A c t i v i t i e s$ and $A g e n t s$ we use the notation $I ⊨ t y p e O f (i d, t)$ to indicate that $i d$ must have type $t$ in $I$ according to the typing constraints. For example, for entities, this means that the set $E n t i t i e s$ contains all identifiers $e, e^{'}$ appearing in the $e n t i t y (e, a t t r s)$ , $a l t e r n a t e O f (e, e^{'})$ , or $s p e c i a l i z a t i o n O f (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 $A c t i v i t i e s$ , $G e n e r a t i o n s$ , $I n v a l i d a t i o n s$ , and $U s a g e s$ we write $a_{i d}$ , $g_{i d}$ , $i_{i d}$ and $u_{i d}$ respectively to indicate additional activities, generations and usages added for imprecise derivations or entities.

In addition, to define the set of $T h i n g s$ , we introduce an equivalence relation on $E n t i t i e s$ as follows:

e_{1} \equiv e_{2} ⟺ a l t e r n a t e O f (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 $a l t e r n a t e O f$ ensure that it is an equivalence relation. Recall that given an equivalence relation $\equiv$ on some set $X$ , theequivalence class of $x \in X$ is the set $[x]_{\equiv} = {y \in X ∣ x \equiv y}$ . Thequotient of $X$ by an equivalence relation on $X$ is the set of equivalence classes, $X_{\equiv} = {[x]_{\equiv} ∣ x \in X}$ . Now we define the set of $T h i n g s$ as the quotient of $\equiv$ -equivalence classes of $E n t i t i e s$ .

T h i n g s = E n t i t i e s /_{\equiv} = {[e]_{\equiv} ∣ e \in E n t i t i e s}

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

6.2.2Functions

First, we consider the functions associated with $E n t i t i e s$ .

\begin{array}{rcl} e v e n t s^{'} (e) & = & {i d ∣ u s e d (i d, a, e, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s G e n e r a t e d B y (i d, e, a, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s S t a r t e d B y (i d, a, e, a^{'}, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s E n d e d B y (i d, a, e, a^{'}, t, a t t r s) \in I} \\ \cup & {g_{e}, i_{e}} \\ e v e n t s (e) & = & e v e n t s^{'} (e) \cup ⋃_{s p e c i a l i z a t i o n O f (e^{'}, e) \in I} e v e n t s^{'} (e^{'}) \\ v a l u e^{'} (e, a) & = & {v ∣ e n t i t y (e, a t t r s) \in I, (a = v) \in a t t r s} (a \neq u n i q) \\ v a l u e^{'} (e, u n i q) & = & {u n i q_{e}} \\ v a l u e (e, a) & = & v a l u e^{'} (e) \cup ⋃_{s p e c i a l i z a t i o n O f (e, e^{'}) \in I} v a l u e^{'} (e^{'}) \\ t h i n g O f (e) & = & [e]_{\equiv} \end{array}

Above, we introduce a fresh attribute name $u n i q$ , not already inuse in $I$ , along with a fresh value $e$ and for each entity $e$ weadd a value $u n i q_{e}$ to $v a l u e s (e, u n i q)$ . Thisconstruction ensures that if an entity is a specialization of anotherin $I$ then the specialization relationship will hold in $M (I)$ . Wealso define the set of all events involved in $e$ as the set of eventsimmediately 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 dummygeneration and invalidation events for each entity $e$ , along withactivities $a_{e}, a_{e}^{'}$ to perform them.

Similarly, for $T h i n g s$ , weemploy an auxiliary function $e v e n t s : T h i n g s \to P (E v e n t s)$ that collects the set of allevents in which one of the entities constituting the thing participated.

\begin{array}{rcl} e v e n t s (T) & = & ⋃_{e \in T} e v e n t s (e) \\ v a l u e (T, a, e v t) & = & ⋃_{e \in T, e v t \in e v e n t s (e)} v a l u e (e, a) \end{array}

The functions $e v e n t s$ , $s t a r t T i m e$ and $e n d T i m e$ mapping activities to their start and end times are defined as follows:

\begin{array}{rcl} e v e n t s (a) & = & {i d ∣ u s e d (i d, a, e, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s G e n e r a t e d B y (i d, e, a, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s S t a r t e d B y (i d, a, e, a^{'}, t, a t t r s) \in I} \\ \cup & {i d ∣ w a s E n d e d B y (i d, a, e, a^{'}, t, a t t r s) \in I} \\ \cup & {g_{e}, i_{e}} \\ s t a r t T i m e (i d) & = & t_{1} where a c t i v i t y (a, t_{1}, t_{2}, a t t r s) \in I \\ e n d T i m e (i d) & = & t_{2} where a c t i v i t y (a, t_{1}, t_{2}, a t t r s) \in I \end{array}

The start and end times are arbitrary (say, some zero value) for activities with no $a c t i v i t y$ formula declaring the times. The above definitions of $s t a r t T i m e$ and $e n d T i m e$ ignore any start times asserted in $w a s S t a r t e d B y$ or $w a s E n d e d B y$ formulas. If both $a c t i v i t y$ and $w a s S t a r t e d B y / w a s E n d e d B y$ 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 $a c t i v i t y$ 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 $a c t i v i t y (a, [])$ statement, because it expands to $a c t i v i t y (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 $O b j e c t s$ besides $E n t i t i e s$ and $A c t i v i t i e s$ , theassociated sets of $E v e n t s$ are defined to be empty. (An $A g e n t$ thathappens to be an $E n t i t y$ or $A c t i v i t y$ will have the set of eventsdefined above for the appropriate kind of object. Note that since $E n t i t i e s$ and $A c t i v i t i e s$ are disjoint, this definition is unambiguous.)

The function $t i m e$ mapping $E v e n t s$ to their $T i m e s$ is defined as follows:

\begin{array}{rcl} t i m e (i d) & = & t where u s e d (i d, a, e, t, a t t r s) \in I \\ t i m e (i d) & = & t where w a s G e n e r a t e d B y (i d, e, a, t, a t t r s) \in I \\ t i m e (i d) & = & t where w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s) \in I \\ t i m e (i d) & = & t where w a s S t a r t e d B y (i d, a, e, a^{'}, t, a t t r s) \in I \\ t i m e (i d) & = & t where w a s E n d e d B y (i d, a, e, a^{'}, t, a t t r s) \in I \end{array}

This definition is deterministic because the sets of identifiers of different $E v e n t s$ are disjoint, and the associated times are unique.

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

\begin{array}{rcl} u s e d (i d) & = & (a, e) where u s e d (i d, a, e, t, a t t r s) \in I \\ u s e d (u_{i d}) & = & (a_{i d}, e_{1}) where 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) \in I \\ g e n e r a t e d (i d) & = & (e, a) where w a s G e n e r a t e d B y (i d, e, a, t, a t t r s) \in I \\ g e n e r a t e d (g_{i d}) & = & (e_{2}, a_{i d}) where 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) \in I \\ g e n e r a t e d (g_{e}) & = & (e, a_{e}) where e \in E n t i t i e s \\ i n v a l i d a t e d (i d) & = & (e, a) where w a s I n v a l i d a t e d B y (i d, e, a, t, a t t r s) \in I \\ i n v a l i d a t e d (i_{e}) & = & (e, a_{e}^{'}) where e \in E n t i t i e s \\ s t a r t e d (i d) & = & (a, e, a^{'}) where w a s S t a r t e d B y (i d, a, e, a^{'}, t, a t t r s) \in I \\ e n d e d (i d) & = & (a, e, a^{'}) where w a s E n d e d B y (i d, a, e, a^{'}, t, a t t r s) \in I \\ a s s o c i a t e d W i t h (i d) & = & (a g, a c t, p l) where w a s A s s o c i a t e d W i t h (i d, a g, a c t, p l, a t t r s) \in I \\ a t t r i b u t e d T o (i d) & = & (e, a g) where w a s A t t r i b u t e d T o (i d, e, a g, a t t r s) \in I \\ a c t e d F o r (i d) & = & (a g_{2}, a g_{1}, a c t) where a c t e d O n B e h a l f O f (i d, a g_{2}, a g_{1}, a c t, a t t r s) \in I \\ c o m m u n i c a t e d (i d) & = & (a_{2}, a_{1}) where w a s I n f o r m e d B y (i d, a_{2}, a_{1}, a t t r s) \in I \\ d e r i v a t i o n P a t h (i d) & = & e_{2} \cdot g \cdot a \cdot u \cdot e_{1} where w a s D e r i v e d F r o m (i d, e_{2}, e_{1}, a, g, u, a t t r s) \in I \\ d e r i v a t i o n P a t h (i d) & = & e_{2} \cdot g_{i d} \cdot a_{i d} \cdot u_{i d} \cdot e_{1} where 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) \in I \end{array}

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 $i n f l u e n c e d$ function is more involved, andis as follows:

\begin{array}{rcl} i n f l u e n c e d (i d) & = & u s e d (i d) \cup g e n e r a t e d (i d) \cup i n v a l i d a t e d (i d) \\ \cup & {(a, e) ∣ (a, e, a^{'}) \in s t a r t e d (i d)} \\ \cup & {(a, e) ∣ (a, e, a^{'}) \in e n d e d (i d)} \\ \cup & {(a g, a c t) ∣ (a g, a c t, p l) \in a s s o c i a t e d W i t h (i d)} \\ \cup & a t t r i b u t e d T o (i d) \\ \cup & {(a g_{2}, a g_{1}) ∣ (a g_{2}, a g_{1}, a c t) \in a c t e d F o r (i d)} \\ \cup & c o m m u n i c a t e d (i d) \\ \cup & {(e_{2}, e_{1}) ∣ e_{2} \cdot w \cdot e_{1} \in d e r i v a t i o n P a t h (i d)} \\ \cup & {(o_{2}, o_{1}) ∣ w a s I n f l u e n c e d B y (i d, o_{2}, o_{1}) \in I} \end{array}

This definition ensures that by construction $i n f l u e n c e d (i d)$ contains all of the other associated relationships. For any specific $i d$ , however, most of the above sets will be empty, and the finalline will often be redundant. It is not always redundant, because itis possible to assert an unspecified influence in $I$ .

It is straightforward to verify (by their definitions) that theevent sets associated with entities and activities satisfy theside-conditions inComponent 9.

Finally, the collection membership function $m e m b e r s$ is defined as follows:

m e m b e r s (c) = {e ∣ h a d M e m b e r (c, e) \in I

6.2.3Relations

We introduced a relation $\equiv$ corresponding to $a l t e r n a t e O f$ above, in defining $T h i n g s$ , but this relation is not a component of the semantics.

The event ordering relation is defined as follows:

e v t ⪯ e v t^{'} ⟺ (e v t, e v t^{'}) \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].

6.2.4Axioms

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 $t y p e o f$ .

6.2.5Main results

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

Theorem 41 (weak-completeness-theorem)

Suppose $J$ is a valid PROV instance. Then there exists a PROV structure $M$ such that $M ⊨ 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) ⊨ 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 $a l t e r n a t e O f$ and $s p e c i a l i z a t i o n O f$ since they are among the most interesting.

Suppose $a l t e r n a t e O f (e_{1}, e_{2}) \in I$ . We wish to show that $M (I) ⊨ a l t e r n a t e O f (e_{1}, e_{2})$ . Since there are no existential variables in $I$ , we know that $e_{1}, e_{2} \in M (I) . E n t i t i e s$ . Moreover, $e_{1} \equiv e_{2}$ according to the equivalence relation defined above, and so $t h i n g O f (e_{1}) = [e_{1}]_{\equiv} = [e_{2}]_{\equiv} = t h i n g O f (e_{2})$ , so we can conclude that $M (I) ⊨ a l t e r n a t e O f (e_{1}, e_{2})$ .
Suppose $s p e c i a l i z a t i o n O f (e_{1}, e_{2}) \in I$ . We wish to show that $M (I) ⊨ s p e c i a l i z a t i o n O f (e_{1}, e_{2})$ . Again, clearly $e_{1}, e_{2} \in E n t i t i e s$ , and since $I$ satisfies all inferences, we know that $a l t e r n a t e O f (e_{1}, e_{2}) \in I$ so clearly $t h i n g O f (e_{2}) = t h i n g O f (e_{1})$ as argued above. Next,
$\begin{array}{rcl} e v e n t s (e_{1}) & = & e v e n t s^{'} (e_{1}) \cup ⋃_{s p e c i a l i z a t i o n O f (e^{'}, e_{1}) \in I} e v e n t s^{'} (e^{'}) \\ \subseteq & e v e n t s^{'} (e_{2}) \cup ⋃_{s p e c i a l i z a t i o n O f (e^{'}, e_{2}) \in I} e v e n t s^{'} (e_{2}) \\ = & e v e n t s (e_{2}) \end{array}$
because $s p e c i a l i z a t i o n O f (e_{1}, e_{2}) \in I$ and all $e^{'}$ that are specializations of $e_{1}$ are also specializations of $e_{2}$ . Furthermore, for each $a t t r$ ,
$\begin{array}{rcl} v a l u e (e_{1}, a t t r) & = & v a l u e^{'} (e_{1}, a t t r) \cup ⋃_{s p e c i a l i z a t i o n O f (e_{1}, e^{'}) \in I} v a l u e^{'} (e^{'}, a t t r) \\ \supseteq & v a l u e^{'} (e_{2}, a t t r) \cup ⋃_{s p e c i a l i z a t i o n O f (e_{2}, e^{'}) \in I} v a l u e^{'} (e^{'}, a t t r) \\ = & v a l u e (e_{2}, a t t r) \end{array}$
for the same reason. Finally, by construction $u n i q_{e_{1}} \in v a l u e (e_{1}, u n i q)$ and $u n i q_{e_{1}} \notin v a l u e (e_{2}, u n i q)$ so the inclusion is strict for the special attribute $u n i q$ . Thus, we have verified all of the conditions necessary to conclude $M (I) ⊨ s p e c i a l i z a t i o n O f (e_{1}, e_{2})$ .

Next, we show how to handle a normalized, valid $I$ containsexistential variables $x_{1}, \dots, x_{n}$ . Choose fresh constants $c_{1}, \dots, c_{n}$ ofappropriate types for the existential variables and define $ρ (x_{i}) = c_{i}$ . Then $M (ρ (I)) ⊨ ρ (I)$ by the above argument.Moreover, $M (ρ (I)), ρ ⊨ I$ . So $M (ρ (I))$ is itself the desiredmodel.

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 ⊨ I$ , then $M ⊨ 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 ⊨ J^{'}$ . For each possible normalization step, we must show that if $M ⊨ J^{'}$ then $M ⊨ J$ .

First consider inference steps. These add information, that is, $J^{'} \supseteq J$ . Hence it is immediate that $M ⊨ 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 (i d, a_{1}, \dots, a_{n}, a t t r s_{1}), r (i d, b_{1}, \dots, b_{n}, a t t r s_{2})}$ and $J^{'} = S (J_{0}) \cup {r (i d, S (a_{1}), \dots, S (a_{n}), a t t r s_{1} \cup a t t r s_{2})}$ , where $S$ is a unifying substitution making $S (a_{i}) = S (b_{i})$ for each $i \in {1, \dots, n}$ . Since $M ⊨ J^{'}$ , we must have $M, ρ ⊨ J^{'}$ for some $ρ$ , and therefore we must also have that $M, ρ ⊨ S (J_{0})$ and $M, ρ ⊨ r (i d, S (a_{1}), \dots, S (a_{n}), a t t r s_{1} \cup a t t r s_{2})$ . We can extend $ρ$ to a valuation $ρ^{'}$ such that $M, ρ^{'} ⊨ S (x_{1}) = x_{1} \land \dots \land S (x_{k}) = x_{k}$ where $d o m (S) = {x_{1}, \dots, x_{k}}$ . Also, $M, ρ^{'} ⊨ J_{0}$ and $M, ρ^{'} ⊨ r (i d, a_{1}, \dots, a_{n}, a t t r s_{1} \cup a t t r s_{2})$ . Moreover, since $S$ is a unifier, we also have $M, ρ^{'} ⊨ r (i d, b_{1}, \dots, b_{n}, a t t r s_{1} \cup a t t r s_{2})$ . Finally, since we can always remove attributes from an atomic formula without damaging its satisfiability, we can conclude that $M, ρ^{'} ⊨ r (i d, a_{1}, \dots, a_{n}, a t t r s_{1}) \land r (i d, b_{1}, \dots, b_{n}, a t t r s_{2})$ . To conclude, we have shown $M ⊨ J_{0} \cup {r (i d, a_{1}, \dots, a_{n}, a t t r s_{1}), r (i d, b_{1}, \dots, b_{n}, a t t r s_{2})}$ , that is, $M ⊨ J$ , as desired.

Movatterモバイル変換

Semantics of the PROV Data Model

W3C Working Group Note 30 April 2013

Abstract

Status of This Document

PROV Family of Documents

Implementations Encouraged

Please Send Comments

Table of Contents

1.Introduction

1.1Purpose of this document

1.2Structure of this document

1.3 Audience

2. Basics

2.1 Identifiers

2.2 Attributes and Values

2.3 Times

2.4Atomic Formulas

2.5First-Order Formulas

3. Structures and Interpretations

3.1 Things

3.2 Objects

3.2.1 Entities

3.2.1.1 Plans

3.2.1.2Collections

3.2.2 Activities

3.2.3 Agents

3.2.4 Influences

3.2.4.1 Events

3.2.4.2 Associations

3.2.4.3 Attributions

3.2.4.4Communications

3.2.4.5Delegations

3.2.4.6 Derivations

3.3Additional axioms

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

4.4.6 End

4.4.7 Attribution

4.4.8Communication

4.4.9 Delegation

4.4.10 Derivation

4.4.10.1 Precise

4.4.10.2 Imprecise

4.4.11Influence

4.4.12 Specialization

4.4.13 Alternate

4.4.14 Membership

4.5Semantics of Auxiliary Formulas

4.5.1Precedes and Strictly Precedes

4.5.2notNull

4.5.3typeOf

5. Inferences and Constraints

5.1Inferences

5.2Constraints

5.2.1Uniqueness constraints

5.2.2Ordering constraints

5.2.3Typing constraints

5.2.4Impossibility constraints

6.Soundness and Completeness

6.1Soundness

6.2Weak Completeness

6.2.1Sets

6.2.2Functions

6.2.3Relations

6.2.4Axioms

6.2.5Main results