In this section we give a translation from valid PROV instances to
structures, and show that a valid PROV instance has a model. We
call this property weak completeness.
First, without loss of generality, we assume that all times
specified in activity or event formulas in are ground values.
If not, set each variable in such a position to some dummy value.
This is justified by the following fact:
The sets of structure are:
In the definitions of , , and
we use the notation to indicate
that must have type in according to the typing
constraints. For example, for entities, this means that the set
contains all identifiers appearing in the ,
, or formulas, as well as all tose
appearing in the appropriate positions of other formulas, as
specified in the typing constraints.
In the definitions of , , , and we
write , , and respectively to indicate
additional activities, generations and usages added for imprecise
derivations or entities.
In addition, to define the set of , we introduce an
equivalence relation on as follows:
The fact that this is an equivalence relation follows from the
fact that is in normal form, since the constraints on
ensure that it is an equivalence relation. Recall
that given an equivalence relation on some set , the
equivalence class of is the set . The quotient of by an equivalence
relation on is the set of equivalence classes, . Now we
define the set of as the quotient of -equivalence classes of .
Observe that since is normalized and valid, entities and
activities are disjoint, the influences are disjoint from entities,
activities, and agents,
and the different subsets of events and influences are pairwise
disjoint, as required.
First, we consider the functions associated with .
Above, we introduce a fresh attribute name , not already in
use in , along with a fresh value and for each entity we
add a value to . This
construction ensures that if an entity is a specialization of another
in then the specialization relationship will hold in . We
also define the set of all events involved in as the set of events
immediately involved in or any specialization of . Similarly,
the values of attributes of are those immediately declared for
along with those of any that specializes. We also introduce dummy
generation and invalidation events for each entity , along with
activities to perform them.
Similarly, for , we
employ an auxiliary function that collects the set of all
events in which one of the entities constituting the thing participated.
The functions , and mapping activities to
their start and end times are defined as follows:
The start and end times are arbitrary (say, some zero value) for activities with no
formula declaring the times. The above definitions of and
ignore any start times asserted in or
formulas. If both and
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
For other besides and , the
associated sets of are defined to be empty. (An that
happens to be an or will have the set of events
defined above for the appropriate kind of object. Note that since
and are disjoint, this definition is unambiguous.)
The function mapping to their is defined
This definition is deterministic because the sets of identifiers
of different are disjoint, and the associated times are unique.
The functions giving the interpretations of the
different identified influences are as follows:
Note that since 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 to .
The definition of the function is more involved, and
is as follows:
This definition ensures that by construction
contains all of the other associated relationships. For any specific
, however, most of the above sets will be empty, and the final
line will often be redundant. It is not always redundant, because it
is possible to assert an unspecified influence in .
It is straightforward to verify (by their definitions) that the
event sets associated with entities and activities satisfy the
side-conditions in Component 9.
Finally, the collection membership function is
defined as follows: