From Provenance WG Wiki

(Difference between revisions)

Revision as of 13:57, 9 January 2013

Overview

Status

This is work in progress. The semantics is being updated to be consistent with the Candidate Recommendation of PROV. The plan is to release the semantics as a Note over the next few months. At that point, the wiki pages containing drafts of the semantics will be superseded.

Idea of the semantics

As a starting point, I will assume that we intend the assertions made in a PROV-DM instance to be intended to describe one, consistent state of the world, much like a logical formula is said to be satisfied in a mathematical model. That is, I propose an approach similar to that taken in model theory, where the PROV-DM instance corresponds to a formula or theory of a logic, and the semantics corresponds to what logicians call a model.

For example, the formula $\forall x. P(x) \Rightarrow Q(x)$ is satisfied in a mathematical model where the relation $P$ denotes a set of elements that is contained in that denoted by $Q$ . Here, the goal is to come up with a plausible "intended model" for interpreting PROV-DM instances, where the formulas are assertions in PROV-DM and the individuals are things and agents. This is complicated by the fact that many statements about provenance involve talking about objects that change over time.

The word "world" is used in PROV-DM to talk about the actual state of affairs that the PROV-DM instance describes, which is what I would usually call a "model". The word "model" is used in PROV-DM mainly in the sense of "data model", that is, to talk about what I would otherwise call the syntax of PROV-DM. To avoid confusion with the uses of terms in PROV-DM, I will use "world model" to describe the mathematical structure that corresponds to actual state of affairs, and will try to avoid ambiguous, unqualified uses of the word "model".

Axiomatization and relationship to PROV-CONSTRAINTS

One goal of the semantics is to link the procedural specification of validity and equivalence with traditional notions of logical consistency and equivalence of theories, for example in first-order logic. A first-order axiomatization that corresponds to the formal constraints and is sound for reasoning about the models described below is in progress at the end of the document.

Basics

I will use syntax for PROV-DM records (which I will usually call formulas) as described in the Candidate Recommendation of PROV-DM (PROV-DM CR).

A PROV-DM instance, or set of atomic formulas $φ 1$ ... $φ n$ , is interpreted as a conjunction, that is, the overall instance is considered to hold in a given structure if each atomic formula in it holds.

The rest of the document will discuss the structures and define when an atomic assertion holds in a given world.

Identifiers

A lowercase symbol $x, y,...$ on its own denotes an identifier. Identifiers may or may not be URIs. I view identifiers as being like variables in logic (or blank nodes in RDF): just because we have two different identifiers $x$ and $y$ doesn't tell us that they denote different things, since we could discover that they are actually the same later. We write $I d e n t i f i e r s$ for the set of identifiers of interest in a given situation (typically, the set of identifiers present in the PROV instance of interest).

Times and Intervals

We assume a linearly ordered set $(Times,\leq)$ of time instants. For convenience we assume the order is total or linear order, corresponding to a linear timeline; however, PROV does not assume that time is linear and events could be partially ordered and not necessarily reconciled to a single global clock.

We also consider a set $I n t e r v a l s$ of closed intervals of the form $\{t \mid t_1 \leq t \leq t_2\}$ .

Attributes and Values

We assume a set $A t t r i b u t e s$ of attribute labels and a set $V a l u e s$ of possible values of attributes.

Formulas

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

Each parameter is either an identifier, a constant (e.g. a time or other literal value in an attribute list), or a null symbol "-". Null symbols can only appear in the specified arguments in $w a s A s s o c i a t e d W i t h$ and $w a s D e r i v e d F r o m$ , as shown in the grammar below.

$\begin{array}{rcl} formula &::=& element\_formula\\ & | & relation\_formula\\ element\_formula &::= &entity(id,attrs) \\ & |& activity(id,st,et,attrs)\\ & |& agent(id,attrs)\\ relation\_formula &::=& wasGeneratedBy(id,e,a,t,attrs)\\ & |& used(id,e,a,t,attrs)\\ & |& wasInvalidatedBy(id,e,a,t,attrs)\\ & |& wasAssociatedWith(id,ag,act,pl,attrs)\\ & |& wasAssociatedWith(id,ag,act,-,attrs)\\ & |& wasStartedBy(id,a_2,e,a_1,attrs)\\ & |& wasEndedBy(id,a_2,e,a_1,attrs)\\ & |& wasAttributedTo(id,e,ag,attrs)\\ & |& actedOnBehalfOf(if,ag_2,ag_1,act,attrs)\\ & |& wasDerivedFrom(id,e_2,e_1,act,g,u,attrs)\\ & |& wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)\\ & |& alternateOf(e_1,e_2)\\ & |& specializationOf(e_1,e_2) \end{array}$

World Models

Things

Things are things in the world. Each thing has a lifetime during which it exists and attributes whose values can change over time.

To model this, a world model $W$ includes

a set $T h i n g s$ of things
a function $lifetime : Things \to Intervals$ from objects to time intervals
a function $value : Things \times Attributes \times Times \to Values_\bot$

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

The range of the $v a l u e$ function us $Values_\bot$ , that is, $Values \uplus \{\bot\}$ , the set of values with an additional element $\bot \notin Values$ . When $value(x,a,t) = \bot$ , we say that attribute $a$ is undefined for $x$ at time $t$ .

It is possible for two Things to be indistinguishable by their attribute values and lifetime, but have different identity.

Objects

A Object is described by a time interval and attributes with unchanging values. Objects encompass entities, interactions, and activities.

To model this, a world includes

a set $O b j e c t s$
a function $lifetime : Objects \to Intervals$ from objects to time intervals
a function $value : Objects \times Attributes \to Values_\bot$

Intuitively, $l i f e t i m e (e)$ is the time interval during which object $e$ exists. The value $v a l u e (e, a)$ is the value of attribute $a$ during the object's lifetime.

As with Things, the range of $v a l u e$ includes the special undefined value $\bot$ , making $v a l u e$ effectively a partial function. It is also possible to have two different objects that are indistinguishable by their attributes and time intervals. Objects are not things, and the sets of $O b j e c t s$ and $T h i n g s$ are disjoint; however, certain objects, namely entities, are linked to things.

Entities

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

a set $Entities \subseteq Objects$ of entities, disjoint from $A c t i v i t i e s$ and $E v e n t s$ below.
a function $thingOf : Entities \to Things$ that associates each Entity with a Thing, such that for each $t \in lifetime(obj)$ , and for each attribute $a$ such that $value(obj,a) \neq \bot$ , we have $v a l u e (o b j, a) = v a l u e (t h i n g O f (o b j), a, t)$ .
$lifetime(e) \subseteq lifetime(t)$ .

Remark: Although both entities and things can have undefined attribute values, their meaning is slightly different: for a thing, $value(x,a,t) = \bot$ means that the attribute $a$ has no value at time $t$ , whereas for an entity, $value(x,a) = \bot$ only means that the entity does not record a fixed value for $a$ . This does not imply that $value(thingOf(e),a,t) = \bot$ when $t \in lifetime(e)$ . In particular, if the $v a l u e (x, a, t)$ has multiple values during the lifetime of $e$ , then $v a l u e (e, a)$ must be $\bot$ , since assigning a value to $v a l u e (e, a)$ would violate condition (3) above.

Plans

We identify a specific subset of the entities called plans, $Plans \subseteq Entities$ .

Agents

An agent is an entity that can act, by controlling, starting, ending, or participating in activities. Agents can act on behalf of other agents. We introduce:

a set $Agents \subseteq Objects$ of agents.

Actvities

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

a set $Activities \subseteq Objects$ of activities, disjoint from $E n t i t i e s$ and $E v e n t s$

Interactions

We consider a $Interactions \subseteq Objects$ which are split into Events between entities and activities, Associations between agents and activities, and Derivations that describe chains of generation and usage steps. (The first two sets may overlap.) Interactions are disjoint from entities, activities and agents.

$Interactions = (Events \cup Associations) \cup Derivations \subseteq Objects$
$(Events \cup Associations) \cap Derivations = \emptyset$
$Interactions \cap (Entities \cup Activities \cup Agents) = \emptyset$

Events

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

A set $Events \subseteq Interactions$ of events.
A function $time : Events \to Times$ giving the time of each event; i.e. $l i f e t i m e (e v t) = {t i m e (t)}$ .
The derived ordering on events given by $evt_1 \leq evt_2 \iff time(evt_1) \leq time(evt_2)$
A function $type: Events \to \{start,end,use,generate\}$ such that Events have types in ${s t a r t, e n d, u s e, g e n e r a t e}$ .

Associations

An Association is an interaction relating an agent to an activity. Associations can overlap with events; for example, a start event is also an association. To model associations, we introduce:

A set $Associations \subseteq Interactions$ , such that every event $evt \in Events$ that is a start or end event is also an association. That is, $type(evt) \in \{start,end\}$ implies $evt \in Associations$

Associations are used below in the $A c t s F o r$ and $A s s o c i a t e d W i t h$ relations. Add types for association or delegation?

Derivations

