--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/semantics/checker.pl Thu Jan 24 18:37:55 2013 +0000
@@ -0,0 +1,266 @@
+% 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).
+
+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].
+
+
+
+% 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))),
+ 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)),
+ J = [wasInformedBy(_Id,A2,A1,[])|I].
+
+% Constraint 22.1: key constraint: entity
+infer(I,J) :- multimember(entity(ID1,Attrs1),
+ entity(ID2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ remove(entity(ID1,Attrs1),I,J1), % and merge
+ remove(entity(ID2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [entity(ID1,Attrs)|J2].
+
+% Constraint 22.2: key constraint: activity
+infer(I,J) :- multimember(activity(ID1,ST1,ET1,Attrs1),
+ activity(ID2,ST2,ET2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((ST1=ST2, ET1=ET2)
+ -> (
+ remove(activity(ID1,ST1,ET1,Attrs1),I,J1), % and merge
+ remove(activity(ID2,ST2,ET2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [activity(ID1,ST1,ET1,Attrs)|J2])
+ ; J = invalid).
+
+
+% Constraint 22.3: key constraint: agent
+infer(I,J) :- multimember(agent(ID1,Attrs1),
+ agent(ID2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ remove(agent(ID1,Attrs1),I,J1), % and merge
+ remove(agent(ID2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [agent(ID1,Attrs)|J2].
+
+% Constraint 23.1: key constraint: used
+infer(I,J) :- multimember(wasGeneratedBy(ID1,E1,A1,T1,Attrs1),
+ wasGeneratedBy(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(wasGeneratedBy(ID1,E1,A1,T1,Attrs1),I,J1), % and merge
+ 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
+infer(I,J) :- multimember(used(ID1,A1,E1,T1,Attrs1),
+ used(ID2,A2,E2,T2,Attrs2),I),
+ ID1 == ID2, % If keys are equal terms
+ % And non-keys are unifiable, unify them
+ ((A1 = A2, E1 = E2, T1 = T2)
+ -> (
+ remove(used(ID1,A1,E1,T1,Attrs1),I,J1), % and merge
+ remove(used(ID2,A2,E2,T2,Attrs2),J1,J2),
+ append(Attrs1,Attrs2,Attrs),
+ J = [used(ID1,A1,E1,T1,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
+
+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),
+ member(wasEndedBy(End,A,_E2,_A2,_T2,_Attrs2),I),
+ \+(member(precedes(Start,End),O1)),
+ O2 = [precedes(Start,End)|O1].
+
+% TODO: Lots more ordering constraints following this pattern.
+
+ordering_saturate(I,O,O) :- \+(ordering_step(I,O,_)),!.
+ordering_saturate(I,O1,O3) :-
+ ordering_step(I,O1,O2),
+ saturate_ordering(I,O2,O3).
+
+strict_cycle(_O) :- fail. % TODO: Search graph for cycles containing a strict edge. Prolog 101.
+
+ordering_check(I) :-
+ ordering_saturate(I,[],O),
+ \+(strict_cycle(O)).
+
+
+% Typing constraints
+% Constraint 50.1
+typing_step(I) -->
+ {member(entity(E,_Attrs),I)},
+ ensure(typeOf(E,entity)).
+
+% Constraint 50.2
+typing_step(I) -->
+ {member(agent(Ag,_Attrs),I)},
+ ensure(typeOf(Ag,agent)).
+
+% Constraint 50.3
+typing_step(I) -->
+ {member(activity(A,_T1,_T2,_Attrs),I)},
+ ensure(typeOf(A,activity)).
+
+ % Disjunction in conclusion is correct here
+ % because we can take a saturation step
+ % iff either conclusion is not yet satisfied
+
+% Constraint 50.4.
+typing_step(I) -->
+ {member(used(_ID,A,E,_T,_Attrs),I)},
+ (ensure(typeOf(A,activity)) ;
+ ensure(typeOf(E,entity)) ).
+
+% Constraint 50.5.
+typing_step(I) -->
+ {member(wasGeneratedBy(_ID,E,A,_T,_Attrs),I)},
+ (ensure(typeOf(A,activity)) ;
+ ensure(typeOf(E,entity)) ).
+
+% Constraint 50.9.
+typing_step(I) -->
+ {member(wasInvalidatedBy(_ID,E,A,_T,_Attrs),I)},
+ (ensure(typeOf(A,activity)) ;
+ ensure(typeOf(E,entity)) ).
+
+
+% Constraint 50.10.
+typing_step(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),
+ A \== null, Gen \== null, Use \== null},
+ (ensure(typeOf(E1,entity)) ;
+ ensure(typeOf(E2,entity)) ;
+ ensure(typeOf(A,activity)) ).
+
+
+
+% Constraint 50.13.
+typing_step(I) -->
+ {member(wasAssociatedWith(_id,A,Ag,Pl,_Attrs),I),
+ Pl \== null},
+ (ensure(typeOf(A,activity)) ;
+ ensure(typeOf(Ag,agent)) ;
+ ensure(typeOf(Pl,entity)) ).
+
+% Constraint 50.14.
+typing_step(I) -->
+ {member(wasAssociatedWith(_id,A,Ag,Pl,_Attrs),I),
+ Pl == null},
+ (ensure(typeOf(A,activity)) ;
+ ensure(typeOf(Ag,agent)) ).
+
+
+% TODO: More typing constraints
+
+
+typing_saturate(I,T,T) :- \+(typing_step(I,T,_)).
+typing_saturate(I,T1,T3) :- typing_step(I,T1,T2), !, typing_saturate(I,T2,T3).
+
+typing(I,T) :- typing_saturate(I,[],T).
+
+% Impossibility constraints
+
+%Some background info
+object(entity).
+object(activity).
+object(agent).
+relation(used).
+relation(wasGeneratedBy).
+relation(wasInvalidatedBy).
+relation(wasStartedBy).
+relation(wasEndedBy).
+relation(wasInformedBy).
+relation(wasAttributedTo).
+relation(wasAssociatedWith).
+relation(actedOnBehalfOf).
+
+% Constraint 51
+impos(I,_T) :- member(wasDerivedFrom(_Id,_E2,_E1,null,G,null,_Attrs),I),
+ G \== null.
+impos(I,_T) :- member(wasDerivedFrom(_Id,_E2,_E1,null,null,U,_Attrs),I),
+ U \== null.
+impos(I,_T) :- member(wasDerivedFrom(_Id,_E2,_E1,null,G,U,_Attrs),I),
+ G \== null, U \== null.
+
+
+
+%Constraint 52. Have to be careful not to unify.
+impos(I,_T) :- member(specializationOf(E1,E2),I), E1 == E2.
+
+% Constraint 53.
+
+
+impos(I,_T) :- member(T1,I),
+ member(T2,I),
+ T1 =.. [R,Id1|_],
+ T2 =.. [S,Id2|_],
+ Id1 == Id2,
+ relation(R),
+ relation(S),
+ R \== S.
+
+%Constraint 54
+impos(I,_T) :- member(T1,I),
+ member(T2,I),
+ T1 =.. [P,Id1|_],
+ T2 =.. [R,Id2|_],
+ Id1 == Id2,
+ object(P),
+ relation(R).
+
+% Constraint 55
+impos(_I,T) :- member(typeOf(Id1,entity),T),
+ member(typeOf(Id2,activity),T),
+ Id1 == Id2.
+
+% Constraint 56
+impos(I,T) :- member(hadMember(C1,_E1),I),
+ member(typeOf(C2,'prov:EmptyCollection'),T),
+ C1 == C2.
+
+
+impos_check(I,T) :- \+(impos(I,T)).
+
+valid(I) :- normalize(I,J),
+ ordering_check(J),
+ typing(J,T),
+ impos_check(J,T).
\ No newline at end of file