--- a/semantics/constraints.pl Wed Jan 09 16:11:26 2013 +0000
+++ b/semantics/constraints.pl Wed Jan 09 16:11:44 2013 +0000
@@ -7,6 +7,7 @@
%% Rules is the body of the rule.
%% A declaration body is of the form
%% Body ::= rule(Xs,Hyps,Ys,Concls)
+%% | rule(Xs,Hyps,Concls) % no existential vars
%% | comment(Comment,Body)
%% | rules([Body1,...,Bodyn])
%% A rule(Xs,Hyps,Ys,Body) is an implication
@@ -30,19 +31,19 @@
[wasGeneratedBy(gen, e,a_1,t_1,[]), used(use, a_2,e,t_2,[])])).
decl('Inference', 6, 'generation-use-communication-inference',
- rule([gen, a_1, t_1, attrs_1,id_2,a_2,t_2,attrs_2],
- [wasGeneratedBy(gen, e,a_1,t_1,attrs_1),
- used(id_2, a_2,e,t_2,attrs_2)],
- [id],
- [wasInformedBy(id, a_2,a_1,[])])).
-
-decl('Inference', 7, 'entity-generation-invalidation-inference',
rule([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),
used(id_2, a_2,e,t_2,attrs_2)],
[id],
[wasInformedBy(id, a_2,a_1,[])])).
+decl('Inference', 7, 'entity-generation-invalidation-inference',
+ rule([e,attrs],
+ [entity(e,attrs)],
+ [gen,a_1,t_1,inv,a_2,t_2],
+ [wasGeneratedBy(gen,e,a_1,t_1,[]),
+ wasInvalidatedBy(inv,e,a_2,t_2,[])])).
+
decl('Inference', 8, 'activity-start-end-inference',
rule([a, t_1, t_2, attrs],
[activity(a,t_1,t_2,attrs)],
@@ -67,8 +68,11 @@
decl('Inference', 11, 'derivation-generation-use-inference',
comment('In this inference, none of <em>a</em>, <em>gen<sub>2</sub></em> or <em>use_1</em> can be placeholders -.',
rule( [id, e_2, e_1, a, gen_2, use_1, attrs],
- [wasDerivedFrom(id, e_2,e_1,a,gen_2,use_1,attrs)],
- [s, t_1,t_2 ],
+ [notNull(a),
+ notNull(gen_2),
+ notNull(use_1),
+ wasDerivedFrom(id, e_2,e_1,a,gen_2,use_1,attrs)],
+ [t_1,t_2 ],
[used(use_1, a,e_1,t_1,[]),
wasGeneratedBy(gen_2, e_2,a,t_2,[])]))).
@@ -77,7 +81,6 @@
comment('In this inference, any of <em>a</em>, <em>g</em> or <em>u</em> may be placeholders.',
rule( [id, e_1, e_2, a, g,u],
[wasDerivedFrom(id, e_2,e_1,a,g,u,['prov:type = prov:Revision'])],
- [],
[alternateOf(e_2,e_1)]))).
decl('Inference', 13, 'attribution-inference',
@@ -97,45 +100,35 @@
decl('Inference', 15, 'influence-inference',
rules([rule( [id, e, a, t, attrs],
[wasGeneratedBy(id, e,a,t,attrs)],
- [],
[wasInfluencedBy(id, e, a, attrs)]),
rule( [id, a, e, t, attrs],
[used(id, a,e,t,attrs)],
- [],
[wasInfluencedBy(id, a, e, attrs)]),
rule( [id, a_2, a_1, attrs],
[wasInformedBy(id, a_2,a_1,attrs)],
- [],
[wasInfluencedBy(id, a_2, a_1, attrs)]),
rule( [id, a_2, e, a_1, t, attrs],
[wasStartedBy(id, a_2,e,a_1,t,attrs)],
- [],
[wasInfluencedBy(id, a_2, e, attrs)]),
rule( [id, a_2, e, a_1, t, attrs],
[wasEndedBy(id, a_2,e,a_1,t,attrs)],
- [],
[wasInfluencedBy(id, a_2, e, attrs)]),
rule( [id, e, a, t, attrs],
[wasInvalidatedBy(id, e,a,t,attrs)],
- [],
[wasInfluencedBy(id, e, a, attrs)]),
rule( [id, e_2, e_1, a, g, u, attrs],
[wasDerivedFrom(id, e_2, e_1, a, g, u, attrs)],
- [],
[wasInfluencedBy(id, e_2, e_1, attrs)]),
comment('In this rule, <em>a</em>, <em>g</em>, <em>u</em> may be placeholders -.',
rule( [id, e, ag, attrs],
[wasAttributedTo(id, e,ag,attrs)],
- [],
[wasInfluencedBy(id, e, ag, attrs)])),
comment('In this rule, <em>pl</em> may be a placeholder -.',
rule( [id, a, ag, pl, attrs],
[wasAssociatedWith(id, a,ag,pl,attrs)],
- [],
[wasInfluencedBy(id, a, ag, attrs)])),
rule( [id, ag_2, ag_1, a, attrs],
[actedOnBehalfOf(id, ag_2,ag_1,a,attrs)],
- [],
[wasInfluencedBy(id, ag_2, ag_1, attrs)])])).
decl('Inference', 16, 'alternate-reflexive',
@@ -176,9 +169,267 @@
%% Constraints. Most of these remain to do.
+decl('Constraint',24,'unique-generation',
+ rule([gen_1,gen_2,e,a,t_1,t_2,attrs_1,attrs_2],
+ [wasGeneratedBy(gen_1, e,a,t_1,attrs_1),
+ wasGeneratedBy(gen_2, e,a,t_2,attrs_2)],
+ [], [gen_1 = gen_2])).
+
+decl('Constraint',25,'unique-invalidation',
+ rule([inv_1,inv_2,e,a,t_1,t_2,attrs_1,attrs_2],
+ [wasInvalidatedBy(inv_1, e,a,t_1,attrs_1),
+ wasInvalidatedBy(inv_2, e,a,t_2,attrs_2)],
+ [], [inv_1 = inv_2])).
+
+decl('Constraint', 26,'unique-wasStartedBy',
+ rule( [ 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) ,
+ wasStartedBy(start_2, a,e_2,a_0,t_2,attrs_2) ],
+ [],
+ [ start_1 = start_2])).
+
+decl('Constraint', 27 ,'unique-wasEndedBy',
+ rule([ 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,a_0,t_1,attrs_1) ,
+ wasEndedBy(end_2, a,e_2,a_0,t_2,attrs_2)],
+ [],
+ [ end_1 = end_2])).
+
+decl('Constraint', 28, 'unique-startTime',
+ rule( [ start,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1 ],
+ [activity(a_2,t_1,t_2,attrs) ,
+ wasStartedBy(start, a_2,e,a_1,t,attrs_1) ],
+ [],[ t_1=t])).
+
+
+decl('Constraint', 29, 'unique-endTime',
+ rule( [ end,a_1,a_2,t,t_1,t_2,e,attrs,attrs_1],
+ [activity(a_2,t_1,t_2,attrs) ,
+ wasEndedBy(end, a_2,e,a_1,t,attrs_1) ],
+ [],
+ [ t_2 = t])).
+
+decl('Constraint', 30, 'start-precedes-end',
+ rule( [ 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),
+ wasEndedBy(end, a,e_2,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(start,end)])).
+
+decl('Constraint', 31, 'start-start-ordering',
+ rule( [ 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) ,
+ wasStartedBy(start_2, a,e_2,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(start_1, start_2)])).
+
+decl('Constraint', 32, 'end-end-ordering',
+ rule( [ 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) ,
+ wasEndedBy(end_2, a,e_2,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(end_1, end2)])).
+
+decl('Constraint', 33, 'usage-within-activity',
+ rules([rule(
+ [ 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) ,
+ used(use, a,e_2,t_2,attrs_2) ],
+ [],
+ [ preceq(start, use)]
+ ),
+ rule(
+ [ 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) ,
+ wasEndedBy(end, a,e_2,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(use,end)])])).
+
+decl('Constraint', 34, 'generation-within-activity',
+ rules([rule(
+ [ 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) ,
+ wasGeneratedBy(gen, e_2,a,t_2,attrs_2) ],
+ [],
+ [ preceq(start, gen)]),
+ rule(
+ [ gen,end,e,e_1,a,a_1,t,t_1,attrs,attrs_1 ],
+ [ wasGeneratedBy(gen, e,a,t,attrs) ,
+ wasEndedBy(end, a,e_1,a_1,t_1,attrs_1) ],
+ [],
+ [ preceq(gen,end)])])).
+
+decl('Constraint', 35, 'wasInformedBy-ordering',
+ rule( [ 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) ,
+ wasStartedBy(start, a_1,e_1,'a_1\'',t_1,attrs_1) ,
+ wasEndedBy(end, a_2,e_2,'a_2\'',t_2,attrs_2) ],
+ [],
+ [ preceq(start, end)])).
+
+decl('Constraint', 36, 'generation-precedes-invalidation',
+ rule( [ gen,inv,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 ],
+ [ wasGeneratedBy(gen, e,a_1,t_1,attrs_1) ,
+ wasInvalidatedBy(inv, e,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(gen ,inv)])).
+
+decl('Constraint', 37, 'generation-precedes-usage',
+ rule( [ gen,use,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 ],
+ [ wasGeneratedBy(gen, e,a_1,t_1,attrs_1) ,
+ used(use, a_2,e,t_2,attrs_2) ],
+ [],
+ [ preceq(gen, use)])).
+
+decl('Constraint', 38, 'usage-precedes-invalidation',
+ rule( [ use,inv,a_1,a_2,e,t_1,t_2,attrs_1,attrs_2 ],
+ [ used(use, a_1,e,t_1,attrs_1) ,
+ wasInvalidatedBy(inv, e,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(use, inv)])).
+
+decl('Constraint', 39, 'generation-generation-ordering',
+ rule( [ 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) ,
+ wasGeneratedBy(gen_2, e,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(gen_1, gen_2)])).
+
+decl('Constraint', 40, 'invalidation-invalidation-ordering',
+ rule( [ 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) ,
+ wasInvalidatedBy(inv_2, e,a_2,t_2,attrs_2) ],
+ [],
+ [ preceq(inv_1, inv_2)])).
+
+decl('Constraint', 41, 'derivation-usage-generation-ordering',
+ comment('In this constraint, <math>a</math>, <math>gen_2</math>, <math>use_1</math> must not be placeholders.',
+ rule( [ d,e_1,e_2,a,gen_2,use_1,attrs ],
+ [ notNull(a) ,
+ notNull(gen_2) ,
+ notNull(use_1) ,
+ wasDerivedFrom(d, e_2,e_1,a,gen_2,use_1,attrs) ],
+ [ preceq(use_1, gen_2)]))).
+
+decl('Constraint', 42, 'derivation-generation-generation-ordering',
+ comment('In this constraint, any of <math>a</math>, <math>g</math>, <math>u</math> may be placeholders.',
+ rule( [ 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) ,
+ wasGeneratedBy(gen_1, e_1,a_1,t_1,attrs_1) ,
+ wasGeneratedBy(gen_2, e_2,a_2,t_2,attrs_2) ],
+ [ prec(gen_1, gen_2)]))).
+
+decl('Constraint', 43, 'wasStartedBy-ordering',
+ rules([rule([ gen,start,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 ],
+ [ wasGeneratedBy(gen, e,a_1,t_1,attrs_1) ,
+ wasStartedBy(start, a,e,a_2,t_2,attrs_2) ],
+ [ preceq(gen, start)]),
+ rule([ 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) ,
+ wasInvalidatedBy(inv, e,a_2,t_2,attrs_2) ],
+ [ preceq(start, inv)])])).
+
+decl('Constraint', 44, 'wasEndedBy-ordering',
+ rules([rule([ gen,end,e,a_1,a_2,t_1,t_2,attrs_1,attrs_2 ],
+ [ wasGeneratedBy(gen, e,a_1,t_1,attrs_1) ,
+ wasEndedBy(end, a,e,a_2,t_2,attrs_2) ],
+ [ preceq(gen, end)]),
+ rule([ 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) ,
+ wasInvalidatedBy(inv, e,a_2,t_2,attrs_2) ],
+ [ preceq(end, inv)])])).
+
+decl('Constraint', 45, 'specialization-generation-ordering',
+ rule( [ 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) ,
+ wasGeneratedBy(gen_1, e_1,a_1,t_1,attrs_1) ,
+ wasGeneratedBy(gen_2, e_2,a_2,t_2,attrs_2) ],
+ [ preceq(gen_1, gen_2)])).
+
+decl('Constraint', 46, 'specialization-invalidation-ordering',
+ rule( [ 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) ,
+ wasInvalidatedBy(inv_1, e_1,a_1,t_1,attrs_1) ,
+ wasInvalidatedBy(inv_2, e_2,a_2,t_2,attrs_2) ],
+ [ preceq(inv_1, inv_2)])).
+
+decl('Constraint', 47, 'wasAssociatedWith-ordering',
+ comment('In the following inferences, pl may be a placeholder -.',
+ rules([rule([ 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) ,
+ wasStartedBy(start_1, a,e_1,a_1,t_1,attrs_1) ,
+ wasInvalidatedBy(inv_2, ag,a_2,t_2,attrs_2) ],
+ [ preceq(start_1, inv_2)]),
+ rule([ 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) ,
+ wasGeneratedBy(gen_1, ag,a_1,t_1,attrs_1) ,
+ wasEndedBy(end_2, a,e_2,a_2,t_2,attrs_2) ],
+ [ preceq(gen_1, end_2)]),
+ rule([ 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) ,
+ wasStartedBy(start_1, a,e_1,a_1,t_1,attrs_1) ,
+ wasEndedBy(end_2, ag,e_2,a_2,t_2,attrs_2) ],
+ [ preceq(start_1, end_2)]),
+ rule([ 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) ,
+ wasStartedBy(start_1, ag,e_1,a_1,t_1,attrs_1) ,
+ wasEndedBy(end_2, a,e_2,a_2,t_2,attrs_2) ],
+ [ preceq(start_1, end_2)])]))).
+
+decl('Constraint', 48, 'wasAttributedTo-ordering',
+ rules([rule([ 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) ,
+ wasGeneratedBy(gen_1, ag,a_1,t_1,attrs_1) ,
+ wasGeneratedBy(gen_2, e,a_2,t_2,attrs_2) ],
+ [ preceq(gen_1, gen_2)]),
+ rule([ 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) ,
+ wasStartedBy(start_1, ag,e_1,a_1,t_1,attrs_1) ,
+ wasGeneratedBy(gen_2, e,a_2,t_2,attrs_2) ],
+ [ preceq(start_1, gen_2)])])).
+
+decl('Constraint', 49, 'actedOnBehalfOf-ordering',
+ rules([rule([ 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) ,
+ wasGeneratedBy(gen_1, ag_1,a_1,t_1,attrs_1) ,
+ wasInvalidatedBy(inv_2, ag_2,a_2,t_2,attrs_2) ],
+ [ preceq(gen_1, inv_2)]),
+ rule([ 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) ,
+ wasStartedBy(start_1, ag_1,e_1,a_1,t_1,attrs_1) ,
+ wasEndedBy(end2, ag_2,e_2,a_2,t_2,attrs_2) ],
+ [ preceq(start_1, end2)])])).
+
+
+decl('Constraint',51,'impossible-unspecified-derivation-generation-use',
+ rules([rule([id,e_1,e_2,g,attrs],
+ [notNull(g),wasDerivedFrom(id,e_2,e_1,-,g,-,attrs)],
+ [],
+ ['False']),
+ rule([id,e_1,e_2,u,attrs],
+ [notNull(u),wasDerivedFrom(id,e_2,e_1,-,-,u,attrs)],
+ [],
+ ['False']),
+ rule([id,e_1,e_2,g,u,attrs],
+ [notNull(g),notNull(u),wasDerivedFrom(id,e_2,e_1,-,g,u,attrs)],
+ [],
+ ['False'])])).
+
+
+decl('Constraint', 52, 'impossible-specialization-reflexive',
+ rule([e],
+ [specializationOf(e,e)],
+ [],
+ ['False'])).
+
+decl('Constraint', 55,'entity-activity-disjoint',
+ rule([id],
+ [typeOf(id,entity), typeOf(id,activity)],
+ [],[ 'False'])).
+
decl('Constraint',56, 'membership-empty-collection',
rule([c,e],
- [hasMember(c,e),'prov:EmptyCollection \\in typeOf(c)'],
+ [hasMember(c,e),typeOf(c,'prov:EmptyCollection')],
[],
['False'])).
@@ -198,6 +449,10 @@
emitListSep(Sep,Emit,[Q|Ps]).
+latexPred(T = U) --> emit(T), emit(' = '), emit(U),!.
+latexPred(typeOf(T,U)) --> emit(U), emit(' \\in typeOf('), emit(T), emit(')'),!.
+latexPred(preceq(T,U)) --> emit(T), emit(' \\preceq '), emit(U),!.
+latexPred(prec(T,U)) --> emit(T), emit(' \\prec '), emit(U),!.
latexPred(A) --> {atom(A)},emit(A).
latexPred(T) -->
{T =.. [F|Ts], Ts \= []},
@@ -232,6 +487,11 @@
latexConj(Concls),
emit('\n\\end{array}').
+latexRules(rule(Xs,Hyps,Concls)) -->
+ emit('<math>\n'),
+% Change this to change from logical formula to inference rule format
+ latexRule(Xs,Hyps,[],Concls),
+ emit('\n</math>').
latexRules(rule(Xs,Hyps,Ys,Concls)) -->
emit('<math>\n'),
@@ -313,6 +573,10 @@
htmlConj(Concls).
+htmlRules(rule(Xs,Hyps,Concls)) -->
+ emit('<span class="math">'),
+ htmlRule(Xs,Hyps,[],Concls),
+ emit('</span>').
htmlRules(rule(Xs,Hyps,Ys,Concls)) -->
emit('<span class="math">'),
@@ -364,5 +628,5 @@
close(Out).
main :- findall(X, decl(_,X,_,_),Xs),
- writeEach(htmlDecl,user,Xs).
+ writeEach(latexWiki,user,Xs).