A Derivation is an interaction chaining one or more generation and use steps. Derivations can also carry attributes, so we introduce an explicit kind of interaction for them that can carry attributes.

A set $Derivations \subseteq Interactions$ , disjoint from $Events \cup Associations$ .

See below for the associated derivation path and DerivedFrom relation.

Relations

Simple relations

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

A relation $Used \subseteq Events \times Entities$ saying when an event used an entity. An event can use at most one entity, and if $(evt,e)\in Used$ then $time(evt) \in lifetime(e)$ and $t y p e (g) = u s e$ must hold.
A relation $Generated \subseteq Events \times Entities$ saying when an event generated an entity. An event can generate at most one entity, and if $(evt,e)\in Generated$ then $m i n (l i f e t i m e (e)) = t i m e (e v t)$ and $t y p e (g) = g e n e r a t i o n$ must hold.
A relation $Invalidated \subseteq Events \times Entities$ saying when an event invalidated an entity. An event can invalidate at most one entity, and if $(evt,e)\in Invalidated$ then $m i n (l i f e t i m e (e)) = t i m e (e v t)$ and $t y p e (g) = i n v a l i d a t i o n$ must hold.
A relation $EventActivity \subseteq Events \times Activities$ associating activities with events, such that $(act,evt) \in EventActivity$ implies $time(evt) \in lifetime(act)$ .
A relation $AssociatedWith \subseteq Association \times Agents \times Activities \times Plans^?$ indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan.
A relation $ActsFor \subseteq Agents \times Agents \times Activities$ indicating when one agent acts on behalf of another with respect to a given activity.

Derivation paths and DerivedFrom

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

$ent_n\cdot g_n\cdot act_n\cdot u_n\cdot ent_{n-1}\cdot ...\cdot ent_1\cdot g_1\cdot act_1\cdot u_1\cdot ent_0$ where the $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:

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

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

and we use this language to give meaning to derivations:

A function $derivedFrom : Derivations \to DerivationPaths$

Note: The reason why we need paths and not just individual derivation steps is that imprecise wasDerivedFrom formulas can represent multiple derivation steps.

Putting it all together

A world model W is a structure containing all of the above described data. If we need to talk about the objects or relations of more than one world model then we may write $W 1 . O b j e c t s$ ; otherwise, to decrease notational clutter, when we consider a fixed world model then the names of the sets, relations and functions above refer to the components of that model.

TODO: List the components.

Semantics

In what follows, let $W$ be a fixed world model with the associated sets and relations discussed in the previous section, and let $I$ be an interpretation of identifiers as objects in $W$ .

The annotations [WF] refer to well-formedness constraints that correspond to typing constraints.

Interpretations

We need to link identifiers to the objects they denote. We do this using a function which we shall call an interpretation.

The mapping from identifiers to objects may not change over time. Thus, we consider interpretations as follows:

An interpretation function $I : Identifiers \to Objects$ describing which object is the target of each identifier.

Satisfaction

Consider an atomic formula $φ$ , a world $W$ and an interpretation $I$ . We define notation $W,I \models \phi$ which means that $φ$ is satisfied in $W, I$ . For basic assertions, the definition of the satisfaction relation is given in the next few subsections. For a conjunction of assertions $\phi_1,\ldots,\phi_n$ we write $W,I \models \phi_1,\ldots,\phi_n$ to indicate that $W,I \models \phi_1$ and ... and $W,I \models \phi_n$ hold.

TODO: Satisfiability of additional formulas to explain constraints/inferences

Attribute matching

We say that an object $o b j$ matches attributes $[a t t r 1 = v a l 1,...]$ in world $W$ provided:

for each attribute $a t t r i$ , we have $W . v a l u e (o b j, a t t r i) = v a l i$ .

This is sometimes abbreviated as: $m a t c h (W, o b j, a t t r s)$

Semantics of Element Records

Entity Records

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 assertions $e n t i t y (i d, a t t r s)$ can be interpreted as follows:

$W,I \models entity(id,attrs)$ if and only if:

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

For example, the following formulas both hold if $x$ denotes an entity $e$ such that $v a l u e (e, a) = 4, v a l u e (e, b) = 5, v a l u e (e, c) = 6$ hold:

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

Activity Records

An activity record 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 start time and $e t$ is an end time.

We say that $W,I \models activity(id,st,et,attrs)$ if and only if:

[WF] The identifier $i d$ maps to an activity $act = I(id) \in Activities$
If $s t$ is specified then it is equal to the start time of the activity, that is: $m i n (l i f e t i m e (i d)) = s t$
If $e t$ is specified then it is equal to the end time of the activity, that is: $m a x (l i f e t i m e (i d)) = e t$
The attributes match: $m a t c h (W, a c t, a t t r s)$ .

Agent Records

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.

Agent assertions $a g e n t (i d, a t t r s)$ can be interpreted as follows:

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

[WF] $i d$ denotes an agent $ag = I(id) \in Agents$
The attributes match: $m a t c h (W, a g, a t t r s)$ .

Semantics of Relations

Entity-Activity

Generation

The generation assertion 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$ is a set of attribute-value pairs, and $t$ is an optional time.

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

[WF] The identifier $i d$ denotes an event $evt = I(id) \in Events$
[WF] The identifier $e$ denotes an entity $ent = I(e) \in Entities$
[WF] The identifier $a$ denotes an activity $act = I(a) \in Activities$ .
The event $e v t$ is involved in $a c t$ , that is, such that $(evt,act) \in EventActivities$ .
The type of $e v t$ is $g e n e r a t i o n$ , i.e. $t y p e (e v t) = g e n e r a t i o n$
The event $e v t$ occurred at time $t$ , i.e. $t i m e (e v t) = t$
The event $e v t$ generated $e n t$ , i.e. $(evt,ent) \in Generated$ .
The attribute values match: $m a t c h (W, e v t, a t t r s)$

Use

The use assertion 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 object identifier, $a t t r s$ is a set of attribute-value pairs, and $t$ is an optional time.

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

[WF] The identifier $i d$ denotes an event $evt = I(id) \in Events$
[WF] The identifier $a$ denotes an activity $act = I(id) \in Activities$
[WF] The identifier $e$ denotes an entity $ent = I(e) \in Entities$
The event $e v t$ is part of $a c t$ , i.e. $(evt,act) \in EventActivities$ .
The type of $e v t$ is $u s e$ , i.e., $t y p e (e v t) = u s e$ .
The event $e v t$ occurred at time $t$ , i.e. $t i m e (e v t) = t$
The event $e v t$ used $o b j$ , i.e. $(evt,ent) \in Used$ .
The attribute values match: $m a t c h (W, e v t, a t t r s)$

Invalidation

The invalidation assertion 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 an optional time.

$W,I \models wasInvalidatedBy(id,e,a,t,attrs)$ if and only if:

[WF] The identifier $i d$ denotes an event $evt = I(id) \in Events$
[WF] The identifier $e$ denotes an entity $ent = I(e) \in Entities$
[WF] The identifier $a$ denotes an activity $act = I(a) \in Activities$ .
The event $e v t$ is involved in $a c t$ , that is, such that $(evt,act) \in EventActivities$ .
The type of $e v t$ is $i n v a l i d a t i o n$ , i.e. $t y p e (e v t) = i n v a l i d a t i o n$
The event $e v t$ occurred at time $t$ , i.e. $t i m e (e v t) = t$
The event $e v t$ invalidated $e n t$ , i.e. $(evt,ent) \in Invalidated$ .
The attribute values match: $m a t c h (W, e v t, a t t r s)$

Agent-Activity

Association Records

An association record 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)$ .

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

[WF] $a s s o c$ denotes an association $assoc = I(id) \in Associations$ .
[WF] $a$ denotes an activity $act = I(a) \in Activities$ .
[WF] $a g$ denotes an agent $agent = I(ag) \in Agents$ .
[WF] $p l$ is either the placeholder $-$ or denotes a plan $plan=I(pl) \in Plans$ .
The association associates the agent with the activity and plan, i.e. $(assoc,agent,act,plan) \in AssociatedWith$ .
The attributes match: $m a t c h (W, a s s o c, a t t r s)$ .

Start Records

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

$W,I \models wasStartedBy(id,a2,e,a1,attrs)$ holds if and only if:

[WF] $i d$ denotes an event $evt = I(id) \in Events$
[WF] $a 2$ denotes an activity $a c t 2 = I (a 2)$
[WF] $e$ denotes an entity $e n t = I (e)$
[WF] $a 1$ denotes an activity $a c t 1 = I (a 1)$
The event $e v t$ has type $s t a r t$ , i.e. $t y p e (e v t) = s t a r t$ .
The event happened at the start of $a c t 2$ , that is, $(act2,evt) \in ActivitiesEvents$ , and $m i n (l i f e t i m e (a c t 2)) = t i m e (e v t)$ .
The event happened during $a c t 1$ , that is, $(act1,evt) \in ActivitiesEvents$ .
The attributes match: $m a t c h (W, e v t, a t t r s)$ .

End Records

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

