--- a/semantics/constraints.pl Sun Dec 16 14:02:50 2012 -0500
+++ b/semantics/constraints.pl Mon Dec 17 10:38:13 2012 +0000
@@ -65,7 +65,7 @@
decl('Inference', 11, 'derivation-generation-use-inference',
- comment('In this inference, none of <math>a</math>, <math>gen_2</math> or <math>use_1</math> can be placeholders -',
+ 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 ],
@@ -74,7 +74,7 @@
decl('Inference', 12, 'revision-is-alternate-inference',
- comment('In this inference, any of <math>a</math>, <math>g</math> or <math>u</math> may be placeholders.',
+ 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'])],
[],
@@ -123,12 +123,12 @@
[wasDerivedFrom(id, e_2, e_1, a, g, u, attrs)],
[],
[wasInfluencedBy(id, e_2, e_1, attrs)]),
- comment('In this rule, <math>a</math>, <math>g</math>, <math>u</math> may be placeholders -.',
+ 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, <math>pl</math> may be a placeholder -',
+ comment('In this rule, <em>pl</em> may be a placeholder -.',
rule( [id, a, ag, pl, attrs],
[wasAssociatedWith(id, a,ag,pl,attrs)],
[],
@@ -269,10 +269,21 @@
%% Todo: Recognize subscripts and translate to <sub>
+emitVar(A) --> {split('_',A,X,I), !},
+ emit(X),
+ emit('<sub>'),
+ emit(I),
+ emit('</sub>').
emitVar(A) --> emit(A).
+split(C,A,A1,A2) :- atom(A),
+ atom_chars(A,L),
+ append(L1,[C|L2],L),
+ atom_chars(A1,L1),
+ atom_chars(A2,L2).
+
htmlPred(A) --> {atom(A)},
- emit(A).
+ emitVar(A).
htmlPred(T) -->
{T =.. [F|Ts], Ts \= []},
emit(F),
@@ -287,11 +298,11 @@
htmlQuantify(_Q,[]) --> [].
htmlQuantify(forall,Xs) --> {Xs \= []},
emit('∀ '),
- emitListSep(',', emit, Xs),
+ emitListSep(',', emitVar, Xs),
emit('. ').
htmlQuantify(exists,Xs) --> {Xs \= []},
emit('∃ '),
- emitListSep(',', emit, Xs),
+ emitListSep(',', emitVar, Xs),
emit('. ').
htmlRule(Xs,Hyps,Ys,Concls) -->
@@ -354,3 +365,4 @@
main :- findall(X, decl(_,X,_,_),Xs),
writeEach(htmlDecl,user,Xs).
+
--- a/semantics/prov-sem.html Sun Dec 16 14:02:50 2012 -0500
+++ b/semantics/prov-sem.html Mon Dec 17 10:38:13 2012 +0000
@@ -539,18 +539,21 @@
<script src="http://www.w3.org/2007/OWL/toggles.js" class="remove"></script>
<script src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.1/jquery.min.js" class="remove"></script>
-
- <script class="remove">
+ <script type="text/javascript" class="remove"
+ src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML">
+ </script>
+<script type="text/x-mathjax-config" class="remove">
+MathJax.Hub.Config({
+ tex2jax: {
+ inlineMath: [ ['$','$'], ["\\(","\\)"] ],
+ displayMath: [ ['$$','$$'], ["\\[","\\]"] ],
+ processEscapes: true
+ },
+ });
+</script>
-function setColoredDiffs () {
- $('dt').each(function(index) {
- var content=$(this).text();
- if (content== "Previous version:") {
- console.log( "content " + content);
- $(this).next().append(" ").append($('<a>').attr('href','diff-c.html').append("(colored-coded diff)"));
- }
- })
-}
+ <script class="remove">
+
function updateRules() {
@@ -894,7 +897,7 @@
// Add extraReferences to bibliography database
preProcess: [addExtraReferences, addProvReferences],
- postProcess: [updateFigures, removeDataAttributes, checkLinksToW3CReports, setColoredDiffs],
+ postProcess: [updateFigures, removeDataAttributes, checkLinksToW3CReports],
};
</script>
</head>
@@ -1002,27 +1005,47 @@
</section>
</section>
+<section id="test">
+<h2>MathJax test</h2>
+
+\(\newcommand{\wasDerivedFrom}{\mathit{wasDerivedFrom}}\)
+\(\newcommand{\wasInformedBy}{\mathit{wasInformedBy}}\)
+\(\newcommand{\wasGeneratedBy}{\mathit{wasGeneratedBy}}\)
+\(\newcommand{\used}{\mathit{used}}\)
+\(\newcommand{\entity}{\mathit{entity}}\)
+\(\newcommand{\activity}{\mathit{activity}}\)
+
+<p>When $a \ne 0$, there are two solutions to \(ax^2 + bx + c = 0\) and they are
+$$x = {-b \pm \sqrt{b^2-4ac} \over 2a}.$$
+</p>
+
+<div class="inference" id="communication-generation-use-inference">
+\(\forall id,a_2,a_1,attrs.~ \wasInformedBy(id,a_2,a_1,attrs) \Longrightarrow \exists e,gen,t_1,use,t_2.~\wasGeneratedBy(gen,e,a_1,t_1,[]) \wedge \used(use,a_2,e,t_2,[])\)</div>
+
+</section>
+
<section id="inferences">
<h2>Inferences</h2>
-<div class="inference" id="communication-generation-use-inference"><span class="math">∀ <span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">attrs</span>. wasInformedBy(id,a_2,a_1,attrs) ⟹ ∃ <span class="math">e</span>,<span class="math">gen</span>,<span class="math">t_1</span>,<span class="math">use</span>,<span class="math">t_2</span>. wasGeneratedBy(gen,e,a_1,t_1,[]) ∧ used(use,a_2,e,t_2,[])</span></div>
-<div class="inference" id="generation-use-communication-inference"><span class="math">∀ <span class="math">gen</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">attrs_1</span>,<span class="math">id_2</span>,<span class="math">a_2</span>,<span class="math">t_2</span>,<span class="math">attrs_2</span>. wasGeneratedBy(gen,e,a_1,t_1,attrs_1) ∧ used(id_2,a_2,e,t_2,attrs_2) ⟹ ∃ <span class="math">id</span>. wasInformedBy(id,a_2,a_1,[])</span></div>
-<div class="inference" id="entity-generation-invalidation-inference"><span class="math">∀ <span class="math">gen</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t_1</span>,<span class="math">attrs_1</span>,<span class="math">id_2</span>,<span class="math">a_2</span>,<span class="math">t_2</span>,<span class="math">attrs_2</span>. wasGeneratedBy(gen,e,a_1,t_1,attrs_1) ∧ used(id_2,a_2,e,t_2,attrs_2) ⟹ ∃ <span class="math">id</span>. wasInformedBy(id,a_2,a_1,[])</span></div>
-<div class="inference" id="activity-start-end-inference"><span class="math">∀ <span class="math">a</span>,<span class="math">t_1</span>,<span class="math">t_2</span>,<span class="math">attrs</span>. activity(a,t_1,t_2,attrs) ⟹ ∃ <span class="math">start</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">end</span>,<span class="math">a_2</span>,<span class="math">e_2</span>. wasStartedBy(start,a,e_1,a_1,t_1,[]) ∧ wasEndedBy(end,a,e_2,a_2,t_2,[])</span></div>
-<div class="inference" id="wasStartedBy-inference"><span class="math">∀ <span class="math">id</span>,<span class="math">a</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>. wasStartedBy(id,a,e_1,a_1,t,attrs) ⟹ ∃ <span class="math">gen</span>,<span class="math">t_1</span>. wasGeneratedBy(gen,e_1,a_1,t_1,[])</span></div>
-<div class="inference" id="wasEndedBy-inference"><span class="math">∀ <span class="math">id</span>,<span class="math">a</span>,<span class="math">e_1</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>. wasEndedBy(id,a,e_1,a_1,t,attrs) ⟹ ∃ <span class="math">gen</span>,<span class="math">t_1</span>. wasGeneratedBy(gen,e_1,a_1,t_1,[])</span></div>
-<div class="inference" id="derivation-generation-use-inference">In this inference, none of <math>a</math>, <math>gen_2</math> or <math>use_1</math> can be placeholders -<span class="math">∀ <span class="math">id</span>,<span class="math">e_2</span>,<span class="math">e_1</span>,<span class="math">a</span>,<span class="math">gen_2</span>,<span class="math">use_1</span>,<span class="math">attrs</span>. wasDerivedFrom(id,e_2,e_1,a,gen_2,use_1,attrs) ⟹ ∃ <span class="math">s</span>,<span class="math">t_1</span>,<span class="math">t_2</span>. used(use_1,a,e_1,t_1,[]) ∧ wasGeneratedBy(gen_2,e_2,a,t_2,[])</span></div>
-<div class="inference" id="revision-is-alternate-inference">In this inference, any of <math>a</math>, <math>g</math> or <math>u</math> may be placeholders.<span class="math">∀ <span class="math">id</span>,<span class="math">e_1</span>,<span class="math">e_2</span>,<span class="math">a</span>,<span class="math">g</span>,<span class="math">u</span>. wasDerivedFrom(id,e_2,e_1,a,g,u,.(=(prov:type,prov:Revision),[])) ⟹ alternateOf(e_2,e_1)</span></div>
-<div class="inference" id="attribution-inference"><span class="math">∀ <span class="math">att</span>,<span class="math">e</span>,<span class="math">ag</span>,<span class="math">attrs</span>. wasAttributedTo(att,e,ag,attrs) ⟹ ∃ <span class="math">a</span>,<span class="math">t</span>,<span class="math">gen</span>,<span class="math">assoc</span>,<span class="math">pl</span>. wasGeneratedBy(gen,e,a,t,[]) ∧ wasAssociatedWith(assoc,a,ag,pl,[])</span></div>
-<div class="inference" id="delegation-inference"><span class="math">∀ <span class="math">id</span>,<span class="math">ag_1</span>,<span class="math">ag_2</span>,<span class="math">a</span>,<span class="math">attrs</span>. actedOnBehalfOf(id,ag_1,ag_2,a,attrs) ⟹ ∃ <span class="math">id_1</span>,<span class="math">pl_1</span>,<span class="math">id_2</span>,<span class="math">pl_2</span>. wasAssociatedWith(id_1,a,ag_1,pl_1,[]) ∧ wasAssociatedWith(id_2,a,ag_2,pl_2,[])</span></div>
-<div class="inference" id="influence-inference"><ol><li><span class="math">∀ <span class="math">id</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">t</span>,<span class="math">attrs</span>. wasGeneratedBy(id,e,a,t,attrs) ⟹ wasInfluencedBy(id,e,a,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">a</span>,<span class="math">e</span>,<span class="math">t</span>,<span class="math">attrs</span>. used(id,a,e,t,attrs) ⟹ wasInfluencedBy(id,a,e,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">a_2</span>,<span class="math">a_1</span>,<span class="math">attrs</span>. wasInformedBy(id,a_2,a_1,attrs) ⟹ wasInfluencedBy(id,a_2,a_1,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>. wasStartedBy(id,a_2,e,a_1,t,attrs) ⟹ wasInfluencedBy(id,a_2,e,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">a_2</span>,<span class="math">e</span>,<span class="math">a_1</span>,<span class="math">t</span>,<span class="math">attrs</span>. wasEndedBy(id,a_2,e,a_1,t,attrs) ⟹ wasInfluencedBy(id,a_2,e,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">e</span>,<span class="math">a</span>,<span class="math">t</span>,<span class="math">attrs</span>. wasInvalidatedBy(id,e,a,t,attrs) ⟹ wasInfluencedBy(id,e,a,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">e_2</span>,<span class="math">e_1</span>,<span class="math">a</span>,<span class="math">g</span>,<span class="math">u</span>,<span class="math">attrs</span>. wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) ⟹ wasInfluencedBy(id,e_2,e_1,attrs)</span></li><li>In this rule, <math>a</math>, <math>g</math>, <math>u</math> may be placeholders -.<span class="math">∀ <span class="math">id</span>,<span class="math">e</span>,<span class="math">ag</span>,<span class="math">attrs</span>. wasAttributedTo(id,e,ag,attrs) ⟹ wasInfluencedBy(id,e,ag,attrs)</span></li><li>In this rule, <math>pl</math> may be a placeholder -<span class="math">∀ <span class="math">id</span>,<span class="math">a</span>,<span class="math">ag</span>,<span class="math">pl</span>,<span class="math">attrs</span>. wasAssociatedWith(id,a,ag,pl,attrs) ⟹ wasInfluencedBy(id,a,ag,attrs)</span></li><li><span class="math">∀ <span class="math">id</span>,<span class="math">ag_2</span>,<span class="math">ag_1</span>,<span class="math">a</span>,<span class="math">attrs</span>. actedOnBehalfOf(id,ag_2,ag_1,a,attrs) ⟹ wasInfluencedBy(id,ag_2,ag_1,attrs)</span></li></ol></div>
-<div class="inference" id="alternate-reflexive"><span class="math">∀ <span class="math">e</span>. entity(e) ⟹ alternateOf(e,e)</span></div>
-<div class="inference" id="alternate-transitive"><span class="math">∀ <span class="math">e_1</span>,<span class="math">e_2</span>,<span class="math">e_3</span>. alternateOf(e_1,e_2) ∧ alternateOf(e_2,e_3) ⟹ alternateOf(e_1,e_3)</span></div>
-<div class="inference" id="alternate-symmetric"><span class="math">∀ <span class="math">e_1</span>,<span class="math">e_2</span>. alternateOf(e_1,e_2) ⟹ alternateOf(e_2,e_1)</span></div>
-<div class="inference" id="specialization-transitive"><span class="math">∀ <span class="math">e_1</span>,<span class="math">e_2</span>,<span class="math">e_3</span>. specializationOf(e_1,e_2) ∧ specializationOf(e_2,e_3) ⟹ specializationOf(e_1,e_3)</span></div>
-<div class="inference" id="specialization-alternate-inference"><span class="math">∀ <span class="math">e_1</span>,<span class="math">e_2</span>. specializationOf(e_1,e_2) ⟹ alternateOf(e_1,e_2)</span></div>
-<div class="inference" id="specialization-attributes-inference"><span class="math">∀ <span class="math">e_1</span>,<span class="math">attrs</span>,<span class="math">e_2</span>. entity(e_1,attrs) ∧ specializationOf(e_2,e_1) ⟹ entity(e_2,attrs)</span></div>
+<div class="inference" id="communication-generation-use-inference"><span class="math">∀ id,a<sub>2</sub>,a<sub>1</sub>,attrs. wasInformedBy(id,a<sub>2</sub>,a<sub>1</sub>,attrs) ⟹ ∃ e,gen,t<sub>1</sub>,use,t<sub>2</sub>. wasGeneratedBy(gen,e,a<sub>1</sub>,t<sub>1</sub>,[]) ∧ used(use,a<sub>2</sub>,e,t<sub>2</sub>,[])</span></div>
+<div class="inference" id="generation-use-communication-inference"><span class="math">∀ gen,a<sub>1</sub>,t<sub>1</sub>,attrs<sub>1</sub>,id<sub>2</sub>,a<sub>2</sub>,t<sub>2</sub>,attrs<sub>2</sub>. wasGeneratedBy(gen,e,a<sub>1</sub>,t<sub>1</sub>,attrs<sub>1</sub>) ∧ used(id<sub>2</sub>,a<sub>2</sub>,e,t<sub>2</sub>,attrs<sub>2</sub>) ⟹ ∃ id. wasInformedBy(id,a<sub>2</sub>,a<sub>1</sub>,[])</span></div>
+<div class="inference" id="entity-generation-invalidation-inference"><span class="math">∀ gen,e,a<sub>1</sub>,t<sub>1</sub>,attrs<sub>1</sub>,id<sub>2</sub>,a<sub>2</sub>,t<sub>2</sub>,attrs<sub>2</sub>. wasGeneratedBy(gen,e,a<sub>1</sub>,t<sub>1</sub>,attrs<sub>1</sub>) ∧ used(id<sub>2</sub>,a<sub>2</sub>,e,t<sub>2</sub>,attrs<sub>2</sub>) ⟹ ∃ id. wasInformedBy(id,a<sub>2</sub>,a<sub>1</sub>,[])</span></div>
+<div class="inference" id="activity-start-end-inference"><span class="math">∀ a,t<sub>1</sub>,t<sub>2</sub>,attrs. activity(a,t<sub>1</sub>,t<sub>2</sub>,attrs) ⟹ ∃ start,e<sub>1</sub>,a<sub>1</sub>,end,a<sub>2</sub>,e<sub>2</sub>. wasStartedBy(start,a,e<sub>1</sub>,a<sub>1</sub>,t<sub>1</sub>,[]) ∧ wasEndedBy(end,a,e<sub>2</sub>,a<sub>2</sub>,t<sub>2</sub>,[])</span></div>
+<div class="inference" id="wasStartedBy-inference"><span class="math">∀ id,a,e<sub>1</sub>,a<sub>1</sub>,t,attrs. wasStartedBy(id,a,e<sub>1</sub>,a<sub>1</sub>,t,attrs) ⟹ ∃ gen,t<sub>1</sub>. wasGeneratedBy(gen,e<sub>1</sub>,a<sub>1</sub>,t<sub>1</sub>,[])</span></div>
+<div class="inference" id="wasEndedBy-inference"><span class="math">∀ id,a,e<sub>1</sub>,a<sub>1</sub>,t,attrs. wasEndedBy(id,a,e<sub>1</sub>,a<sub>1</sub>,t,attrs) ⟹ ∃ gen,t<sub>1</sub>. wasGeneratedBy(gen,e<sub>1</sub>,a<sub>1</sub>,t<sub>1</sub>,[])</span></div>
+<div class="inference" id="derivation-generation-use-inference">In this inference, none of <em>a</em>, <em>gen<sub>2</sub></em> or <em>use_1</em> can be placeholders -.<span class="math">∀ id,e<sub>2</sub>,e<sub>1</sub>,a,gen<sub>2</sub>,use<sub>1</sub>,attrs. wasDerivedFrom(id,e<sub>2</sub>,e<sub>1</sub>,a,gen<sub>2</sub>,use<sub>1</sub>,attrs) ⟹ ∃ s,t<sub>1</sub>,t<sub>2</sub>. used(use<sub>1</sub>,a,e<sub>1</sub>,t<sub>1</sub>,[]) ∧ wasGeneratedBy(gen<sub>2</sub>,e<sub>2</sub>,a,t<sub>2</sub>,[])</span></div>
+<div class="inference" id="revision-is-alternate-inference">In this inference, any of <em>a</em>, <em>g</em> or <em>u</em> may be placeholders.<span class="math">∀ id,e<sub>1</sub>,e<sub>2</sub>,a,g,u. wasDerivedFrom(id,e<sub>2</sub>,e<sub>1</sub>,a,g,u,.(prov:type = prov:Revision,[])) ⟹ alternateOf(e<sub>2</sub>,e<sub>1</sub>)</span></div>
+<div class="inference" id="attribution-inference"><span class="math">∀ att,e,ag,attrs. wasAttributedTo(att,e,ag,attrs) ⟹ ∃ a,t,gen,assoc,pl. wasGeneratedBy(gen,e,a,t,[]) ∧ wasAssociatedWith(assoc,a,ag,pl,[])</span></div>
+<div class="inference" id="delegation-inference"><span class="math">∀ id,ag<sub>1</sub>,ag<sub>2</sub>,a,attrs. actedOnBehalfOf(id,ag<sub>1</sub>,ag<sub>2</sub>,a,attrs) ⟹ ∃ id<sub>1</sub>,pl<sub>1</sub>,id<sub>2</sub>,pl<sub>2</sub>. wasAssociatedWith(id<sub>1</sub>,a,ag<sub>1</sub>,pl<sub>1</sub>,[]) ∧ wasAssociatedWith(id<sub>2</sub>,a,ag<sub>2</sub>,pl<sub>2</sub>,[])</span></div>
+<div class="inference" id="influence-inference"><ol><li><span class="math">∀ id,e,a,t,attrs. wasGeneratedBy(id,e,a,t,attrs) ⟹ wasInfluencedBy(id,e,a,attrs)</span></li><li><span class="math">∀ id,a,e,t,attrs. used(id,a,e,t,attrs) ⟹ wasInfluencedBy(id,a,e,attrs)</span></li><li><span class="math">∀ id,a<sub>2</sub>,a<sub>1</sub>,attrs. wasInformedBy(id,a<sub>2</sub>,a<sub>1</sub>,attrs) ⟹ wasInfluencedBy(id,a<sub>2</sub>,a<sub>1</sub>,attrs)</span></li><li><span class="math">∀ id,a<sub>2</sub>,e,a<sub>1</sub>,t,attrs. wasStartedBy(id,a<sub>2</sub>,e,a<sub>1</sub>,t,attrs) ⟹ wasInfluencedBy(id,a<sub>2</sub>,e,attrs)</span></li><li><span class="math">∀ id,a<sub>2</sub>,e,a<sub>1</sub>,t,attrs. wasEndedBy(id,a<sub>2</sub>,e,a<sub>1</sub>,t,attrs) ⟹ wasInfluencedBy(id,a<sub>2</sub>,e,attrs)</span></li><li><span class="math">∀ id,e,a,t,attrs. wasInvalidatedBy(id,e,a,t,attrs) ⟹ wasInfluencedBy(id,e,a,attrs)</span></li><li><span class="math">∀ id,e<sub>2</sub>,e<sub>1</sub>,a,g,u,attrs. wasDerivedFrom(id,e<sub>2</sub>,e<sub>1</sub>,a,g,u,attrs) ⟹ wasInfluencedBy(id,e<sub>2</sub>,e<sub>1</sub>,attrs)</span></li><li>In this rule, <em>a</em>, <em>g</em>, <em>u</em> may be placeholders -.<span class="math">∀ id,e,ag,attrs. wasAttributedTo(id,e,ag,attrs) ⟹ wasInfluencedBy(id,e,ag,attrs)</span></li><li>In this rule, <em>pl</em> may be a placeholder -.<span class="math">∀ id,a,ag,pl,attrs. wasAssociatedWith(id,a,ag,pl,attrs) ⟹ wasInfluencedBy(id,a,ag,attrs)</span></li><li><span class="math">∀ id,ag<sub>2</sub>,ag<sub>1</sub>,a,attrs. actedOnBehalfOf(id,ag<sub>2</sub>,ag<sub>1</sub>,a,attrs) ⟹ wasInfluencedBy(id,ag<sub>2</sub>,ag<sub>1</sub>,attrs)</span></li></ol></div>
+<div class="inference" id="alternate-reflexive"><span class="math">∀ e. entity(e) ⟹ alternateOf(e,e)</span></div>
+<div class="inference" id="alternate-transitive"><span class="math">∀ e<sub>1</sub>,e<sub>2</sub>,e<sub>3</sub>. alternateOf(e<sub>1</sub>,e<sub>2</sub>) ∧ alternateOf(e<sub>2</sub>,e<sub>3</sub>) ⟹ alternateOf(e<sub>1</sub>,e<sub>3</sub>)</span></div>
+<div class="inference" id="alternate-symmetric"><span class="math">∀ e<sub>1</sub>,e<sub>2</sub>. alternateOf(e<sub>1</sub>,e<sub>2</sub>) ⟹ alternateOf(e<sub>2</sub>,e<sub>1</sub>)</span></div>
+<div class="inference" id="specialization-transitive"><span class="math">∀ e<sub>1</sub>,e<sub>2</sub>,e<sub>3</sub>. specializationOf(e<sub>1</sub>,e<sub>2</sub>) ∧ specializationOf(e<sub>2</sub>,e<sub>3</sub>) ⟹ specializationOf(e<sub>1</sub>,e<sub>3</sub>)</span></div>
+<div class="inference" id="specialization-alternate-inference"><span class="math">∀ e<sub>1</sub>,e<sub>2</sub>. specializationOf(e<sub>1</sub>,e<sub>2</sub>) ⟹ alternateOf(e<sub>1</sub>,e<sub>2</sub>)</span></div>
+<div class="inference" id="specialization-attributes-inference"><span class="math">∀ e<sub>1</sub>,attrs,e<sub>2</sub>. entity(e<sub>1</sub>,attrs) ∧ specializationOf(e<sub>2</sub>,e<sub>1</sub>) ⟹ entity(e<sub>2</sub>,attrs)</span></div>
+<div class="constraint" id="membership-empty-collection"><span class="math">∀ c,e. hasMember(c,e) ∧ prov:EmptyCollection \in typeOf(c) ⟹ False</span></div>
</section>