using explicit rule:vars in rdfreasoning

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v8.6.19 (2023-11-24) using explicit rule:vars in rdfreasoning
 v8.6.18 (2023-11-23) using log:negativeTriple as backward chaining hint
 v8.6.17 (2023-11-22) expressing blogic in RDF and running with rdfreasoning
 v8.6.16 (2023-11-21) fixing rdfreasoning for variable conclusions

VERSION

@@ -1 +1 @@
-8.6.18
+8.6.19

eye.pl

@@ -21,7 +21,7 @@
 :- use_module(library(pcre)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v8.6.18 (2023-11-23)').
+version_info('EYE v8.6.19 (2023-11-24)').
 
 license_info('MIT License
 
@@ -639,21 +639,23 @@
     % forward rule
     assertz(implies((
             '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(R, '<http://eyereasoner.github.io/rule#ForwardRule>'),
+            '<http://eyereasoner.github.io/rule#vars>'(R, U),
+            getlist(U, V),
             '<http://eyereasoner.github.io/rule#premise>'(R, K),
             getconj(K, A),
             '<http://eyereasoner.github.io/rule#conclusion>'(R, H),
             getconj(H, B),
-            findvars([A, B], V, beta),
             makevars([A, B], [Q, I], beta(V))
             ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
     % backward rule
     assertz(implies((
             '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(R, '<http://eyereasoner.github.io/rule#BackwardRule>'),
+            '<http://eyereasoner.github.io/rule#vars>'(R, U),
+            getlist(U, V),
             '<http://eyereasoner.github.io/rule#premise>'(R, K),
             getconj(K, A),
             '<http://eyereasoner.github.io/rule#conclusion>'(R, [[S, P, O]]),
             B =.. [P, S, O],
-            findvars([A, B], V, beta),
             makevars(':-'(B, A), C, beta(V)),
             copy_term_nat(C, CC),
             labelvars(CC, 0, _, avar),
@@ -666,12 +668,13 @@
     % query rule
     assertz(implies((
             '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(R, '<http://eyereasoner.github.io/rule#QueryRule>'),
+            '<http://eyereasoner.github.io/rule#vars>'(R, U),
+            getlist(U, V),
             '<http://eyereasoner.github.io/rule#premise>'(R, K),
             getconj(K, A),
             '<http://eyereasoner.github.io/rule#conclusion>'(R, H),
             getconj(H, B),
             djiti_answer(answer(B), J),
-            findvars([A, J], V, beta),
             makevars(implies(A, J, '<>'), C, beta(V)),
             copy_term_nat(C, CC),
             labelvars(CC, 0, _, avar),

rdfreasoning/acp/acp.ttl

@@ -15,6 +15,12 @@
     :noneOf :D.
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:Pol
+        _:Test
+        _:Field
+        _:X
+    );
     rule:conclusion (
         (_:Pol :pass :allOfTest)
     );
@@ -25,7 +31,14 @@
     ).
 
 [] a rule:BackwardRule;
-    rule:conclusion (
+    rule:vars (
+        _:Pol
+        _:Test
+        _:Field
+        _:List
+        _:X
+        _:L
+    );rule:conclusion (
         (_:Pol :pass :anyOfTest)
     );
     rule:premise (
@@ -37,6 +50,14 @@
     ).
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:Pol
+        _:Test
+        _:Field
+        _:List
+        _:X
+        _:L
+    );
     rule:conclusion (
         (_:Pol :pass :noneOfTest)
     );
@@ -49,6 +70,9 @@
     ).
 
 [] a rule:QueryRule;
+    rule:vars (
+        _:Pol
+    );
     rule:premise (
         (_:Pol rdf:type :Policy)
         (_:Pol :pass :allOfTest)

rdfreasoning/complex-numbers/out/complex-numbers.ttl.out

@@ -1,8 +0,0 @@
-@prefix complex: <http://eyereasoner.github.io/complex#>.
-
-((-1 0) (0.5 0)) complex:exponentiation (6.123233995736766e-17 1.0).
-((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation (-1.0 1.2246467991473532e-16).
-((0 1) (0 1)) complex:exponentiation (0.20787957635076193 0.0).
-((2.718281828459045 0) (-1.57079632679 0)) complex:exponentiation (0.20787957635177984 0.0).
-(2 0) complex:asin (1.5707963267948966 1.3169578969248166).
-(2 0) complex:acos (0.0 -1.3169578969248166).

rdfreasoning/fibonacci/out/fibonacci.ttl.out

@@ -1,8 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-0 :fibonacci 0 .
-1 :fibonacci 1 .
-6 :fibonacci 8 .
-91 :fibonacci 4660046610375530309 .
-283 :fibonacci 62232491515607091882574410635924603070626544377175485625797 .
-3674 :fibonacci 295872959797101479478634366815157108100573212705250690577871041398423606408217262643449728342664061812585639168722421830407677671667740585806703531229882783069925750619720511808616484846128237251921414441458265138672827487722512845223115526738192067144721087756159352711138340620702266509343657403678256247195010013499661223527119909308682062873140767135468966093474944529418214755911968500799987099146489838560114063096775586903976827512299123202488315139397181279903459556726060805948910609527571241968534269554079076649680403030083743420820438603816095671532163428933363322524736324029745871445486444623006627119156710782085648303485296149604974010598940800770684835758031137479033374229914629583184427269638360355586190323578625395157899987377625662075558684705457 .

rdfreasoning/gps/out/gps.ttl.out

@@ -1,5 +0,0 @@
-@prefix : <http://example.org/ns#>.
-@prefix gps: <http://eyereasoner.github.io/eye/reasoning/gps/gps-schema#>.
-
-:i1 gps:path ((:drive_gent_brugge :drive_brugge_oostende) 2400.0 0.01 0.9408 0.99).
-:i1 gps:path ((:drive_gent_kortrijk :drive_kortrijk_brugge :drive_brugge_oostende) 4100.0 0.018000000000000002 0.903168 0.9801).

rdfreasoning/graph/graph.ttl

@@ -15,6 +15,10 @@
 
 # oneway subproperty of path
 [] a rule:ForwardRule;
+    rule:vars (
+        _:A
+        _:B
+    );
     rule:premise (
         (_:A :oneway _:B)
     );
@@ -24,6 +28,11 @@
 
 # path transitive property
 [] a rule:ForwardRule;
+    rule:vars (
+        _:A
+        _:B
+        _:C
+    );
     rule:premise (
         (_:A :path _:B)
         (_:B :path _:C)
@@ -34,6 +43,9 @@
 
 # query
 [] a rule:QueryRule;
+    rule:vars (
+        _:A
+    );
     rule:premise (
         (_:A :path :nantes)
     );

rdfreasoning/hanoi/hanoi.ttl

@@ -5,6 +5,16 @@
 
 # _:M is the sequence of moves to move _:N disks from _:X to _:Y using _:Z as intermediary
 [] a rule:BackwardRule;
+    rule:vars (
+        _:N
+        _:X
+        _:Y
+        _:Z
+        _:M
+        _:N1
+        _:M1
+        _:M2
+    );
     rule:conclusion (
         ((_:N _:X _:Y _:Z) :moves _:M)
     );
@@ -17,12 +27,20 @@
     ).
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:X
+        _:Y
+        _:Z
+    );
     rule:conclusion (
         ((1 _:X _:Y _:Z) :moves ((_:X _:Y)))
     );
     rule:premise ().
 
 [] a rule:QueryRule;
+    rule:vars (
+        _:M
+    );
     rule:premise (
         ((9 :left :right :center) :moves _:M)
     );

rdfreasoning/negation-predicates/negation-predicates.ttl

@@ -3,6 +3,9 @@
 
 # saying A means saying C
 [] a rule:ForwardRule;
+    rule:vars (
+        _:S
+    );
     rule:premise (
         (_:S :saying :A)
     );
@@ -11,6 +14,9 @@
     ).
 
 [] a rule:ForwardRule;
+    rule:vars (
+        _:S
+    );
     rule:premise (
         (_:S :not_saying :C)
     );
@@ -20,6 +26,9 @@
 
 # saying B means saying C
 [] a rule:ForwardRule;
+    rule:vars (
+        _:S
+    );
     rule:premise (
         (_:S :saying :B)
     );
@@ -37,6 +46,9 @@
 
 # saying A or saying B
 [] a rule:ForwardRule;
+    rule:vars (
+        _:S
+    );
     rule:premise (
         (_:S :not_saying :A)
     );
@@ -45,6 +57,9 @@
     ).
 
 [] a rule:ForwardRule;
+    rule:vars (
+        _:S
+    );
     rule:premise (
         (_:S :not_saying :B)
     );
@@ -58,6 +73,7 @@
 
 # query
 [] a rule:QueryRule;
+    rule:vars ();
     rule:premise (
         (:alice :saying :C)
     );

rdfreasoning/peano/peano.ttl

@@ -3,12 +3,20 @@
 
 # add
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+    );
     rule:conclusion (
         ((_:A 0) :add _:A)
     );
     rule:premise ().
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+        _:B
+        _:C
+    );
     rule:premise (
         ((_:A _:B) :add _:C)
     );
@@ -18,12 +26,21 @@
 
 # multiply
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+    );
     rule:conclusion (
         ((_:A 0) :multiply 0)
     );
     rule:premise ().
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+        _:B
+        _:C
+        _:D
+    );
     rule:conclusion (
         ((_:A (:s _:B)) :multiply _:C)
     );
@@ -34,6 +51,10 @@
 
 # factorial
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+        _:B
+    );
     rule:conclusion (
         (_:A :factorial _:B)
     );
@@ -42,12 +63,21 @@
     ).
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+    );
     rule:conclusion (
         ((0 _:A) :fac _:A)
     );
     rule:premise ().
 
 [] a rule:BackwardRule;
+    rule:vars (
+        _:A
+        _:B
+        _:C
+        _:D
+    );
     rule:conclusion (
         (((:s _:A) _:B) :fac _:C)
     );
@@ -58,6 +88,11 @@
 
 # query
 [] a rule:QueryRule;
+    rule:vars (
+        _:A
+        _:B
+        _:C
+    );
     rule:premise (
         (((:s 0) (:s (:s 0))) :add _:A)
         ((_:A (:s (:s 0))) :multiply _:B)

rdfreasoning/pi/out/pi.ttl.out

@@ -1,3 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-(50000 3.141592653589793) :pi true.

rdfreasoning/sdcoding/out/sdcoding.ttl.out

@@ -1,6 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-0 :sdcoding 0 .
-1 :sdcoding 1 .
-2 :sdcoding 2 .
-3 :sdcoding 3 .

rdfreasoning/socrates/out/socrates.ttl.out

@@ -1,3 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-:Socrates a :Mortal.

rdfreasoning/temp/out/append.ttl.out

@@ -1,16 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-((
-    (:A :B :C)
-    (:A :X :C)
-    (:D :E :F)
-) (
-    (:A :Y :C)
-    (:A :B :C)
-)) :append (
-    (:A :B :C)
-    (:A :X :C)
-    (:D :E :F)
-    (:A :Y :C)
-    (:A :B :C)
-).

rdfreasoning/temp/out/lott.ttl.out

@@ -1,3 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-:Socrates a :Mortal.

rdfreasoning/temp/out/sha512.ttl.out

@@ -1,3 +0,0 @@
-@prefix : <http://example.org/ns#>.
-
-"hello world" :sha512 "309ecc489c12d6eb4cc40f50c902f2b4d0ed77ee511a7c7a9bcd3ca86d4cd86f989dd35bc5ff499670da34255b45b0cfd830e81f605dcf7dc5542e93ae9cd76f".

rdfreasoning/temp/out/socrates-contradiction.ttl.out

@@ -1,4 +0,0 @@
-** ERROR ** eam ** inference_fuse((
-    (:Socrates a :Mortal)
-    (:Socrates a :Immortal)
-) => false)