$W,I \models wasEndedBy(id,a2,e,a1,attrs)$ holds if and only if:

[WF] $i d$ denotes an event $evt = I(id) \in Events$
[WF] $a 2$ denotes an activity $a c t 2 = I (a 2)$
[WF] $e$ denotes an entity $e n t = I (e)$
[WF] $a 1$ denotes an activity $a c t 1 = I (a 1)$
The event $e v t$ has type $e n d$ , i.e. $t y p e (e v t) = e n d$ .
The event happened at the end of $a c t 2$ , that is, $(act2,evt) \in ActivitiesEvents$ , and $m a x (l i f e t i m e (a c t 2)) = t i m e (e v t)$ .
The event happened during $a c t 1$ , that is, $(act1,evt) \in ActivitiesEvents$ .
The attributes match: $m a t c h (W, e v t, a t t r s)$ .

Agent-Entity

Attribution Records

An attribution record $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:

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

[WF] $i d$ denotes an event $e v t = I (i d)$ that is also an association $evt \in Associations$
[WF] $e$ denotes an entity $e n t = I (e)$
[WF] $a g$ denotes an agent $a g e n t = I (a g)$
The event $e v t$ has type $a t t r i b u t i o n$ , i.e. $t y p e (e v t) = a t t r i b u t i o n$ .
The entity was attributed to the agent, i.e. $(id,ent,ag) \in AttributedTo$
The attributes match: $m a t c h (W, e v t, a t t r s)$ .

Agent-Agent

Responsibility

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 using the $A c t s F o r$ relation as follows:

$W,I \models actedOnBehalfOf(id,ag2,ag1,act,attrs)$ holds if and only if:

[WF] $i d$ denotes an association $assoc=I(id) \in Associations$ that is an association interaction, and $t y p e (i d) = r e s p o n s i b i l i t y$ .
[WF] $a$ denotes an activity $act=I(a) \in Activities$ is an activity.
[WF] $a g 1, a g 2$ denote agents $agent1=I(ag1), agent2=I(ag2) \in Agents$ are agents.
The agent $a g e n t 2$ acts for the agent $a g e n t 1$ with respect to the activity $a c t$ , i.e. $(agent2,agent1,act) \in ActsFor$ .
[Redundant?] The association $i d$ associates both agents with the activity, i.e. $(assoc,agent1,act),(assoc,agent2,act) \in AssociatedWith$ .
The attributes match: $m a t c h (W, a s s o c, a t t r s)$ .

Entity-Entity

Derivation

Precise

A precise derivation record 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)$ .

$W,I \models wasDerivedFrom(id,e2,e1,act,g,u,attrs)$ if and only if:

[WF] $i d$ denotes a derivation $deriv = I(id) \in Derivations$
[WF] $e 1, e 2$ denote entities $ent1 = I(e1), ent2=I(e2) \in Entities$
[WF] $a$ denotes an activity $act = I(a) \in Activities$
[WF] $g$ denotes a generation event $gen = I(g) \in Events$ and $t y p e (I (g)) = g e n e r a t i o n$
[WF] $u$ denotes a use event $I(u) \in Events$ and $t y p e (I (u)) = u s e$
The derivation denotes a valid one-step derivation $derivedFrom(deriv) = I(e2) \cdot I(g) \cdot I(act) \cdot I(u) \cdot I(e1)$
The attribute values match: $m a t c h (W, d e r i v, a t t r s)$ .

Imprecise

An imprecise derivation record 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)$ .

$W,I \models wasDerivedFrom(id,e2,e1,-,-,-,attrs)$ if and only if there exists $path \in DerivationPaths$ such that:

[WF] $i d$ denotes a derivation $deriv = I(id) \in Derivations$
[WF] $e 1, e 2$ denote entities $ent1 = I(e1), ent2=I(e2) \in Entities$
$derivedFrom(deriv)= ent2 \cdot w \cdot ent1$ for some $w$
The attribute values match: $m a t c h (W, d e r i v, a t t r s)$ .

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 record presents more specific aspects of another.

$W,I \models specializationOf(e1,e2)$ if and only if:

[WF] Both $e 1$ and $e 2$ are entity identifiers, denoting $ent_1 = I(e1) \in Entities$ and $ent_2 = I(e2) \in Entities$ .
The two Entities refer to 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 lifetime of $o b j 1$ is contained in that of $e n t 2$ ,i.e. $lifetime(ent_1) \subseteq lifetime(ent_2)$ .
For each attribute such that $value(obj_2,a) \neq \bot$ we have $v a l u e (o b j 1, a t t r) = v a l u e (o b j 2, a t t r)$ .

The second criterion says that the two Entities present aspects of the same Thing. Note that the third criterion allows $o b j 1$ and $o b j 2$ to have the same lifetime (or that of $o b j 2$ can be larger). The last criterion allows $o b j 1$ to have more defined attributes than $o b j 2$ , but they must agree on the attributes defined by $o b j 2$ .

Remark: There has been discussion whether $s p e c i a l i z a t i o n O f$ is transitive and/oranti-symmetric:

Transitivity: If $s p e c i a l i z a t i o n O f (a, b)$ and $s p e c i a l i z a t i o n O f (b, c)$ hold then $s p e c i a l i z a t i o n O f (a, c)$ hold. This holds for the above definition.
Antisymmetry: If $s p e c i a l i z a t i o n O f (a, b)$ and $s p e c i a l i z a t i o n O f (b, a)$ hold then $a = b$ . This doesn't follow from the current definition (but it would if we stipulated that two entities that have the same interval, attribute and thing are equal).

Alternate

The $a l t e r n a t e O f$ relation indicates when two entity records present (possibly different) aspects of the same thing. The two entities may or may not overlap in time.

$W,I \models alternateOf(e1,e2)$ if and only if:

[WF] Both $e 1$ and $e 2$ are entity identifiers, denoting $e n t 1 = I (e 1)$ and $e n t 2 = I (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)$

Remark: There has been discussion whether $a l t e r n a t e O f$ is symmetric and transitive:

Symmetry: If $a l t e r n a t e O f (a, b)$ holds then $a l t e r n a t e O f (b, a)$ holds.
Transitivity: If $a l t e r n a t e O f (a, b)$ and $a l t e r n a t e O f (b, c)$ hold then $a l t e r n a t e O f (a, c)$ hold. This holds of the above definition.

We also consider the following properties which have been suggested:

$s p e c i a l i z a t i o n O f (e 1, e 2)$ implies $a l t e r n a t e O f (e 1, e 2)$ ? (This holds at the moment.)
$a l t e r n a t e O f (a, b)$ if and only if there exists c such that $s p e c i a l i z a t i o n O f (a, c)$ and $s p e c i a l i z a t i o n O f (b, c)$ ? This does not necessarily hold without further assumptions about the Entities.

Axiomatization

Definitional Rules

The definitions are essentially used to map the compact notation and implicit placeholder notation used n PROV-N with the abstract syntax of PROV-DM used in the rest of this semantics. We can formalize the definitional expansion rules as follows:

Definition 1 (optional-identifiers)

For each $r \in \{ used, wasGeneratedBy, wasInvalidatedBy, wasInfluencedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasDerivedFrom, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$ the following axioms hold:

$r(a_1,...,a_n) \iff \exists id.~ r(id; a_1,...,a_n)$
$r(-; a_1,...,a_n) \iff \exists id.~ r(id; a_1,...,a_n)$

Definition 2 (optional-attributes)

For each p in {entity, activity, agent}, if $a n$ is not an attribute list parameter then the following definitional rule holds: $p(a_1,...,a_n) \iff p(a_1,...,a_n,[])$
For each $r \in \{ used, wasGeneratedBy, wasInvalidated, wasInfluencedBy, wasStartedBy, wasEndedBy, wasInformedBy, wasDerivedFrom, wasAttributedTo, wasAssociatedWith, actedOnBehalfOf\}$ , if $a n$ is not an attribute list parameter then the following definition holds:

$r(id; a_1,...,a_n) \iff r(id; a_1,...,a_n,[])$

Definition 3 (definition-short-forms)

$\forall id,attrs. ~ activity(id,attrs) \iff activity(id,-,-,attrs)$
$\forall id, e, attrs. ~ wasGeneratedBy(id; e,attrs) \iff wasGeneratedBy(id; e,-,-,attrs)$
$\forall id,a,attrs. ~ used(id; a,attrs) \iff used(id; a,-,-,attrs)$
$\forall id,a,attrs. ~ wasStartedBy(id; a,attrs) \iff wasStartedBy(id; a,-,-,-,attrs)$
$\forall id,a,attrs. ~ wasEndedBy(id; a,attrs) \iff wasEndedBy(id; a,-,-,-,attrs)$
$\forall id,e,attrs. ~ wasInvalidatedBy(id; e,attrs) \iff wasInvalidatedBy(id; e,-,-,attrs)$
$\forall id,e1,e2,attrs. ~ wasDerivedFrom(id; e2,e1,attrs) \iff wasDerivedFrom(id; e2,e1,-,-,-,attrs)$
$\forall id,e,attrs. ~ wasAssociatedWith(id; e,attrs) \iff wasAssociatedWith(id; e,-,-,attrs)$
$\forall id,a1,a2,attrs. ~ actedOnBehalfOf(id; a2,a1,attrs) \iff actedOnBehalfOf(id; a2,a1,-,attrs)$

Definition 4 (optional-placeholders)

$activity(id,-,t2,attrs) \iff \exists t1.~ activity(id,t1,t2,attrs)$ . Here, t2 may be a placeholder.
$activity(id,t1,-,attrs) \iff \exists t2.~activity(id,t1,t2,attrs)$ . Here, t1 must not be a placeholder.
For each $r \in \{ used, wasGeneratedBy, wasStartedBy, wasEndedBy, wasInvalidatedBy, wasAssociatedWith, actedOnBehalfOf \}$ , if the $i$ th parameter of $r$ is an expandable parameter of $r$ as specified in Table 3 of PROV-CONSTRAINTS then the following definition holds:

$r(a_0;...,a_{i-1}, -, a_{i+1}, ...,a_n) \iff \exists a'.~ r(a_0;...,a_{i-1},a',a_{i+1},...,a_n)$ .

