* Updated constraint symbolic representations
authorjcheney@inf.ed.ac.uk
Wed, 09 Jan 2013 15:12:17 +0000
changeset 5394 067cd1968039
parent 5393 165edc482426
child 5396 43de412d4596
child 5408 ed4a27738f4b
* Updated constraint symbolic representations
semantics/constraints.pl
semantics/prov-sem.html
--- a/semantics/constraints.pl	Wed Jan 09 15:20:14 2013 +0100
+++ b/semantics/constraints.pl	Wed Jan 09 15:12:17 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).
 
--- a/semantics/prov-sem.html	Wed Jan 09 15:20:14 2013 +0100
+++ b/semantics/prov-sem.html	Wed Jan 09 15:12:17 2013 +0000
@@ -548,7 +548,10 @@
  tex2jax: {
       inlineMath: [ ['$','$'], ["\\(","\\)"] ],
       displayMath: [ ['$$','$$'], ["\\[","\\]"] ],
-      processEscapes: true
+      processEscapes: true,
+      "HTML-CSS": {
+    availableFonts: ["STIX"]
+  }
     },
  });
 </script>