--- a/semantics/checker.pl Wed Jan 30 16:23:59 2013 -0700
+++ b/semantics/checker.pl Thu Jan 31 00:18:53 2013 +0000
@@ -1,28 +1,186 @@
% Some horrible Prolog code for PROV-CONSTRAINTS
remove(X,[Y|J],J) :- X == Y,!.
-remove(X,[Y|J],K) :- X \== Y, remove(X,J,K).
+remove(X,[Y|J],[Y|K]) :- X \== Y, remove(X,J,K).
multimember(A,B,[A|L]) :- member(B,L).
multimember(A,B,[_|L]) :- multimember(A,B,L).
-ensure(T,T1,T2) :- \+(member(T,T1)), T2 = [T|T1].
+ensure(A,I,J) :- \+(member(A,I)), J = [A|I].
% inference 5
infer(I,J) :- member(wasInformedBy(_Id,A2,A1,_Attrs),I),
- \+((member(wasGeneratedBy(Gen,E,A1,_T1,_),I),
- member(used(Use,A2,E,_T2,_),I))),
+ \+((member(wasGeneratedBy(Gen,E,A1,_,_),I),
+ member(used(Use,A2,E,_,_),I))),
J = [wasGeneratedBy(Gen,E,A1,_T1,[]),
used(Use,A2,E,_T2,[])|I].
% inference 6
-infer(I,J) :- member(wasGeneratedBy(_Gen,E,A1,_T1,_Attrs1),I),
- member(used(_Use,A2,E,_T2,_Attrs2),I),
- \+(member(wasInformedBy(_Id,A2,A1,_),I)),
+infer(I,J) :- member(wasGeneratedBy(_Gen,E1,A1,_T1,_Attrs1),I),
+ member(used(_Use,A2,E2,_T2,_Attrs2),I),
+ E1 == E2,
+ \+(member(wasInformedBy(_,A2,A1,_),I)),
J = [wasInformedBy(_Id,A2,A1,[])|I].
+% inference 7a
+infer(I,J) :- member(entity(E,_Attrs),I),
+ \+(member(wasGeneratedBy(_,E,_,_,_),I)),
+ J = [wasGeneratedBy(_,E,_,_,[])|I].
+% inference 7b
+infer(I,J) :- member(entity(E,_Attrs),I),
+ \+(member(wasInvalidatedBy(_,E,_,_,_),I)),
+ J = [wasInvalidatedBy(_,E,_,_,[])|I].
+
+% inference 8a
+infer(I,J) :- member(activity(A,T1,_T2,_Attrs),I),
+ \+(member(wasStartedBy(_,A,_,_,T1,_),I)),
+ J = [wasStartedBy(_,A,_,_,T1,_)|I].
+% inference 8b
+infer(I,J) :- member(activity(A,_T1,T2,_Attrs),I),
+ \+(member(wasEndedBy(_,A,_,_,T2,_),I)),
+ J = [wasEndedBy(_,A,_,_,T2,[])|I].
+
+% inference 9
+infer(I,J) :- member(wasStartedBy(_ID,_A,E1,A1,_T,_Attrs),I),
+ \+(member(wasGeneratedBy(_,E1,A1,_,_),I)),
+ J = [wasGeneratedBy(_,E1,A1,_,[])|I].
+
+% inference 10
+infer(I,J) :- member(wasEndedBy(_ID,_A,E1,A1,_T,_Attrs),I),
+ \+(member(wasGeneratedBy(_,E1,A1,_,_),I)),
+ J = [wasGeneratedBy(_,E1,A1,_,[])|I].
+
+% inference 11a
+infer(I,J) :- member(wasDerivedFrom(_ID,E1,_E2,A,Gen2,Use1,_Attrs),I),
+ A \== null, Gen2 \== null, Use1 \== null,
+ \+(member(used(Use1,A,E1,_,_),I)),
+ J = [used(Use1,A,E1,_,[])|I].
+% inference 11b
+infer(I,J) :- member(wasDerivedFrom(_ID,_E1,E2,A,Gen2,Use1,_Attrs),I),
+ A \== null, Gen2 \== null, Use1 \== null,
+ \+(member(wasGeneratedBy(Gen2,E2,A,_,_),I)),
+ J = [wasGeneratedBy(Gen2,E2,A,_,[])|I].
+
+% inference 12
+infer(I,J) :- member(wasDerivedFrom(_ID,E2,E1,_A,_G,_U,Attrs),I),
+ member('prov:type'='prov:Revision', Attrs),
+ \+(member(alternateOf(E2,E1),I)),
+ J = [alternateOf(E2,E1)|I].
+
+% inference 13
+infer(I,J) :- member(wasAttributedTo(_ID,E,Ag,_Attrs),I),
+ \+((member(wasGeneratedBy(_,E,A,_,_),I),
+ member(wasAssociatedWith(_,A,Ag,_,_),I))),
+ J = [wasGeneratedBy(_,E,A,_,[]),
+ wasAssociatedWith(_,A,Ag,_,_)|I].
+
+% inference 14a
+infer(I,J) :- member(actedOnBehalfOf(_ID,Ag1,_Ag2,A,_Attrs),I),
+ \+(member(wasAssociatedWith(_,A,Ag1,_,_),I)),
+ J = [wasAssociatedWith(_,A,Ag1,_,[])|I].
+
+% inference 14b
+infer(I,J) :- member(actedOnBehalfOf(_ID,_Ag1,Ag2,A,_Attrs),I),
+ \+(member(wasAssociatedWith(_,A,Ag2,_,_),I)),
+ J = [wasAssociatedWith(_,A,Ag2,_,[])|I].
+
+% inference 15.1
+infer(I,J) :- member(wasGeneratedBy(Id,E,A,_T,Attrs),I),
+ \+(member(wasInfluencedBy(Id,E,A,_),I)),
+ J = [wasInfluencedBy(Id,E,A,Attrs)|I].
+% Tricky because of attribute inheritance
+% Add if no previous influence
+% Should merge if there is already an influence, but this is tricky to
+% handle without diverging
+
+% inference 15.2
+infer(I,J) :- member(used(Id,A,E,_T,Attrs),I),
+ \+(member(wasInfluencedBy(Id,A,E,_),I)),
+ J = [wasInfluencedBy(Id,A,E,Attrs)|I].
+
+% inference 15.3
+infer(I,J) :- member(wasInformedBy(Id,Y,X,_T,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 15.4
+infer(I,J) :- member(wasStartedBy(Id,Y,X,_,_T,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 15.5
+infer(I,J) :- member(wasEndedBy(Id,Y,X,_,_T,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 15.6
+infer(I,J) :- member(wasInvalidatedBy(Id,E,A,_T,Attrs),I),
+ \+(member(wasInfluencedBy(Id,E,A,_),I)),
+ J = [wasInfluencedBy(Id,E,A,Attrs)|I].
+
+% inference 15.7
+infer(I,J) :- member(wasDerivedFrom(Id,Y,X,_A,_G,_U,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 15.8
+infer(I,J) :- member(wasAttributedTo(Id,Y,X,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 15.9
+infer(I,J) :- member(wasAssociatedWith(Id,Y,X,_Pl,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 15.9
+infer(I,J) :- member(actedOnBehalfOf(Id,Y,X,_A,Attrs),I),
+ \+(member(wasInfluencedBy(Id,Y,X,_),I)),
+ J = [wasInfluencedBy(Id,Y,X,Attrs)|I].
+
+% inference 16
+
+infer(I,J) :- member(entity(E,_Attrs),I),
+ \+(member(alternateOf(E,E),I)),
+ J = [alternateOf(E,E)|I].
+
+% inference 17
+% careful about unification
+infer(I,J) :- member(alternateOf(E1,E21),I),
+ member(alternateOf(E22,E3),I),
+ E21==E22,
+ \+(member(alternateOf(E1,E3),I)),
+ J = [alternateOf(E1,E3)|I].
+
+% inference 18
+infer(I,J) :- member(alternateOf(E1,E2),I),
+ \+(member(alternateOf(E2,E1),I)),
+ J = [alternateOf(E2,E1)|I].
+
+% inference 19
+% careful about unification
+infer(I,J) :- member(specializationOf(E1,E21),I),
+ member(specializationOf(E22,E3),I),
+ E21==E22,
+ \+(member(specializationOf(E1,E3),I)),
+ J = [specializationOf(E1,E3)|I].
+
+% inference 20
+infer(I,J) :- member(specializationOf(E1,E2),I),
+ \+(member(alternateOf(E1,E2),I)),
+ J = [alternateOf(E1,E2)|I].
+
+% inference 21
+infer(I,J) :- member(entity(E,Attrs),I),
+ member(specializationOf(E2,E1),I),
+ E1 == E,
+ \+(member(entity(E2,Attrs),I)),
+ J = [entity(E2,Attrs)|I].
+
+
+
% Constraint 22.1: key constraint: entity
infer(I,J) :- multimember(entity(ID1,Attrs1),
entity(ID2,Attrs2),I),
@@ -55,7 +213,7 @@
append(Attrs1,Attrs2,Attrs),
J = [agent(ID1,Attrs)|J2].
-% Constraint 23.1: key constraint: used
+% Constraint 23.1:
infer(I,J) :- multimember(wasGeneratedBy(ID1,E1,A1,T1,Attrs1),
wasGeneratedBy(ID2,E2,A2,T2,Attrs2),I),
ID1 == ID2, % If keys are equal terms
@@ -63,12 +221,12 @@
((A1 = A2, E1 = E2, T1 = T2)
-> (
remove(wasGeneratedBy(ID1,E1,A1,T1,Attrs1),I,J1), % and merge
- remove( wasGeneratedBy(ID2,E2,A2,T2,Attrs2),J1,J2),
+ remove(wasGeneratedBy(ID2,E2,A2,T2,Attrs2),J1,J2),
append(Attrs1,Attrs2,Attrs),
J = [wasGeneratedBy(ID1,E1,A1,T1,Attrs)|J2])
; J = invalid).
-% Constraint 23.2: key constraint: used
+% Constraint 23.2:
infer(I,J) :- multimember(used(ID1,A1,E1,T1,Attrs1),
used(ID2,A2,E2,T2,Attrs2),I),
ID1 == ID2, % If keys are equal terms
@@ -81,21 +239,186 @@
J = [used(ID1,A1,E1,T1,Attrs)|J2])
; J = invalid).
+% Constraint 23.3:
+infer(I,J) :- multimember(wasInformedBy(ID1,A12,A11,Attrs1),
+ wasInformedBy(ID2,A22,A21,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((A12 = A22, A11=A21)
+ -> (
+ remove(wasInformedBy(ID1,A12,A11,Attrs1),I,J1), % and merge
+ remove(wasInformedBy(ID2,A22,A21,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasInformedBy(ID1,A12,A11,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.4:
+infer(I,J) :- multimember(wasStartedBy(ID1,A12,E1,A11,T1,Attrs1),
+ wasStartedBy(ID2,A22,E2,A21,T2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((A12 = A22, A11=A21,E1=E2,T1=T2)
+ -> (
+ remove(wasStartedBy(ID1,A12,E1,A11,T1,Attrs1),I,J1), % and merge
+ remove(wasStartedBy(ID2,A22,E2,A21,T2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasStartedBy(ID1,A12,E1,A11,T1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.5:
+infer(I,J) :- multimember(wasEndedBy(ID1,A12,E1,A11,T1,Attrs1),
+ wasEndedBy(ID2,A22,E2,A21,T2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((A12 = A22, A11=A21,E1=E2,T1=T2)
+ -> (
+ remove(wasEndedBy(ID1,A12,E1,A11,T1,Attrs1),I,J1), % and merge
+ remove(wasEndedBy(ID2,A22,E2,A21,T2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasEndedBy(ID1,A12,E1,A11,T1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.6:
+infer(I,J) :- multimember(wasInvalidatedBy(ID1,E1,A1,T1,Attrs1),
+ wasInvalidatedBy(ID2,E2,A2,T2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((A1 = A2, E1 = E2, T1 = T2)
+ -> (
+ remove(wasInvalidatedBy(ID1,E1,A1,T1,Attrs1),I,J1), % and merge
+ remove(wasInvalidatedBy(ID2,E2,A2,T2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasInvalidatedBy(ID1,E1,A1,T1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.7:
+infer(I,J) :- multimember(wasDerivedFrom(ID1,E12,E11,A1,G1,U1,Attrs1),
+ wasDerivedFrom(ID2,E22,E21,A2,G2,U2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((E12=E22,E11=E21,A1 = A2, G1=G2, U1=U2)
+ -> (
+ remove(wasDerivedFrom(ID1,E12,E11,A1,G1,U1,Attrs1),I,J1), % and merge
+ remove(wasDerivedFrom(ID2,E22,E21,A2,G2,U2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasDerivedFrom(ID1,E12,E11,A1,G1,U1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.8:
+infer(I,J) :- multimember(wasAttributedTo(ID1,E1,Ag1,Attrs1),
+ wasAttributedTo(ID2,E2,Ag2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((E1=E2,Ag1=Ag2)
+ -> (
+ remove(wasAttributedTo(ID1,E1,Ag1,Attrs1),I,J1), % and merge
+ remove(wasAttributedTo(ID2,E2,Ag2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasAttributedTo(ID1,E1,Ag1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.9:
+infer(I,J) :- multimember(wasAssociatedWith(ID1,A1,Ag1,Pl1,Attrs1),
+ wasAssociatedWith(ID2,A2,Ag2,Pl2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((A1=A2,Ag1=Ag2,Pl1=Pl2)
+ -> (
+ remove(wasAssociatedWith(ID1,A1,Ag1,Pl1,Attrs1),I,J1), % and merge
+ remove(wasAssociatedWith(ID2,A2,Ag2,Pl2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasAssociatedWith(ID1,A1,Ag1,Pl1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.10:
+infer(I,J) :- multimember(actedOnBehalfOf(ID1,Ag12,Ag11,A1,Attrs1),
+ actedOnBehalfOf(ID2,Ag22,Ag21,A2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((Ag12=Ag22,Ag11=Ag21,A1=A2)
+ -> (
+ remove(actedOnBehalfOf(ID1,Ag12,Ag11,A1,Attrs1),I,J1), % and merge
+ remove(actedOnBehalfOf(ID2,Ag22,Ag21,A2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [actedOnBehalfOf(ID1,Ag12,Ag11,A1,Attrs)|J2])
+ ; J = invalid).
+
+% Constraint 23.11:
+infer(I,J) :- multimember(wasInfluencedBy(ID1,Y1,X1,Attrs1),
+ wasInfluencedBy(ID2,Y2,X2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((X1=X2,Y1=Y2)
+ -> (
+ remove(wasInfluencedBy(ID1,Y1,X1,Attrs1),I,J1), % and merge
+ remove(wasInfluencedBy(ID2,Y2,X2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [wasInfluencedBy(ID1,Y1,X1,Attrs)|J2])
+ ; J = invalid).
+
+
+
+
% Constraint 24: unique-generation
infer(I,J) :- multimember(wasGeneratedBy(Gen1,E1,A1,_T1,_Attrs1),
wasGeneratedBy(Gen2,E2,A2,_T2,_Attrs2),I),
E1 == E2, % If entity and activity are equal terms
A1 == A2,
- Gen1 \== Gen2, % to avoid nontermination if we already got this pair
((Gen1 = Gen2)
-> (J = I) % And the ids unify, then done. Key constraint will do the rest.
; J = invalid). % Otherwise invalid.
-% todo: duplicate elimination
+% Constraint 25: unique-invalidation
+infer(I,J) :- multimember(wasInvalidatedBy(Inv1,E1,A1,_T1,_Attrs1),
+ wasInvalidatedBy(Inv2,E2,A2,_T2,_Attrs2),I),
+ E1 == E2, % If entity and activity are equal terms
+ A1 == A2,
+ ((Inv1 = Inv2)
+ -> (J = I) % And the ids unify, then done. Key constraint will do the rest.
+ ; J = invalid). % Otherwise invalid.
+
+
+% Constraint 26: unique-wasStartedBy
+infer(I,J) :- multimember(wasStartedBy(ID1,A1,_E1,A11,_T1,_Attrs1),
+ wasStartedBy(ID2,A2,_E2,A12,_T2,_Attrs2),I),
+ A1 == A2, % If entity and activity are equal terms
+ A11 == A12,
+ ((ID1 = ID2)
+ -> (J = I) % And the ids unify, then done. Key constraint will do the rest.
+ ; J = invalid). % Otherwise invalid.
+
+% Constraint 27: unique-wasEndedBy
+infer(I,J) :- multimember(wasEndedBy(ID1,A1,_E1,A11,_T1,_Attrs1),
+ wasEndedBy(ID2,A2,_E2,A12,_T2,_Attrs2),I),
+ A1 == A2, % If entity and activity are equal terms
+ A11 == A12,
+ ((ID1 = ID2)
+ -> (J = I) % And the ids unify, then done. Key constraint will do the rest.
+ ; J = invalid). % Otherwise invalid.
+
+% Constraint 28: unique-startTime
+infer(I,J) :- member(activity(A,T1,_T2,_Attrs),I),
+ member(wasStartedBy(_Start,A2,_E,_A1,T,_Attrs2),I),
+ A==A2,
+ T1 \== T,
+ ((T1=T)
+ -> (J = I)
+ ; J = invalid).
+
+% Constraint 29: unique-endTime
+infer(I,J) :- member(activity(A,_T1,T2,_Attrs),I),
+ member(wasEndedBy(_End,A2,_E,_A1,T,_Attrs2),I),
+ A==A2,
+ T2 \== T,
+ ((T2=T)
+ -> (J = I)
+ ; J = invalid).
normalize(I,I) :- \+(infer(I,_)), !.
normalize(I,K) :- infer(I,J), !, normalize(J,K).
+
+
% Constraint 30
ordering_step(I,O1,O2) :-
member(wasStartedBy(Start,A,_E1,_A1,_T1,_Attrs1),I),
@@ -108,7 +431,7 @@
ordering_saturate(I,O,O) :- \+(ordering_step(I,O,_)),!.
ordering_saturate(I,O1,O3) :-
ordering_step(I,O1,O2),
- saturate_ordering(I,O2,O3).
+ ordering_saturate(I,O2,O3).
strict_cycle(_O) :- fail. % TODO: Search graph for cycles containing a strict edge. Prolog 101.
@@ -158,14 +481,14 @@
% Constraint 50.10.
typing_step(I) -->
- {member(wasDerivedFrom(_id,E2,E1,A,Gen,Use,_Attrs),I),
+ {member(wasDerivedFrom(_Id,E2,E1,A,Gen,Use,_Attrs),I),
A == null, Gen == null, Use == null},
(ensure(typeOf(E1,entity)) ;
ensure(typeOf(E2,entity)) ).
% Constraint 50.11.
typing_step(I) -->
- {member(wasDerivedFrom(_id,E2,E1,A,Gen,Use,_Attrs),I),
+ {member(wasDerivedFrom(_Id,E2,E1,A,Gen,Use,_Attrs),I),
A \== null, Gen \== null, Use \== null},
(ensure(typeOf(E1,entity)) ;
ensure(typeOf(E2,entity)) ;
@@ -175,7 +498,7 @@
% Constraint 50.13.
typing_step(I) -->
- {member(wasAssociatedWith(_id,A,Ag,Pl,_Attrs),I),
+ {member(wasAssociatedWith(_Id,A,Ag,Pl,_Attrs),I),
Pl \== null},
(ensure(typeOf(A,activity)) ;
ensure(typeOf(Ag,agent)) ;
@@ -183,7 +506,7 @@
% Constraint 50.14.
typing_step(I) -->
- {member(wasAssociatedWith(_id,A,Ag,Pl,_Attrs),I),
+ {member(wasAssociatedWith(_Id,A,Ag,Pl,_Attrs),I),
Pl == null},
(ensure(typeOf(A,activity)) ;
ensure(typeOf(Ag,agent)) ).
@@ -199,7 +522,7 @@
% Impossibility constraints
-%Some background info
+% Some background info
object(entity).
object(activity).
object(agent).
@@ -223,7 +546,7 @@
-%Constraint 52. Have to be careful not to unify.
+% Constraint 52. Have to be careful not to unify.
impos(I,_T) :- member(specializationOf(E1,E2),I), E1 == E2.
% Constraint 53.
@@ -261,4 +584,4 @@
valid(I) :- normalize(I,J),
ordering_check(J),
typing(J,T),
- impos_check(J,T).
\ No newline at end of file
+ impos_check(J,T).
--- a/semantics/prov-sem.html Wed Jan 30 16:23:59 2013 -0700
+++ b/semantics/prov-sem.html Thu Jan 31 00:18:53 2013 +0000
@@ -70,7 +70,7 @@
background: #fff;
}
-.formal {
+.formalism {
padding: 1em;
margin: 1em 0em 0em;
border: 1px solid #0f0;
@@ -571,7 +571,7 @@
function updateRules() {
var count=1;
- $('.constraint,.definition,.inference,.formal').each(function(index) {
+ $('.constraint,.definition,.inference,.formalism').each(function(index) {
var myid=$(this).attr('id');
var mycount=$(this).attr('number');
@@ -1193,7 +1193,7 @@
<p>An <em>Event</em> 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:
</p>
-<div class="formal">
+<div class="formalism">
<ul><li> A set $Events \subseteq Interactions$ of events.
</li><li> A function $time : Events \to Times$ giving the time of each event; i.e. $lifetime(evt) = \{time(t)\}$.
</li><li> The derived ordering on events given by $evt_1 \leq evt_2 \iff time(evt_1) \leq time(evt_2)$
@@ -1204,7 +1204,7 @@
<p>An <em>Association</em> 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:
</p>
-<div class="formal">
+<div class="formalism">
<p>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$
</p>
</div>
@@ -1216,7 +1216,7 @@
<p>A <em>Derivation</em> 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.
</p>
-<div class="formal">
+<div class="formalism">
<p> * A set $Derivations \subseteq Interactions$, disjoint from $Events \cup Associations$.
</p></div>
<p>See below for the associated derivation path and DerivedFrom relation.
@@ -1282,7 +1282,7 @@
</p>
<p>The mapping from identifiers to objects may <b>not</b> change over time. Thus, we consider interpretations as follows:
</p>
-<div class="formal"> An interpretation function $I : Identifiers \to Objects$ describing which object is the target of each identifier.
+<div class="formalism"> An interpretation function $I : Identifiers \to Objects$ describing which object is the target of each identifier.
</div>
<h3> Satisfaction </h3>
@@ -1308,7 +1308,7 @@
</p>
<p>Entity assertions $entity(id,attrs)$ can be interpreted as follows:
</p>
-<div class="formal">
+<div class="formalism">
$W,I \models entity(id,attrs)$ if and only if:
<ol>
<li>[WF] $id$ denotes an entity $ent = I(id) \in Entities$
@@ -1328,7 +1328,7 @@
<p>An activity record is of the form $activity(id,st,et,attrs)$ where $id$ is a identifier referring to the activity, $st$ is a start time and $et$ is an end time.
</p>
-<div class="formal">
+<div class="formalism">
<p>We say that $W,I \models activity(id,st,et,attrs)$ if and only if:</p>
<ol>
<li>[WF] The identifier $id$ maps to an activity $act = I(id) \in Activities$
@@ -1346,7 +1346,7 @@
<p>An agent formula is of the form $agent(id,attrs)$ where $id$ denotes the agent and $attrs$ describes additional attributes.
</p>
-<div class="formal">
+<div class="formalism">
<p>Agent assertions $agent(id,attrs)$ can be interpreted as follows:
$W,I \models agent(id,attrs)$ if and only if:
</p>
@@ -1366,7 +1366,7 @@
<p>The generation assertion is of the form $wasGeneratedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
</p>
-<div class="formal">
+<div class="formalism">
$W,I \models wasGeneratedBy(id,e,a,t,attrs)$ if and only if:
<ol>
<li>[WF] The identifier $id$ denotes an event $evt = I(id) \in Events$
@@ -1392,7 +1392,7 @@
The use assertion is of the form $used(id,a,e,t,attrs)$ where $id$ denotes an event, $a$ is an activity identifier, $e$ is an object identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
-<div class="formal"> $W,I \models used(id,a,e,t,attrs)$ if and only if:
+<div class="formalism"> $W,I \models used(id,a,e,t,attrs)$ if and only if:
</li>
<li>[WF] The identifier $id$ denotes an event $evt = I(id) \in Events$
</li>
@@ -1415,7 +1415,7 @@
The invalidation assertion is of the form $wasInvalidatedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is an optional time.
-<div class="formal"> $W,I \models wasInvalidatedBy(id,e,a,t,attrs)$ if and only if:
+<div class="formalism"> $W,I \models wasInvalidatedBy(id,e,a,t,attrs)$ if and only if:
<ol>
<li>[WF] The identifier $id$ denotes an event $evt = I(id) \in Events$
</li>
@@ -1439,7 +1439,7 @@
An association record has the form $wasAssociatedWith(id,a,ag,pl,attrs)$.
-<div class="formal"> $W,I \models wasAssociatedWith(id,a,ag,pl,attrs)$ holds if and only if:
+<div class="formalism"> $W,I \models wasAssociatedWith(id,a,ag,pl,attrs)$ holds if and only if:
<ol>
<li>[WF] $assoc$ denotes an association $assoc = I(id) \in Associations$.
</li>
@@ -1458,7 +1458,7 @@
A start record $wasStartedBy(id,a2,e,a1,attrs)$ is interpreted as follows:
-<div class="formal"> $W,I \models wasStartedBy(id,a2,e,a1,attrs)$ holds if and only if:
+<div class="formalism"> $W,I \models wasStartedBy(id,a2,e,a1,attrs)$ holds if and only if:
<ol>
<li>[WF] $id$ denotes an event $evt = I(id) \in Events$
</li>
@@ -1481,7 +1481,7 @@
An activity end record $wasEndedBy(id,a2,e,a1,attrs)$ is interpreted as follows:
-<div class="formal">
+<div class="formalism">
$W,I \models wasEndedBy(id,a2,e,a1,attrs)$ holds if and only if:
<ol>
<li>[WF] $id$ denotes an event $evt = I(id) \in Events$</li>
@@ -1500,7 +1500,7 @@
An attribution record $wasAttributedTo(id,e,ag,attrs)$ is interpreted as follows:
-<div class="formal"> $W,I \models wasAttributedTo(id,e,ag,attrs)$ holds if and only if:
+<div class="formalism"> $W,I \models wasAttributedTo(id,e,ag,attrs)$ holds if and only if:
<ol>
<li>[WF] $id$ denotes an event $evt = I(id)$ that is also an association $evt \in Associations$
</li>
@@ -1521,7 +1521,7 @@
The $actedOnBehalfOf(id,ag2,ag1,act,attrs)$ relation is interpreted using the $ActsFor$ relation as follows:
-<div class="formal"> $W,I \models actedOnBehalfOf(id,ag2,ag1,act,attrs)$ holds if and only if:
+<div class="formalism"> $W,I \models actedOnBehalfOf(id,ag2,ag1,act,attrs)$ holds if and only if:
<ol>
<li>[WF] $id$ denotes an association $assoc=I(id) \in Associations$ that is an association interaction, and $type(id) = responsibility$.
</li>
@@ -1544,7 +1544,7 @@
<p>A precise derivation record has the form $wasDerivedFrom(id,e2,e1,a,g,u,attrs)$.
</p>
-<div class="formal"> $W,I \models wasDerivedFrom(id,e2,e1,act,g,u,attrs)$ if and only if:
+<div class="formalism"> $W,I \models wasDerivedFrom(id,e2,e1,act,g,u,attrs)$ if and only if:
<ol>
<li>[WF] $id$ denotes a derivation $deriv = I(id) \in Derivations$
</li>
@@ -1566,7 +1566,7 @@
<p>
An imprecise derivation record has the form $wasDerivedFrom(id,e2,e1,-,-,-,attrs)$.</p>
-<div class="formal"> $W,I \models wasDerivedFrom(id,e2,e1,-,-,-,attrs)$ if and only if there exists $path \in DerivationPaths$ such that:
+<div class="formalism"> $W,I \models wasDerivedFrom(id,e2,e1,-,-,-,attrs)$ if and only if there exists $path \in DerivationPaths$ such that:
<ol>
<li>[WF] $id$ denotes a derivation $deriv = I(id) \in Derivations$
</li>
@@ -1582,7 +1582,7 @@
<p>The $specializationOf(e1,e2)$ relation indicates when one entity record presents more specific aspects of another.
</p>
-<div class="formal"> $W,I \models specializationOf(e1,e2)$ if and only if:
+<div class="formalism"> $W,I \models specializationOf(e1,e2)$ if and only if:
<ol>
<li>[WF] Both $e1$ and $e2$ are entity identifiers, denoting $ent_1 = I(e1) \in Entities$ and $ent_2 = I(e2) \in Entities$.
</li>
@@ -1612,7 +1612,7 @@
<p>The $alternateOf$ relation indicates when two entity records present (possibly different) aspects of the same thing. The two entities may or may not overlap in time.
</p>
-<div class="formal"> $W,I \models alternateOf(e1,e2)$ if and only if:
+<div class="formalism"> $W,I \models alternateOf(e1,e2)$ if and only if:
<ol>
<li>[WF] Both $e1$ and $e2$ are entity identifiers, denoting $ent_1 = I(e1)$ and $ent_2 = I(e2)$.
</li>