$a \neq - \Rightarrow (wasDerivedFrom(id;e2,e1,a,-,u,attrs) \iff \exists g.~ wasDerivedFrom(id; e2,e1,a,g,u,attrs))$
$a \neq - \Rightarrow (wasDerivedFrom(id;e2,e1,a,g,-,attrs) \iff \exists u.~ wasDerivedFrom(id; e2,e1,a,g,u,attrs))$ .

Inference Rules

Inference 5 (communication-generation-use-inference)

$\forall id, a_2,a_1,attrs. wasInformedBy(id; a_2,a_1,attrs) \Longrightarrow \exists e, gen, t_1, use, t_2. wasGeneratedBy(gen; e,a_1,t_1,[]) \wedge used(use; a_2,e,t_2,[])$

Inference 6 (generation-use-communication-inference)

$\forall gen, a_1, t_1, attrs_1,id_2,a_2,t_2,attrs_2.~wasGeneratedBy(gen; e,a_1,t_1,attrs_1) \wedge used(id_2; a_2,e,t_2,attrs_2) \Longrightarrow \exists id.~wasInformedBy(id; a_2,a_1,[])$

Inference 7 (entity-generation-invalidation-inference)

$\forall e,attrs.~entity(e,attrs) \Longrightarrow \exists gen,a_1,t_1,inv,a_2,t_2.~wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge wasInvalidatedBy(inv,e,a_2,t_2,[])$

Inference 8 (activity-start-end-inference)

$\forall a, t_1, t_2, attrs.~ activity(a,t_1,t_2,attrs) \Longrightarrow \exists start, e_1, a_1, end, a_2, e_2.~ wasStartedBy(start; a,e_1,a_1,t_1,[]) \wedge wasEndedBy(end; a,e_2,a_2,t_2,[])$

Inference 9 (wasStartedBy-inference)

$\forall id, a, e_1, a_1, t, attrs.~ wasStartedBy(id; a,e_1,a_1,t,attrs), \Longrightarrow \exists gen, t_1.~ wasGeneratedBy(gen; e_1,a_1,t_1,[])$

Inference 10 (wasEndedBy-inference)

$\forall id, a, e_1, a_1, t, attrs.~ wasEndedBy(id; a,e_1,a_1,t,attrs), \Longrightarrow \exists gen, t_1 .~ wasGeneratedBy(gen; e_1,a_1,t_1,[])$

Inference 11 (derivation-generation-use-inference)

In this inference, none of a, gen2 or use1 can be placeholders -.

$\forall id, e_2, e_1, a, gen_2, use_1, attrs.~ wasDerivedFrom(id; e_2,e_1,a,gen_2,use_1,attrs) \Longrightarrow \exists t_1,t_2 .~ used(use_1; a,e_1,t_1,[]) \wedge wasGeneratedBy(gen_2; e_2,a,t_2,[])$

Inference 12 (revision-is-alternate-inference)

In this inference, any of a, g or u may be placeholders.

$\forall id, e_1, e_2, a, g,u.~ wasDerivedFrom(id; e_2,e_1,a,g,u,[prov:type='prov:Revision']) \Longrightarrow alternateOf(e_2,e_1)$

Inference 13 (attribution-inference)

$\forall att, e, ag, attrs.~ wasAttributedTo(att; e,ag,attrs) \Longrightarrow \exists a, t, gen, assoc, pl .~ wasGeneratedBy(gen; e,a,t,[]) \wedge wasAssociatedWith(assoc; a,ag,pl,[])$

Inference 14 (delegation-inference)

$\forall id, ag_1, ag_2, a, attrs.~ actedOnBehalfOf(id; ag_1, ag_2, a, attrs) \Longrightarrow \exists id_1, pl_1, id_2, pl_2 .~ wasAssociatedWith(id_1; a, ag_1, pl_1, []) \wedge wasAssociatedWith(id_2; a, ag_2, pl_2, [])$

Inference 15 (influence-inference)

$\forall id, e, a, t, attrs.~ wasGeneratedBy(id; e,a,t,attrs) \Longrightarrow wasInfluencedBy(id; e, a, attrs)$
$\forall id, a, e, t, attrs.~ used(id; a,e,t,attrs) \Longrightarrow wasInfluencedBy(id; a, e, attrs)$
$\forall id, a_2, a_1, attrs.~ wasInformedBy(id; a_2,a_1,attrs) \Longrightarrow wasInfluencedBy(id; a_2, a_1, attrs)$
$\forall id, a_2, e, a_1, t, attrs.~ wasStartedBy(id; a_2,e,a_1,t,attrs) \Longrightarrow wasInfluencedBy(id; a_2, e, attrs)$
$\forall id, a_2, e, a_1, t, attrs.~ wasEndedBy(id; a_2,e,a_1,t,attrs) \Longrightarrow wasInfluencedBy(id; a_2, e, attrs)$
$\forall id, e, a, t, attrs.~ wasInvalidatedBy(id; e,a,t,attrs) \Longrightarrow wasInfluencedBy(id; e, a, attrs)$
$\forall id, e_2, e_1, a, g, u, attrs.~ wasDerivedFrom(id; e_2, e_1, a, g, u, attrs) \Longrightarrow wasInfluencedBy(id; e_2, e_1, attrs).$ Here, a, g, u may be placeholders -.
$\forall id, e, ag, attrs.~ wasAttributedTo(id; e,ag,attrs) \Longrightarrow wasInfluencedBy(id; e, ag, attrs)$
$\forall id, a, ag, pl, attrs.~ wasAssociatedWith(id; a,ag,pl,attrs) \Longrightarrow wasInfluencedBy(id; a, ag, attrs)$ Here, pl may be a placeholder -.
$\forall id, ag_2, ag_1, a, attrs.~ actedOnBehalfOf(id; ag_2,ag_1,a,attrs) \Longrightarrow wasInfluencedBy(id; ag_2, ag_1, attrs)$

TODO: In 4 and 5, should e be a1? Otherwise these two rules are redundant since the influence of e on a2 can also be derived using other inferences.

Inference 16 (alternate-reflexive)

$\forall e.~ entity(e) \Longrightarrow alternateOf(e,e)$

Inference 17 (alternate-transitive)

$\forall e_1, e_2, e_3.~ alternateOf(e_1,e_2) \wedge alternateOf(e_2,e_3) \Longrightarrow alternateOf(e_1,e_3)$

Inference 18 (alternate-symmetric)

$\forall e_1, e_2.~ alternateOf(e_1,e_2) \Longrightarrow alternateOf(e_2,e_1)$

Inference 19 (specialization-transitive)

$\forall e_1, e_2, e_3 .~ specializationOf(e_1,e_2) \wedge specializationOf(e_2,e_3) \Longrightarrow specializationOf(e_1,e_3)$

Inference 20 (specialization-alternate-inference)

$\forall e_1, e_2.~ specializationOf(e_1,e_2) \Longrightarrow alternateOf(e_1,e_2)$

Inference 21 (specialization-attributes-inference)

$\forall e_1, attrs, e_2.~ entity(e_1, attrs) \wedge specializationOf(e_2,e_1), \Longrightarrow entity(e_2, attrs)$

Constraints

Constraint 22 (key-object)

The identifier field id is a KEY for the $e n t i t y (i d, a t t r s)$ statement.
The identifier field id is a KEY for the $a c t i v i t y (i d, t 1, t 2, a t t r s)$ statement.
The identifier field id is a KEY for the $a g e n t (i d, a t t r s)$ statement.

Constraint 23 (key-properties)

