moving back to blank nodes with formula scope

eyereasoner · Jul 8, 2021 · 9536c37 · 9536c37
1 parent c91fbe1
commit 9536c37
Show file tree

Hide file tree

Showing 53 changed files with 743 additions and 677 deletions.
diff --git a/RELEASE b/RELEASE
@@ -1,5 +1,6 @@
                                   EYE release
 
+[v21.0708.1245] moving back to blank nodes with formula scope
 [v21.0706.1214] fixing log:semantics (obs from Doerthe Arndt)
 [v21.0622.1431] fixing blank node quantification according to https://lists.w3.org/Archives/Public/public-n3-dev/2021Jun/0026.html
 [v21.0621.2307] looking into consequences of 'static' (lexical) scoping behaviour of bnodes

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-EYE v21.0706.1214 josd
+EYE v21.0708.1245 josd
diff --git a/eye.pl b/eye.pl
@@ -22,7 +22,7 @@
 :- use_module(library(prolog_jiti)).
 :- use_module(library(http/http_open)).
 
-version_info('EYE v21.0706.1214 josd').
+version_info('EYE v21.0708.1245 josd').
 
 license_info('MIT License
 
@@ -1558,7 +1558,8 @@
     !,
     {   gensym('bn_', S),
         (   (   nb_getval(entail_mode, false),
-                nb_getval(fdepth, 0)
+                nb_getval(fdepth, FD),
+                FD =\= 1
             ;   flag('pass-all-ground')
             )
         ->  nb_getval(skolem_ns, Sns),
@@ -1860,15 +1861,23 @@
         )
     }.
 symbol(Name) -->
-    [bnode(N)],
-    {   (   evar(N, S, 0)
+    [bnode(Label)],
+    {   nb_getval(fdepth, D),
+        (   D =:= 0
+        ->  N = Label
+        ;   atom_codes(Label, LabelCodes),
+            subst([[[0'-], [0'_, 0'M, 0'I, 0'N, 0'U, 0'S, 0'_]], [[0'.], [0'_, 0'D, 0'O, 0'T, 0'_]]], LabelCodes, LabelTidy),
+            atom_codes(N, LabelTidy)
+        ),
+        (   evar(N, S, D)
         ->  true
         ;   atom_concat(N, '_', M),
             gensym(M, S),
-            assertz(evar(N, S, 0))
+            assertz(evar(N, S, D))
         ),
         (   (   nb_getval(entail_mode, false),
-                nb_getval(fdepth, 0)
+                nb_getval(fdepth, FD),
+                FD =\= 1
             ;   flag('pass-all-ground')
             )
         ->  nb_getval(skolem_ns, Sns),
@@ -4035,6 +4044,14 @@
         conj_list(Concs, Ls),
         conj_list(Conce, Le),
         astep(Src, Prem, Concd, Conce, Rule),
+        findvars(Prem, Vars, delta),
+        forall(
+            member(Var, Vars),
+            (   \+keep_skolem(Var)
+            ->  assertz(keep_skolem(Var))
+            ;   true
+            )
+        ),
         (   (   Concs = answer(_, _, _)
             ;   Concs = (answer(_, _, _), _)
             )

diff --git a/eye.zip b/eye.zip
diff --git a/reasoning/4color/4color_answer.n3 b/reasoning/4color/4color_answer.n3
@@ -2,6 +2,7 @@ PREFIX : <http://josd.github.io/eye/reasoning/4color#>
 PREFIX list: <http://www.w3.org/2000/10/swap/list#>
 PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>
 PREFIX func: <http://www.w3.org/2007/rif-builtin-function#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/_t:EpZM32quRDa:A:P02qtQ_l04#>
 
 ((:United_Kingdom :blue) (:Sweden :blue) (:Spain :blue) (:Slovenia :yellow) (:Slovakia :blue) (:Romania :blue) (:Portugal :red) (:Poland :red) (:Netherlands :green) (:Malta :red) (:Luxemburg :yellow) (:Lithuania :blue) (:Latvia :green) (:Italy :blue) (:Ireland :red) (:Hungary :green) (:Greece :green) (:Germany :blue) (:France :green) (:Finland :green) (:Estonia :red) (:Denmark :red) (:Czech_Republic :green) (:Cyprus :red) (:Croatia :red) (:Bulgaria :red) (:Belgium :red) (:Austria :red)) :coloring true.
 ((:United_Kingdom :yellow) (:Sweden :blue) (:Spain :blue) (:Slovenia :yellow) (:Slovakia :blue) (:Romania :blue) (:Portugal :red) (:Poland :red) (:Netherlands :green) (:Malta :red) (:Luxemburg :yellow) (:Lithuania :blue) (:Latvia :green) (:Italy :blue) (:Ireland :red) (:Hungary :green) (:Greece :green) (:Germany :blue) (:France :green) (:Finland :green) (:Estonia :red) (:Denmark :red) (:Czech_Republic :green) (:Cyprus :red) (:Croatia :red) (:Bulgaria :red) (:Belgium :red) (:Austria :red)) :coloring true.

diff --git a/reasoning/4color/4color_proof.n3 b/reasoning/4color/4color_proof.n3
@@ -3,6 +3,7 @@ PREFIX list: <http://www.w3.org/2000/10/swap/list#>
 PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>
 PREFIX func: <http://www.w3.org/2007/rif-builtin-function#>
 PREFIX r: <http://www.w3.org/2000/10/swap/reason#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/NPMQZ7VcnkS5UFkiokicPOZuVkA#>
 
 [] a r:Proof, r:Conjunction;
   r:component <#lemma1>;

diff --git a/reasoning/bi/biA.n3 b/reasoning/bi/biA.n3
@@ -9,6 +9,7 @@ PREFIX med: <http://eulersharp.sourceforge.net/2006/02swap/med#>
 PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>
 PREFIX : <http://eulersharp.sourceforge.net/2007/07test#>
 PREFIX fl: <http://eulersharp.sourceforge.net/2003/03swap/fl-rules#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/L2TEOLM0K9fiDhnIneNUM5sYrew#>
 
 {{(55 66 72 87 56 77 73 69 74 56) e:avg 68.5 . 68.5 math:equalTo 68.5} => {:ea1 :result true}} a :PASS.
 {{("1+1") e:calculate 2 . 2 math:equalTo 2} => {:ec1 :result true}} a :PASS.
@@ -46,8 +47,8 @@ PREFIX fl: <http://eulersharp.sourceforge.net/2003/03swap/fl-rules#>
 {{((<http://josd.github.io/eye/reasoning/bi/biP.n3>) 1) e:fail {(1 2 3 4 5) e:subsequence (4 2 1)}} => {:esl2 :result true}} a :PASS.
 {{() e:subsequence ()} => {:esl3 :result true}} a :PASS.
 {{((0 1) (2 3) (4 5)) e:transpose ((0 2 4) (1 3 5))} => {:et1 :result true}} a :PASS.
-{{:a :b :c. :c e:whenGround {:a :b :d}} => {:ewg1 :result true}} a :PASS.
-{{:a :b :d. :d e:whenGround {:a :b :d}} => {:ewg1 :result true}} a :PASS.
+{{:c e:whenGround {:a :b :d}. :a :b :c} => {:ewg1 :result true}} a :PASS.
+{{:d e:whenGround {:a :b :d}. :a :b :d} => {:ewg1 :result true}} a :PASS.
 {{"http://www.agfa.com/w3c/euler" e:wwwFormEncode "http%3a%2f%2fwww.agfa.com%2fw3c%2feuler"} => {:ew1 :result true}} a :PASS.
 {{"Hello World!" e:wwwFormEncode "Hello+World%21"} => {:ew2 :result true}} a :PASS.
 {{((:a :b :c) (:d :e)) list:append (:a :b :c :d :e)} => {:lista1 :result true}} a :PASS.
@@ -60,25 +61,25 @@ PREFIX fl: <http://eulersharp.sourceforge.net/2003/03swap/fl-rules#>
 {{(true {:u :v :w} {:x :y :z. :j :k :l}) log:conjunction {:u :v :w. :x :y :z. :j :k :l}} => {:logc2 :result true}} a :PASS.
 {{(true {:u :v :w} true true) log:conjunction {:u :v :w}} => {:logc3 :result true}} a :PASS.
 {{(:a :b) log:equalTo (:a :b)} => {:loge1 :result true}} a :PASS.
-{{{:a :b :c} log:equalTo {:a :b :c}} => {:loge2 :result true}} a :PASS.
-{{{:a :b :_c} log:equalTo {:a :b :_c}} => {:loge3 :result true}} a :PASS.
+{{{:a :b :c} log:equalTo {:a :b :c}} => {:logee1 :result true}} a :PASS.
 {{<http://josd.github.io/eye/reasoning/bi/abc.n3> log:semantics {:a :b :c}. {:a :b :c} log:equalTo {:a :b :c}} => {:loges0 :result true}} a :PASS.
-{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>}. {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>} log:equalTo {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>}} => {:loges3 :result true}} a :PASS.
+{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>}. {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>} log:notEqualTo {:a :b skolem:e_c_2}} => {:loges3 :result true}} a :PASS.
 {{{:b :a :c. :e :d :f. :h :g :i. :k :j :l} log:includes {:k :j :l. :e :d :f}} => {:logi1 :result true}} a :PASS.
 {{<http://josd.github.io/eye/reasoning/bi/medic.n3> log:semantics {(med:Ann med:Fever) fl:mu 0.8 . (med:Ann med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:AcuteMyocardialInfarction) fl:mu 0.9 . (med:Joe med:ActivePepticUlcerDisease) fl:mu 0.006 . (med:Joe med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:SevereAsthma) fl:mu 0.001 . (med:Joe med:ChronicObstructivePumonaryDisease) fl:mu 0.001 . med:aspirinHighDose med:prescribedFor med:Fever. med:aspirinLowDose med:prescribedFor med:AcuteMyocardialInfarction. med:betaBlocker med:prescribedFor med:AcuteMyocardialInfarction. med:aspirinHighDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinHighDose med:excludedFor med:AllergyForAspirin. med:aspirinLowDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinLowDose med:excludedFor med:AllergyForAspirin. med:betaBlocker med:excludedFor med:SevereAsthma. med:betaBlocker med:excludedFor med:ChronicObstructivePumonaryDisease. {?U_2 med:prescribedFor ?U_3. (?U_4 ?U_3) fl:mu ?U_5. ?U_5 math:greaterThan 0.7 . ?U_6 e:findall (?U_7 {?U_2 med:excludedFor ?U_7} ?U_8). ?U_6 e:findall (?U_7 {?U_2 med:excludedFor ?U_7. (?U_4 ?U_7) fl:mu ?U_9. ?U_9 math:notGreaterThan 0.01} ?U_8)} => {?U_4 med:isPrescribed ?U_2}}. {(med:Ann med:Fever) fl:mu 0.8 . (med:Ann med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:AcuteMyocardialInfarction) fl:mu 0.9 . (med:Joe med:ActivePepticUlcerDisease) fl:mu 0.006 . (med:Joe med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:SevereAsthma) fl:mu 0.001 . (med:Joe med:ChronicObstructivePumonaryDisease) fl:mu 0.001 . med:aspirinHighDose med:prescribedFor med:Fever. med:aspirinLowDose med:prescribedFor med:AcuteMyocardialInfarction. med:betaBlocker med:prescribedFor med:AcuteMyocardialInfarction. med:aspirinHighDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinHighDose med:excludedFor med:AllergyForAspirin. med:aspirinLowDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinLowDose med:excludedFor med:AllergyForAspirin. med:betaBlocker med:excludedFor med:SevereAsthma. med:betaBlocker med:excludedFor med:ChronicObstructivePumonaryDisease. {?U_2 med:prescribedFor ?U_3. (?U_4 ?U_3) fl:mu ?U_5. ?U_5 math:greaterThan 0.7 . ?U_6 e:findall (?U_7 {?U_2 med:excludedFor ?U_7} ?U_8). ?U_6 e:findall (?U_7 {?U_2 med:excludedFor ?U_7. (?U_4 ?U_7) fl:mu ?U_9. ?U_9 math:notGreaterThan 0.01} ?U_8)} => {?U_4 med:isPrescribed ?U_2}} log:includes {med:aspirinHighDose med:excludedFor med:AllergyForAspirin}} => {:logi3 :result true}} a :PASS.
 {{{:a :b :c} log:includes {:a :b :c}} => {:logid0 :result true}} a :PASS.
-{{{:a :b :c} log:includes {:a :b :c}} => {:logid1 :result true}} a :PASS.
-{{{:a :b :_c} log:includes {:a :b :_c}} => {:logid3 :result true}} a :PASS.
 {{<http://josd.github.io/eye/reasoning/bi/abc.n3> log:semantics {:a :b :c}. {:a :b :c} log:includes {:a :b :c}} => {:logis0 :result true}} a :PASS.
-{{<http://josd.github.io/eye/reasoning/bi/abc.n3> log:semantics {:a :b :c}. {:a :b :c} log:includes {:a :b :c}} => {:logis1 :result true}} a :PASS.
-{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>}. {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>} log:includes {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>}} => {:logis3 :result true}} a :PASS.
 {{:a log:notEqualTo :b} => {:logne1 :result true}} a :PASS.
 {{{:a :b :c} log:notEqualTo {:a :b :_c}} => {:logned1 :result true}} a :PASS.
 {{{:a :b :_c} log:notEqualTo {:a :b :c}} => {:logned2 :result true}} a :PASS.
+{{{:a :b :_c} log:notEqualTo {:a :b skolem:e_c_3}} => {:logned3 :result true}} a :PASS.
 {{<http://josd.github.io/eye/reasoning/bi/medic.n3> log:semantics {(med:Ann med:Fever) fl:mu 0.8 . (med:Ann med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:AcuteMyocardialInfarction) fl:mu 0.9 . (med:Joe med:ActivePepticUlcerDisease) fl:mu 0.006 . (med:Joe med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:SevereAsthma) fl:mu 0.001 . (med:Joe med:ChronicObstructivePumonaryDisease) fl:mu 0.001 . med:aspirinHighDose med:prescribedFor med:Fever. med:aspirinLowDose med:prescribedFor med:AcuteMyocardialInfarction. med:betaBlocker med:prescribedFor med:AcuteMyocardialInfarction. med:aspirinHighDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinHighDose med:excludedFor med:AllergyForAspirin. med:aspirinLowDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinLowDose med:excludedFor med:AllergyForAspirin. med:betaBlocker med:excludedFor med:SevereAsthma. med:betaBlocker med:excludedFor med:ChronicObstructivePumonaryDisease. {?U_10 med:prescribedFor ?U_11. (?U_12 ?U_11) fl:mu ?U_13. ?U_13 math:greaterThan 0.7 . ?U_14 e:findall (?U_15 {?U_10 med:excludedFor ?U_15} ?U_16). ?U_14 e:findall (?U_15 {?U_10 med:excludedFor ?U_15. (?U_12 ?U_15) fl:mu ?U_17. ?U_17 math:notGreaterThan 0.01} ?U_16)} => {?U_12 med:isPrescribed ?U_10}}. {(med:Ann med:Fever) fl:mu 0.8 . (med:Ann med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:AcuteMyocardialInfarction) fl:mu 0.9 . (med:Joe med:ActivePepticUlcerDisease) fl:mu 0.006 . (med:Joe med:AllergyForAspirin) fl:mu 0.001 . (med:Joe med:SevereAsthma) fl:mu 0.001 . (med:Joe med:ChronicObstructivePumonaryDisease) fl:mu 0.001 . med:aspirinHighDose med:prescribedFor med:Fever. med:aspirinLowDose med:prescribedFor med:AcuteMyocardialInfarction. med:betaBlocker med:prescribedFor med:AcuteMyocardialInfarction. med:aspirinHighDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinHighDose med:excludedFor med:AllergyForAspirin. med:aspirinLowDose med:excludedFor med:ActivePepticUlcerDisease. med:aspirinLowDose med:excludedFor med:AllergyForAspirin. med:betaBlocker med:excludedFor med:SevereAsthma. med:betaBlocker med:excludedFor med:ChronicObstructivePumonaryDisease. {?U_10 med:prescribedFor ?U_11. (?U_12 ?U_11) fl:mu ?U_13. ?U_13 math:greaterThan 0.7 . ?U_14 e:findall (?U_15 {?U_10 med:excludedFor ?U_15} ?U_16). ?U_14 e:findall (?U_15 {?U_10 med:excludedFor ?U_15. (?U_12 ?U_15) fl:mu ?U_17. ?U_17 math:notGreaterThan 0.01} ?U_16)} => {?U_12 med:isPrescribed ?U_10}} log:notIncludes {med:aspirinLowDose med:excludedFor med:SevereAsthma}} => {:logni3 :result true}} a :PASS.
+{{{:a :b :c} log:notIncludes {:a :b skolem:e_c_4}} => {:lognid1 :result true}} a :PASS.
 {{{:a :b :_c} log:notIncludes {:a :b :c}} => {:lognid2 :result true}} a :PASS.
-{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>}. {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>} log:notIncludes {:a :b :c}} => {:lognis2 :result true}} a :PASS.
-{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>}. <http://josd.github.io/eye/reasoning/bi/abc.n3> log:semantics {:a :b :c}. {:a :b <http://josd.github.io/.well-known/genid/XCPo7extBQ3RUYoEARJWUUGpp3Q#e_c_2>} log:notIncludes {:a :b :c}} => {:lognis4 :result true}} a :PASS.
+{{{:a :b :_c} log:notIncludes {:a :b skolem:e_c_5}} => {:lognid3 :result true}} a :PASS.
+{{<http://josd.github.io/eye/reasoning/bi/abc.n3> log:semantics {:a :b :c}. {:a :b :c} log:notIncludes {:a :b skolem:e_c_6}} => {:lognis1 :result true}} a :PASS.
+{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>}. {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>} log:notIncludes {:a :b :c}} => {:lognis2 :result true}} a :PASS.
+{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>}. {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>} log:notIncludes {:a :b skolem:e_c_7}} => {:lognis3 :result true}} a :PASS.
+{{<http://josd.github.io/eye/reasoning/bi/ab_c.n3> log:semantics {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>}. <http://josd.github.io/eye/reasoning/bi/abc.n3> log:semantics {:a :b :c}. {:a :b <http://josd.github.io/.well-known/genid/I7maIXwjHmWIWxqzeboZbYtIlmQ#e_c_8>} log:notIncludes {:a :b :c}} => {:lognis4 :result true}} a :PASS.
 {{med:Fever log:uri "http://eulersharp.sourceforge.net/2006/02swap/med#Fever"} => {:logu1 :result true}} a :PASS.
 {{:betaBlocker log:uri "http://eulersharp.sourceforge.net/2007/07test#betaBlocker"} => {:logu2 :result true}} a :PASS.
 {{(1 1) math:difference 0} => {:mathd1 :result true}} a :PASS.

diff --git a/reasoning/bi/biP.n3 b/reasoning/bi/biP.n3
@@ -54,7 +54,7 @@ PREFIX : <http://eulersharp.sourceforge.net/2007/07test#>
 {?SCOPE e:fail {(1 2 3 4 5) e:subsequence (4 2 1)}} => {:esl2 :result true}.
 {() e:subsequence ()} => {:esl3 :result true}.
 {((0 1) (2 3) (4 5)) e:transpose ((0 2 4) (1 3 5))} => {:et1 :result true}.
-{:a :b _:c. _:c e:whenGround {:a :b :d}} => {:ewg1 :result true}.
+{_:c e:whenGround {:a :b :d}. :a :b _:c} => {:ewg1 :result true}.
 {"http://www.agfa.com/w3c/euler" e:wwwFormEncode "http%3a%2f%2fwww.agfa.com%2fw3c%2feuler"} => {:ew1 :result true}.
 {"Hello World!" e:wwwFormEncode "Hello+World%21"} => {:ew2 :result true}.
 
@@ -71,24 +71,24 @@ PREFIX : <http://eulersharp.sourceforge.net/2007/07test#>
 {({} {:u :v :w} {:x :y :z. :j :k :l}) log:conjunction {:u :v :w. :x :y :z. :j :k :l}} => {:logc2 :result true}.
 {({} {:u :v :w} {} {}) log:conjunction {:u :v :w}} => {:logc3 :result true}.
 {(:a ?A) log:equalTo (?B :b)} => {:loge1 :result true}.
-{{:a :b :c} log:equalTo {:a :b :c}} => {:loge2 :result true}.
-{{:a :b :_c} log:equalTo {:a :b _:c}} => {:loge3 :result true}.
+{{:a :b :c} log:equalTo {:a :b :c}} => {:logee1 :result true}.
 {<abc.n3> log:semantics ?X. ?X log:equalTo {:a :b :c}} => {:loges0 :result true}.
-{<ab_c.n3> log:semantics ?X. ?X log:equalTo {:a :b _:c}} => {:loges3 :result true}.
+{<ab_c.n3> log:semantics ?X. ?X log:notEqualTo {:a :b _:c}} => {:loges3 :result true}.
 {{:b :a :c. :e :d :f. :h :g :i. :k :j :l} log:includes {:k :j :l. ?X :d ?Z}} => {:logi1 :result true}.
 {<medic.n3> log:semantics ?F. ?F log:includes {med:aspirinHighDose med:excludedFor med:AllergyForAspirin}} => {:logi3 :result true}.
 {{:a :b :c} log:includes {:a :b :c}} => {:logid0 :result true}.
-{{:a :b :c} log:includes {:a :b _:c}} => {:logid1 :result true}.
-{{:a :b :_c} log:includes {:a :b _:c}} => {:logid3 :result true}.
 {<abc.n3> log:semantics ?X. ?X log:includes {:a :b :c}} => {:logis0 :result true}.
-{<abc.n3> log:semantics ?X. ?X log:includes {:a :b _:c}} => {:logis1 :result true}.
-{<ab_c.n3> log:semantics ?X. ?X log:includes {:a :b _:c}} => {:logis3 :result true}.
 {:a log:notEqualTo :b} => {:logne1 :result true}.
 {{:a :b :c} log:notEqualTo {:a :b :_c}} => {:logned1 :result true}.
 {{:a :b :_c} log:notEqualTo {:a :b :c}} => {:logned2 :result true}.
+{{:a :b :_c} log:notEqualTo {:a :b _:c}} => {:logned3 :result true}.
 {<medic.n3> log:semantics ?F. ?F log:notIncludes {med:aspirinLowDose med:excludedFor med:SevereAsthma}} => {:logni3 :result true}.
+{{:a :b :c} log:notIncludes {:a :b _:c}} => {:lognid1 :result true}.
 {{:a :b :_c} log:notIncludes {:a :b :c}} => {:lognid2 :result true}.
+{{:a :b :_c} log:notIncludes {:a :b _:c}} => {:lognid3 :result true}.
+{<abc.n3> log:semantics ?X. ?X log:notIncludes {:a :b _:c}} => {:lognis1 :result true}.
 {<ab_c.n3> log:semantics ?X. ?X log:notIncludes {:a :b :c}} => {:lognis2 :result true}.
+{<ab_c.n3> log:semantics ?X. ?X log:notIncludes {:a :b _:c}} => {:lognis3 :result true}.
 {<ab_c.n3> log:semantics ?X. <abc.n3> log:semantics ?Y. ?X log:notIncludes ?Y} => {:lognis4 :result true}.
 {<http://eulersharp.sourceforge.net/2006/02swap/med#Fever> log:uri "http://eulersharp.sourceforge.net/2006/02swap/med#Fever"} => {:logu1 :result true}.
 {:betaBlocker log:uri "http://eulersharp.sourceforge.net/2007/07test#betaBlocker"} => {:logu2 :result true}.

diff --git a/reasoning/bmi/bmi_proof.n3 b/reasoning/bmi/bmi_proof.n3
@@ -21,6 +21,7 @@ PREFIX func: <http://www.w3.org/2007/rif-builtin-function#>
 PREFIX schema: <http://schema.org/>
 PREFIX fos: <http://eulersharp.sourceforge.net/2003/03swap/foster#>
 PREFIX r: <http://www.w3.org/2000/10/swap/reason#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/7KYWBjJueXqIqK:J2V_3kOjWJuE#>
 
 [] a r:Proof, r:Conjunction;
   r:component <#lemma1>;

diff --git a/reasoning/bnode/example1-pass-all.n3 b/reasoning/bnode/example1-pass-all.n3
@@ -1,5 +1,6 @@
 PREFIX : <https://example.org/ns/example#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/fq_GYeK2wHkFVhh2:VnPzGYTI9Y#>
 
-:alice :believes {_:bn_1 a :Unicorn}.
-_:bn_2 a :Person.
+:alice :believes {skolem:bn_1 a :Unicorn}.
+skolem:bn_2 a :Person.
 
diff --git a/reasoning/bnode/example2-pass-all.n3 b/reasoning/bnode/example2-pass-all.n3
@@ -1,4 +1,5 @@
 PREFIX : <https://example.org/ns/example#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/x6t7u:Mx0tnG4ziiLhBu82qu05Q#>
 
 {?U_0 a :Unicorn} => {:world a :MagicalPlace}.
 
diff --git a/reasoning/bnode/example3-pass-all.n3 b/reasoning/bnode/example3-pass-all.n3
@@ -1,4 +1,5 @@
 PREFIX : <https://example.org/ns/example#>
+PREFIX skolem: <http://josd.github.io/.well-known/genid/pXFpsre:KyMTrZJoLsDrzCW8QfE#>
 
 {?U_0 a :Person} => {?U_0 :mother _:sk_1}.