The identifier field id is a KEY for the $w a s G e n e r a t e d B y (i d; e, a, t, a t t r s)$ statement.
The identifier field id is a KEY for the $u s e d (i d; a, e, t, a t t r s)$ statement.
The identifier field id is a KEY for the $w a s I n f o r m e d B y (i d; a 2, a 1, a t t r s)$ statement.
The identifier field id is a KEY for the $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)$ statement.
The identifier field id is a KEY for the $w a s E n d e d B y (i d; a 2, e, a 1, t, a t t r s)$ statement.
The identifier field id is a KEY for the $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)$ statement.
The identifier field id is a KEY for the $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)$ statement.
The identifier field id is a KEY for the $w a s A t t r i b u t e d T o (i d; e, a g, a t t r)$ statement.
The identifier field id is a KEY for the $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)$ statement.

The identifier field id is a KEY for 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, a t t r s)$ statement.
The identifier field id is a KEY for the $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)$ statement.

Constraint 24 (unique-generation)

$\forall gen_1,gen_2,e,a,t_1,t_2,attrs_1,attrs_2.~ wasGeneratedBy(gen_1; e,a,t_1,attrs_1) \wedge wasGeneratedBy(gen_2; e,a,t_2,attrs_2), \Longrightarrow gen_1 = gen_2.$

Constraint 25 (unique-invalidation)

$\forall inv_1,inv_2,e,a,t_1,t_2,attrs_1,attrs_2 .~ wasInvalidatedBy(inv_1; e,a,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2; e,a,t_2,attrs_2), \Longrightarrow inv_1 = inv_2.$

Constraint 26 (unique-wasStartedBy)

$\forall start_1,start_2,a,e_1,e_2,a_0,t_1,t_2,attrs_1,attrs_2 .~ wasStartedBy(start_1; a,e_1,a_0,t_1,attrs_1) \wedge wasStartedBy(start_2; a,e_2,a_0,t_2,attrs_2), \Longrightarrow start_1 = start_2.$

Constraint 27 (unique-wasEndedBy)

$\forall end_1,end_2,a,e_1,e_2,a_0,t_1,t_2,attrs_1,attrs_2 .~ wasEndedBy(end_1; a,e_1,a0,t_1,attrs_1) \wedge wasEndedBy(end_2; a,e_2,a0,t_2,attrs_2), \Longrightarrow end_1 = end_2.$

Constraint 28 (unique-startTime)

$\forall start,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1 .~ activity(a_2,t_1,t_2,attrs) \wedge wasStartedBy(start; a_2,e,a_1,t,attrs_1) \Longrightarrow t_1=t.$

Constraint 29 (unique-endTime)

$\forall end,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1.~ activity(a_2,t_1,t_2,attrs) \wedge wasEndedBy(end; a_2,e,a_1,t,attrs_1) \Longrightarrow t_2 = t.$

Constraint 30 (start-precedes-end)

$\forall start,end,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasStartedBy(start; a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end; a,e_2,a_2,t_2,attrs_2) \Longrightarrow start \preceq end.$

Constraint 31 (start-start-ordering)

$\forall start_1,start_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasStartedBy(start_1; a,e_1,a_1,t_1,attrs_1) \wedge wasStartedBy(start_2; a,e_2,a_2,t_2,attrs_2) \Longrightarrow start_1 \preceq start_2.$

Constraint 32 (end-end-ordering)

$\forall end_1,end_2,a,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasEndedBy(end_1; a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2; a,e_2,a_2,t_2,attrs_2) \Longrightarrow end_1 \preceq end2.$

Constraint 33 (usage-within-activity)

$\forall start,use,a,e_1,e_2,a_1,t_1,t_2,attrs_1,attrs_2 .~ wasStartedBy(start; a,e_1,a_1,t_1,attrs_1) \wedge used(use; a,e_2,t_2,attrs_2) \Longrightarrow start \preceq use.$
$\forall use,end,a,e_1,e_2,a_2,t_1,t_2,attrs_1,attrs_2 .~ used(use; a,e_1,t_1,attrs_1) \wedge wasEndedBy(end; a,e_2,a_2,t_2,attrs_2) \Longrightarrow use \preceq end.$

Constraint 34 (generation-within-activity)

$\forall start,gen,e_1,e_2,a,a_1,t_1,t_2,attrs_1,attrs_2 .~ wasStartedBy(start; a,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen; e_2,a,t_2,attrs_2) \Longrightarrow start \preceq gen.$
$\forall gen,end,e,e_1,a,a_1,t,t_1,attrs,attrs_1 .~ wasGeneratedBy(gen; e,a,t,attrs) \wedge wasEndedBy(end; a,e_1,a_1,t_1,attrs_1) \Longrightarrow gen \preceq end.$

Constraint 35 (wasInformedBy-ordering)

$\forall id,start,end,a_1,a_1',a_2,a_2',e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2 .~ wasInformedBy(id; a_2,a_1,attrs) \wedge wasStartedBy(start; a_1,e_1,a_1',t_1,attrs_1) \wedge wasEndedBy(end; a_2,e_2,a_2',t_2,attrs_2) \Longrightarrow start \preceq end.$

Constraint 36 (generation-precedes-invalidation)

$\forall gen,inv,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasGeneratedBy(gen; e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv; e,a_2,t_2,attrs_2) \Longrightarrow gen \preceq inv.$

Constraint 37 (generation-precedes-usage)

$\forall gen,use,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasGeneratedBy(gen; e,a_1,t_1,attrs_1) \wedge used(use; a_2,e,t_2,attrs_2) \Longrightarrow gen \preceq use.$

Constraint 38 (usage-precedes-invalidation)

$\forall use,inv,a_1,a_2,e,t_1,t_2,attrs_1,attrs_2 .~ used(use; a_1,e,t_1,attrs_1) \wedge wasInvalidatedBy(inv; e,a_2,t_2,attrs_2) \Longrightarrow use \preceq inv.$

Constraint 39 (generation-generation-ordering)

$\forall gen_1,gen_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasGeneratedBy(gen_1; e,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2; e,a_2,t_2,attrs_2) \Longrightarrow gen_1 \preceq gen_2.$

Constraint 40 (invalidation-invalidation-ordering)

$\forall inv_1,inv_2,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasInvalidatedBy(inv_1; e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2; e,a_2,t_2,attrs_2) \Longrightarrow inv_1 \preceq inv_2.$

Constraint 41 (derivation-usage-generation-ordering)

In this constraint, $a$ , $g e n 2$ , $u s e 1$ must not be placeholders.

$\forall d,e_1,e_2,a,gen_2,use_1,attrs .~ notNull(a) \wedge notNull(gen_2) \wedge notNull(use_1) \wedge wasDerivedFrom(d; e_2,e_1,a,gen_2,use_1,attrs) \Longrightarrow use_1 \preceq gen_2.$

Constraint 42 (derivation-generation-generation-ordering)

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

$\forall d,gen_1,gen_2,e_1,e_2,a,a_1,a_2,g,u,t_1,t_2,attrs,attrs_1,attrs_2 .~ wasDerivedFrom(d; e_2,e_1,a,g,u,attrs) \wedge wasGeneratedBy(gen_1; e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2; e_2,a_2,t_2,attrs_2) \Longrightarrow gen_1 \prec gen_2.$

Constraint 43 (wasStartedBy-ordering)

$\forall gen,start,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasGeneratedBy(gen; e,a_1,t_1,attrs_1) \wedge wasStartedBy(start; a,e,a_2,t_2,attrs_2) \Longrightarrow gen \preceq start.$
$\forall start,inv,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasStartedBy(start; a,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv; e,a_2,t_2,attrs_2) \Longrightarrow start \preceq inv.$

Constraint 44 (wasEndedBy-ordering)

$\forall gen,end,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasGeneratedBy(gen; e,a_1,t_1,attrs_1) \wedge wasEndedBy(end; a,e,a_2,t_2,attrs_2) \Longrightarrow gen \preceq end.$
$\forall end,inv,e,a,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasEndedBy(end; a,e,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv; e,a_2,t_2,attrs_2) \Longrightarrow end \preceq inv.$

Constraint 45 (specialization-generation-ordering)

$\forall gen_1,gen_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ specializationOf(e_2,e_1) \wedge wasGeneratedBy(gen_1; e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2; e_2,a_2,t_2,attrs_2) \Longrightarrow gen_1 \preceq gen_2.$

Constraint 46 (specialization-invalidation-ordering)

$\forall inv_1,inv_2,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ specializationOf(e_1,e_2) \wedge wasInvalidatedBy(inv_1; e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2; e_2,a_2,t_2,attrs_2) \Longrightarrow inv_1 \preceq inv_2.$

Constraint 47 (wasAssociatedWith-ordering)

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

$\forall assoc,start_1,inv_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasAssociatedWith(assoc; a,ag,pl,attrs) \wedge wasStartedBy(start_1; a,e_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2; ag,a_2,t_2,attrs_2) \Longrightarrow start_1 \preceq inv_2.$
$\forall assoc,gen_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasAssociatedWith(assoc; a,ag,pl,attrs) \wedge wasGeneratedBy(gen_1; ag,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2; a,e_2,a_2,t_2,attrs_2) \Longrightarrow gen_1 \preceq end_2.$
$\forall assoc,start_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2.~ wasAssociatedWith(assoc; a,ag,pl,attrs) \wedge wasStartedBy(start_1; a,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2; ag,e_2,a_2,t_2,attrs_2) \Longrightarrow start_1 \preceq end_2.$
$\forall assoc,start_1,end_2,ag,e_1,e_2,a_1,a_2,t_1,t_2,attrs_1,attrs_2 .~ wasAssociatedWith(assoc; a,ag,pl,attrs) \wedge wasStartedBy(start_1; ag,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end_2; a,e_2,a_2,t_2,attrs_2) \Longrightarrow start_1 \preceq end_2.$

Constraint 48 (wasAttributedTo-ordering)

$\forall att,gen_1,gen_2,e,a_1,a_2,t_1,t_2,ag,attrs,attrs_1,attrs_2 .~ wasAttributedTo(att; e,ag,attrs) \wedge wasGeneratedBy(gen_1; ag,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2; e,a_2,t_2,attrs_2) \Longrightarrow gen_1 \preceq gen_2.$
$\forall att,start_1,gen_2,e,e_1,a,a_2,ag,t_1,t_2,attrs,attrs_1,attrs_2 .~ wasAttributedTo(att; e,ag,attrs) \wedge wasStartedBy(start_1; ag,e_1,a_1,t_1,attrs_1) \wedge wasGeneratedBy(gen_2; e,a_2,t_2,attrs_2) \Longrightarrow start_1 \preceq gen_2.$

Constraint 49 (actedOnBehalfOf-ordering)

$\forall del,gen_1,inv_2,ag_1,ag_2,a,a_1,a_2,t_1,t_2,attrs,attrs_1,attrs_2 .~ actedOnBehalfOf(del; ag_2,ag_1,a,attrs) \wedge wasGeneratedBy(gen_1; ag_1,a_1,t_1,attrs_1) \wedge wasInvalidatedBy(inv_2; ag_2,a_2,t_2,attrs_2) \Longrightarrow gen_1 \preceq inv_2.$
$\forall del,start_1,end_2, ag_1,ag_2,a,a_1,a_2,e_1,e_2,t_1,t_2,attrs,attrs_1,attrs_2 .~ actedOnBehalfOf(del; ag_2,ag_1,a,attrs) \wedge wasStartedBy(start_1; ag_1,e_1,a_1,t_1,attrs_1) \wedge wasEndedBy(end2; ag_2,e_2,a_2,t_2,attrs_2) \Longrightarrow start_1 \preceq end2.$

Constraint 50 (typing)

$\forall e,attrs .~ entity(e,attrs) \Longrightarrow entity \in typeOf(e).$
$\forall ag,attrs .~ agent(ag,attrs) \Longrightarrow agent \in typeOf(ag).$
$\forall a,t_1,t_2,attrs .~ activity(a,t_1,t_2,attrs) \Longrightarrow activity \in typeOf(a).$
$\forall u,a,e,t,attrs .~ used(u; a,e,t,attrs) \Longrightarrow activity \in typeOf(a) \wedge entity \in typeOf(e).$
$\forall gen,e,a,t,attrs .~ wasGeneratedBy(gen; e,a,t,attrs) \Longrightarrow entity \in typeOf(e) \wedge activity \in typeOf(a).$
$\forall id,a_1,a_2,attrs .~ wasInformedBy(id; a_2,a_1,attrs) \Longrightarrow activity \in typeOf(a_2) \wedge activity \in typeOf(a_1).$
$\forall id,a_1,a_2,e,t,attrs .~ wasStartedBy(id; a_2,e,a_1,t,attrs) \Longrightarrow activity \in typeOf(a_2) \wedge entity \in typeOf(e) \wedge activity \in typeOf(a_1).$
$\forall id,a_1,a_2,e,t,attrs .~ wasEndedBy(id; a_2,e,a_1,t,attrs) \Longrightarrow activity \in typeOf(a_2) \wedge entity \in typeOf(e) \wedge activity \in typeOf(a_1).$
$\forall id, e,a,t,attrs .~ wasInvalidatedBy(id; e,a,t,attrs) \Longrightarrow entity \in typeOf(e) \wedge activity \in typeOf(a).$
In this constraint, $a$ , $g 2$ , and $u 1$ must not be placeholders. $\forall id, e_2, e_1, a, g2, u1, attrs .~ notNull(a) \wedge notNull(g_2) \wedge notNull(u_1) \wedge wasDerivedFrom(id; e_2, e_1, a, g2, u1, attrs) \Longrightarrow entity \in typeOf(e_2) \wedge entity \in typeOf(e_1) \wedge activity \in typeOf(a).$
$\forall id,e_1,e_2,attrs .~ wasDerivedFrom(id; e_2, e_1, -, -, -, attrs) \Longrightarrow entity \in typeOf(e_2) \wedge entity \in typeOf(e_1).$
$\forall id, e,ag,attr .~ wasAttributedTo(id; e,ag,attr) \Longrightarrow entity \in typeOf(e) \wedge agent \in typeOf(ag).$
In this constraint, $p l$ must not be a placeholder. $\forall id, a,ag,pl,attrs .~ notNull(pl) \wedge wasAssociatedWith(id; a,ag,pl,attrs) \Longrightarrow activity \in typeOf(a) \wedge agent \in typeOf(ag) \wedge entity \in typeOf(pl).$
$\forall id, a,ag,attrs .~ wasAssociatedWith(id; a,ag,-,attrs) \Longrightarrow activity \in typeOf(a) \wedge agent \in typeOf(ag).$
$\forall id, ag_2,ag_1,a,attrs .~ actedOnBehalfOf(id; ag_2,ag_1,a,attrs) \Longrightarrow agent \in typeOf(ag_2) \wedge agent \in typeOf(ag_1) \wedge activity \in typeOf(a).$
$\forall e_2, e_1 .~ alternateOf(e_2, e_1) \Longrightarrow entity \in typeOf(e_2) \wedge entity \in typeOf(e_1).$
$\forall e_2, e_1 .~ specializationOf(e_2, e_1) \Longrightarrow entity \in typeOf(e_2) \wedge entity \in typeOf(e_1).$
$\forall c,e .~ hadMember(c,e) \Longrightarrow prov:Collection \in typeOf(c) \wedge entity \in typeOf(c) \wedge entity \in typeOf(e).$
$\forall c .~ entity(c,[prov:type=prov:EmptyCollection]) \Longrightarrow entity \in typeOf(c) \wedge prov:Collection \in typeOf(c) \wedge prov:EmptyCollection \in typeOf(c).$

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

In the following rules, g and u must not be -.

$\forall id,e_1,e_2,g,attrs .~ notNull(g) \wedge wasDerivedFrom(id;e_2,e_1,-,g,-,attrs) \Longrightarrow False$
$\forall id,e_1,e_2,u,attrs .~ notNull(u) \wedge wasDerivedFrom(id;e_2,e_1,-,-,u,attrs) \Longrightarrow False$
$\forall id,e_1,e_2,g,u,attrs .~ notNull(g) \wedge notNull(u) \wedge wasDerivedFrom(id;e_2,e_1,-,g,u,attrs) \Longrightarrow False$

Constraint 52 (impossible-specialization-reflexive)

$\forall e .~ specializationOf(e,e) \Longrightarrow False$

Constraint 53 (impossible-property-overlap)

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

$\forall id,a_1,\ldots,a_m,b_1,\ldots,b_n .~ r(id; a_1,...,am) \wedge s(id; b_1,...,b_n) \Longrightarrow False$

Constraint 54 (impossible-object-property-overlap)

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

$\forall id,a_1,\ldots,a_m,b_1,\ldots,b_n.~ p(id,a_1,\ldots,a_m) \wedge r(id; b_1,\ldots,b_n) \Longrightarrow False$

Constraint 55 (entity-activity-disjoint)

$\forall id .~ entity \in typeOf(id) \wedge activity \in typeOf(id) \Longrightarrow False$

Constraint 56 (membership-empty-collection)

$\forall c,e.~hasMember(c,e) \wedge prov:EmptyCollection \in typeOf(c) \Longrightarrow False$

Automatically generated inferences

Inference 5 (communication-generation-use-inference)

$\forall id,a_2,a_1,attrs.~wasInformedBy(id,a_2,a_1,attrs) \Longrightarrow \exists e,gen,t_1,use,t_2.~wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge used(use,a_2,e,t_2,[])$

Inference 6 (generation-use-communication-inference)

$\forall gen,a_1,t_1,attrs_1,id_2,a_2,t_2,attrs_2.~wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(id_2,a_2,e,t_2,attrs_2) \Longrightarrow \exists id.~wasInformedBy(id,a_2,a_1,[])$

Inference 7 (entity-generation-invalidation-inference)

$\forall gen,e,a_1,t_1,attrs_1,id_2,a_2,t_2,attrs_2.~wasGeneratedBy(gen,e,a_1,t_1,attrs_1) \wedge used(id_2,a_2,e,t_2,attrs_2) \Longrightarrow \exists id.~wasInformedBy(id,a_2,a_1,[])$

Inference 8 (activity-start-end-inference)

$\forall a,t_1,t_2,attrs.~activity(a,t_1,t_2,attrs) \Longrightarrow \exists start,e_1,a_1,end,a_2,e_2.~wasStartedBy(start,a,e_1,a_1,t_1,[]) \wedge wasEndedBy(end,a,e_2,a_2,t_2,[])$

Inference 9 (wasStartedBy-inference)

$\forall id,a,e_1,a_1,t,attrs.~wasStartedBy(id,a,e_1,a_1,t,attrs) \Longrightarrow \exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])$

Inference 10 (wasEndedBy-inference)

$\forall id,a,e_1,a_1,t,attrs.~wasEndedBy(id,a,e_1,a_1,t,attrs) \Longrightarrow \exists gen,t_1.~wasGeneratedBy(gen,e_1,a_1,t_1,[])$

Inference 11 (derivation-generation-use-inference)

In this inference, none of $a$ , $g e n 2$ or $u s e 1$ can be placeholders - $\forall id,e_2,e_1,a,gen_2,use_1,attrs.~wasDerivedFrom(id,e_2,e_1,a,gen_2,use_1,attrs) \Longrightarrow \exists s,t_1,t_2.~used(use_1,a,e_1,t_1,[]) \wedge wasGeneratedBy(gen_2,e_2,a,t_2,[])$

Inference 12 (revision-is-alternate-inference)

In this inference, any of $a$ , $g$ or $u$ may be placeholders. $\forall id,e_1,e_2,a,g,u.~wasDerivedFrom(id,e_2,e_1,a,g,u,.(=(prov:type,prov:Revision),[])) \Longrightarrow alternateOf(e_2,e_1)$

Inference 13 (attribution-inference)

$\forall att,e,ag,attrs.~wasAttributedTo(att,e,ag,attrs) \Longrightarrow \exists a,t,gen,assoc,pl.~wasGeneratedBy(gen,e,a,t,[]) \wedge wasAssociatedWith(assoc,a,ag,pl,[])$

Inference 14 (delegation-inference)

$\forall id,ag_1,ag_2,a,attrs.~actedOnBehalfOf(id,ag_1,ag_2,a,attrs) \Longrightarrow \exists id_1,pl_1,id_2,pl_2.~wasAssociatedWith(id_1,a,ag_1,pl_1,[]) \wedge wasAssociatedWith(id_2,a,ag_2,pl_2,[])$

Inference 15 (influence-inference)

$\forall id,e,a,t,attrs.~wasGeneratedBy(id,e,a,t,attrs) \Longrightarrow wasInfluencedBy(id,e,a,attrs)$
$\forall id,a,e,t,attrs.~used(id,a,e,t,attrs) \Longrightarrow wasInfluencedBy(id,a,e,attrs)$
$\forall id,a_2,a_1,attrs.~wasInformedBy(id,a_2,a_1,attrs) \Longrightarrow wasInfluencedBy(id,a_2,a_1,attrs)$
$\forall id,a_2,e,a_1,t,attrs.~wasStartedBy(id,a_2,e,a_1,t,attrs) \Longrightarrow wasInfluencedBy(id,a_2,e,attrs)$
$\forall id,a_2,e,a_1,t,attrs.~wasEndedBy(id,a_2,e,a_1,t,attrs) \Longrightarrow wasInfluencedBy(id,a_2,e,attrs)$
$\forall id,e,a,t,attrs.~wasInvalidatedBy(id,e,a,t,attrs) \Longrightarrow wasInfluencedBy(id,e,a,attrs)$
$\forall id,e_2,e_1,a,g,u,attrs.~wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \Longrightarrow wasInfluencedBy(id,e_2,e_1,attrs)$
In this rule, $a$ , $g$ , $u$ may be placeholders -. $\forall id,e,ag,attrs.~wasAttributedTo(id,e,ag,attrs) \Longrightarrow wasInfluencedBy(id,e,ag,attrs)$
In this rule, $p l$ may be a placeholder - $\forall id,a,ag,pl,attrs.~wasAssociatedWith(id,a,ag,pl,attrs) \Longrightarrow wasInfluencedBy(id,a,ag,attrs)$
$\forall id,ag_2,ag_1,a,attrs.~actedOnBehalfOf(id,ag_2,ag_1,a,attrs) \Longrightarrow wasInfluencedBy(id,ag_2,ag_1,attrs)$

Inference 16 (alternate-reflexive)

$\forall e.~entity(e) \Longrightarrow alternateOf(e,e)$

Inference 17 (alternate-transitive)

$\forall e_1,e_2,e_3.~alternateOf(e_1,e_2) \wedge alternateOf(e_2,e_3) \Longrightarrow alternateOf(e_1,e_3)$

Inference 18 (alternate-symmetric)

$\forall e_1,e_2.~alternateOf(e_1,e_2) \Longrightarrow alternateOf(e_2,e_1)$

Inference 19 (specialization-transitive)

$\forall e_1,e_2,e_3.~specializationOf(e_1,e_2) \wedge specializationOf(e_2,e_3) \Longrightarrow specializationOf(e_1,e_3)$

Inference 20 (specialization-alternate-inference)

$\forall e_1,e_2.~specializationOf(e_1,e_2) \Longrightarrow alternateOf(e_1,e_2)$

Inference 21 (specialization-attributes-inference)

$\forall e_1,attrs,e_2.~entity(e_1,attrs) \wedge specializationOf(e_2,e_1) \Longrightarrow entity(e_2,attrs)$

@@ Line 980: / Line 980: @@
 \forall e_1,attrs,e_2.~entity(e_1,attrs) \wedge specializationOf(e_2,e_1) \Longrightarrow entity(e_2,attrs)
 </math>
-== HTML auto-generated rules ==
-=== Inference 5 (communication-generation-use-inference) ===
-&#8704; id,a_2,a_1,attrs. <span class="math">wasInformedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">attrs</span>) &#10233; &#8707; e,gen,t_1,use,t_2. <span class="math">wasGeneratedBy</span>(<span class="math">gen</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">[]</span>) &#8743; <span class="math">used</span>(<span class="math">use</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">t_2</span>,<span class="math">[]</span>)
-=== Inference 6 (generation-use-communication-inference) ===
-&#8704; gen,a_1,t_1,attrs_1,id_2,a_2,t_2,attrs_2. <span class="math">wasGeneratedBy</span>(<span class="math">gen</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">attrs_1</span>) &#8743; <span class="math">used</span>(<span class="math">id_2</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">t_2</span>,<span class="math">attrs_2</span>) &#10233; &#8707; id. <span class="math">wasInformedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">[]</span>)
-=== Inference 7 (entity-generation-invalidation-inference) ===
-&#8704; gen,e,a_1,t_1,attrs_1,id_2,a_2,t_2,attrs_2. <span class="math">wasGeneratedBy</span>(<span class="math">gen</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">attrs_1</span>) &#8743; <span class="math">used</span>(<span class="math">id_2</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">t_2</span>,<span class="math">attrs_2</span>) &#10233; &#8707; id. <span class="math">wasInformedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">[]</span>)
-=== Inference 8 (activity-start-end-inference) ===
-&#8704; a,t_1,t_2,attrs. <span class="math">activity</span>(<span class="math">a</span>,<span class="math">t_1</span>,<span class="math">t_2</span>,<span class="math">attrs</span>) &#10233; &#8707; start,e_1,a_1,end,a_2,e_2. <span class="math">wasStartedBy</span>(<span class="math">start</span>,<span class="math">a</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">[]</span>) &#8743; <span class="math">wasEndedBy</span>(<span class="math">end</span>,<span class="math">a</span>,<span class="math">e_2</span>,<span class="math">a_2</span>,<span class="math">t_2</span>,<span class="math">[]</span>)
-=== Inference 9 (wasStartedBy-inference) ===
-&#8704; id,a,e_1,a_1,t,attrs. <span class="math">wasStartedBy</span>(<span class="math">id</span>,<span class="math">a</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; &#8707; gen,t_1. <span class="math">wasGeneratedBy</span>(<span class="math">gen</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">[]</span>)
-=== Inference 10 (wasEndedBy-inference) ===
-&#8704; id,a,e_1,a_1,t,attrs. <span class="math">wasEndedBy</span>(<span class="math">id</span>,<span class="math">a</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; &#8707; gen,t_1. <span class="math">wasGeneratedBy</span>(<span class="math">gen</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">[]</span>)
-=== Inference 11 (derivation-generation-use-inference) ===
-In this inference, none of <math>a</math>, <math>gen_2</math> or <math>use_1</math> can be placeholders -&#8704; id,e_2,e_1,a,gen_2,use_1,attrs. <span class="math">wasDerivedFrom</span>(<span class="math">id</span>,<span class="math">e_2</span>,<span class="math">e_1</span>,<span class="math">a</span>,<span class="math">gen_2</span>,<span class="math">use_1</span>,<span class="math">attrs</span>) &#10233; &#8707; s,t_1,t_2. <span class="math">used</span>(<span class="math">use_1</span>,<span class="math">a</span>,<span class="math">e_1</span>,<span class="math">t_1</span>,<span class="math">[]</span>) &#8743; <span class="math">wasGeneratedBy</span>(<span class="math">gen_2</span>,<span class="math">e_2</span>,<span class="math">a</span>,<span class="math">t_2</span>,<span class="math">[]</span>)
-=== Inference 12 (revision-is-alternate-inference) ===
-In this inference, any of <math>a</math>, <math>g</math> or <math>u</math> may be placeholders.&#8704; id,e_1,e_2,a,g,u. <span class="math">wasDerivedFrom</span>(<span class="math">id</span>,<span class="math">e_2</span>,<span class="math">e_1</span>,<span class="math">a</span>,<span class="math">g</span>,<span class="math">u</span>,<span class="math">.</span>(<span class="math">=</span>(<span class="math">prov:type</span>,<span class="math">prov:Revision</span>),<span class="math">[]</span>)) &#10233; <span class="math">alternateOf</span>(<span class="math">e_2</span>,<span class="math">e_1</span>)
-=== Inference 13 (attribution-inference) ===
-&#8704; att,e,ag,attrs. <span class="math">wasAttributedTo</span>(<span class="math">att</span>,<span class="math">e</span>,<span class="math">ag</span>,<span class="math">attrs</span>) &#10233; &#8707; a,t,gen,assoc,pl. <span class="math">wasGeneratedBy</span>(<span class="math">gen</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">t</span>,<span class="math">[]</span>) &#8743; <span class="math">wasAssociatedWith</span>(<span class="math">assoc</span>,<span class="math">a</span>,<span class="math">ag</span>,<span class="math">pl</span>,<span class="math">[]</span>)
-=== Inference 14 (delegation-inference) ===
-&#8704; id,ag_1,ag_2,a,attrs. <span class="math">actedOnBehalfOf</span>(<span class="math">id</span>,<span class="math">ag_1</span>,<span class="math">ag_2</span>,<span class="math">a</span>,<span class="math">attrs</span>) &#10233; &#8707; id_1,pl_1,id_2,pl_2. <span class="math">wasAssociatedWith</span>(<span class="math">id_1</span>,<span class="math">a</span>,<span class="math">ag_1</span>,<span class="math">pl_1</span>,<span class="math">[]</span>) &#8743; <span class="math">wasAssociatedWith</span>(<span class="math">id_2</span>,<span class="math">a</span>,<span class="math">ag_2</span>,<span class="math">pl_2</span>,<span class="math">[]</span>)
-=== Inference 15 (influence-inference) ===
-<ol><li>&#8704; id,e,a,t,attrs. <span class="math">wasGeneratedBy</span>(<span class="math">id</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">attrs</span>)</li><li>&#8704; id,a,e,t,attrs. <span class="math">used</span>(<span class="math">id</span>,<span class="math">a</span>,<span class="math">e</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">a</span>,<span class="math">e</span>,<span class="math">attrs</span>)</li><li>&#8704; id,a_2,a_1,attrs. <span class="math">wasInformedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">attrs</span>)</li><li>&#8704; id,a_2,e,a_1,t,attrs. <span class="math">wasStartedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">attrs</span>)</li><li>&#8704; id,a_2,e,a_1,t,attrs. <span class="math">wasEndedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">attrs</span>)</li><li>&#8704; id,e,a,t,attrs. <span class="math">wasInvalidatedBy</span>(<span class="math">id</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">t</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">attrs</span>)</li><li>&#8704; id,e_2,e_1,a,g,u,attrs. <span class="math">wasDerivedFrom</span>(<span class="math">id</span>,<span class="math">e_2</span>,<span class="math">e_1</span>,<span class="math">a</span>,<span class="math">g</span>,<span class="math">u</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">e_2</span>,<span class="math">e_1</span>,<span class="math">attrs</span>)</li><li>In this rule, <math>a</math>, <math>g</math>, <math>u</math> may be placeholders -.&#8704; id,e,ag,attrs. <span class="math">wasAttributedTo</span>(<span class="math">id</span>,<span class="math">e</span>,<span class="math">ag</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">e</span>,<span class="math">ag</span>,<span class="math">attrs</span>)</li><li>In this rule, <math>pl</math> may be a placeholder -&#8704; id,a,ag,pl,attrs. <span class="math">wasAssociatedWith</span>(<span class="math">id</span>,<span class="math">a</span>,<span class="math">ag</span>,<span class="math">pl</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">a</span>,<span class="math">ag</span>,<span class="math">attrs</span>)</li><li>&#8704; id,ag_2,ag_1,a,attrs. <span class="math">actedOnBehalfOf</span>(<span class="math">id</span>,<span class="math">ag_2</span>,<span class="math">ag_1</span>,<span class="math">a</span>,<span class="math">attrs</span>) &#10233; <span class="math">wasInfluencedBy</span>(<span class="math">id</span>,<span class="math">ag_2</span>,<span class="math">ag_1</span>,<span class="math">attrs</span>)</li></ol>
-=== Inference 16 (alternate-reflexive) ===
-&#8704; e. <span class="math">entity</span>(<span class="math">e</span>) &#10233; <span class="math">alternateOf</span>(<span class="math">e</span>,<span class="math">e</span>)
-=== Inference 17 (alternate-transitive) ===
-&#8704; e_1,e_2,e_3. <span class="math">alternateOf</span>(<span class="math">e_1</span>,<span class="math">e_2</span>) &#8743; <span class="math">alternateOf</span>(<span class="math">e_2</span>,<span class="math">e_3</span>) &#10233; <span class="math">alternateOf</span>(<span class="math">e_1</span>,<span class="math">e_3</span>)
-=== Inference 18 (alternate-symmetric) ===
-&#8704; e_1,e_2. <span class="math">alternateOf</span>(<span class="math">e_1</span>,<span class="math">e_2</span>) &#10233; <span class="math">alternateOf</span>(<span class="math">e_2</span>,<span class="math">e_1</span>)
-=== Inference 19 (specialization-transitive) ===
-&#8704; e_1,e_2,e_3. <span class="math">specializationOf</span>(<span class="math">e_1</span>,<span class="math">e_2</span>) &#8743; <span class="math">specializationOf</span>(<span class="math">e_2</span>,<span class="math">e_3</span>) &#10233; <span class="math">specializationOf</span>(<span class="math">e_1</span>,<span class="math">e_3</span>)
-=== Inference 20 (specialization-alternate-inference) ===
-&#8704; e_1,e_2. <span class="math">specializationOf</span>(<span class="math">e_1</span>,<span class="math">e_2</span>) &#10233; <span class="math">alternateOf</span>(<span class="math">e_1</span>,<span class="math">e_2</span>)
-=== Inference 21 (specialization-attributes-inference) ===
-&#8704; e_1,attrs,e_2. <span class="math">entity</span>(<span class="math">e_1</span>,<span class="math">attrs</span>) &#8743; <span class="math">specializationOf</span>(<span class="math">e_2</span>,<span class="math">e_1</span>) &#10233; <span class="math">entity</span>(<span class="math">e_2</span>,<span class="math">attrs</span>)

FormalSemanticsCR

From Provenance WG Wiki

Revision as of 13:57, 9 January 2013

Contents

Overview

Status

Idea of the semantics

Axiomatization and relationship to PROV-CONSTRAINTS

Basics

Identifiers

Times and Intervals

Attributes and Values

Formulas

World Models

Things

Objects

Entities

Plans

Agents

Actvities

Interactions

Events

Associations

Derivations

Relations

Simple relations

Derivation paths and DerivedFrom

Putting it all together

Semantics

Interpretations

Satisfaction

Attribute matching

Semantics of Element Records

Entity Records

Activity Records

Agent Records

Semantics of Relations

Entity-Activity

Generation

Use

Invalidation

Agent-Activity

Association Records

Start Records

End Records

Agent-Entity

Attribution Records

Agent-Agent

Responsibility

Entity-Entity

Derivation

Precise

Imprecise

Specialization

Alternate

Axiomatization

Definitional Rules

Definition 1 (optional-identifiers)

Definition 2 (optional-attributes)

Definition 3 (definition-short-forms)

Definition 4 (optional-placeholders)

Inference Rules

Inference 5 (communication-generation-use-inference)

Inference 6 (generation-use-communication-inference)

Inference 7 (entity-generation-invalidation-inference)

Inference 8 (activity-start-end-inference)

Inference 9 (wasStartedBy-inference)

Inference 10 (wasEndedBy-inference)

Inference 11 (derivation-generation-use-inference)

Inference 12 (revision-is-alternate-inference)

Inference 13 (attribution-inference)

Inference 14 (delegation-inference)

Inference 15 (influence-inference)

Inference 16 (alternate-reflexive)

Inference 17 (alternate-transitive)

Inference 18 (alternate-symmetric)

Inference 19 (specialization-transitive)

Inference 20 (specialization-alternate-inference)

Inference 21 (specialization-attributes-inference)

Constraints