running cases in reasoning/gsm

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v10.24.5 (2024-09-30) running cases in reasoning/gsm
 v10.24.4 (2024-09-30) fixing trig output with rdf:value
 v10.24.3 (2024-09-29) fixing graph:statement built-in to unify and generate TriG graph statements
 v10.24.2 (2024-09-29) using graph:statement instead of graph:namedGraph

VERSION

@@ -1 +1 @@
-10.24.4
+10.24.5

eye.pl

@@ -22,7 +22,7 @@
 :- catch(use_module(library(process)), _, true).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v10.24.4 (2024-09-30)').
+version_info('EYE v10.24.5 (2024-09-30)').
 
 license_info('MIT License
 
@@ -3984,6 +3984,7 @@
             )
         ->  (   (   sub_atom(Y, 0, 2, _, 'e_')
                 ;   sub_atom(Y, 0, 3, _, 'bn_')
+                ;   sub_atom(Y, 0, 5, _, 'node_')
                 )
             ->  write('_:')
             ;   sub_atom(Y, 0, 2, _, Z),
@@ -5349,6 +5350,40 @@
             assertz(graph(G, F)),
             fail
         ;   true
+        ),
+
+        % create types
+        (   '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(X, Y),
+            ground([X, Y]),
+            getterm(X, Z),
+            (   Z = X
+            ->  true
+            ;   retract('<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(X, Y)),
+                assertz('<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(Z, Y))
+            ),
+            fail
+        ;   true
+        ),
+
+        % create terms
+        (   pred(P),
+            P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#first>',
+            P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#reifies>',
+            P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#rest>',
+            P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>',
+            P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#value>',
+            P \= quad,
+            X =.. [P, _, _],
+            call(X),
+            ground(X),
+            getterm(X, Y),
+            (   Y = X
+            ->  true
+            ;   retract(X),
+                assertz(Y)
+            ),
+            fail
+        ;   true
         )
     ;   forall(
             retract('<http://www.w3.org/2000/10/swap/log#isImpliedBy>'(A, B)),
@@ -12457,7 +12492,7 @@
     !,
     (   sub_atom(A, _, 19, _, '/.well-known/genid/'),
         (   sub_atom(A, _, 4, _, '#bn_')
-        ;   sub_atom(A, _, 4, _, '#e_')
+        ;   sub_atom(A, _, 3, _, '#e_')
         )
     ;   sub_atom(A, 0, _, _, some)
     ;   atom_concat('<http://www.w3.org/2000/10/swap/var#', _, A)

reasoning/gsm/ackermann.trig

@@ -0,0 +1,118 @@
+# ------------------
+# Ackermann function
+# ------------------
+#
+# The Ackermann function, holds paramount significance in theoretical
+# computer science and computability theory. Formulated by Wilhelm
+# Ackermann, it stands as a fundamental example illustrating functions
+# that transcend primitive recursion, showcasing the existence of
+# computable problems that defy conventional algorithmic approaches.
+# Its rapid growth, even for small inputs, makes it a powerful tool in
+# complexity theory, establishing lower bounds on computational
+# complexity and emphasizing the inherent challenges in designing
+# efficient algorithms for certain problems. The Ackermann function’s
+# prominence extends to symbolize the limits of computability, playing
+# a crucial role in delineating what can and cannot be algorithmically
+# computed within the theoretical realms of computer science.
+#
+# One can see the rapid growth in
+# https://github.com/eyereasoner/eye/blob/master/reasoning/ackermann/ackermann-answer.n3
+# where A(4,0) has a value of 2 digits, A(4,1) has a value of 5 digits
+# and A(4,2) has a value of 19729 digits.
+
+@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
+@prefix math: <http://www.w3.org/2000/10/swap/math#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+@prefix : <#>.
+
+# ackermann(x, y)
+_:bng_1 log:isImpliedBy _:bng_2.
+
+_:bng_1 {
+    (var:X var:Y) :ackermann var:A.
+}
+
+_:bng_2 {
+    (var:Y 3) math:sum var:B.
+    (var:X var:B 2) :ackermann var:C.
+    (var:C 3) math:difference var:A.
+}
+
+# ackermann(x, y, z)
+# succ (x=0)
+_:bng_3 log:isImpliedBy _:bng_4.
+
+_:bng_3 {
+    (0 var:Y var:Z) :ackermann var:A.
+}
+
+_:bng_4 {
+    [] rdf:value true; log:callWithCut true.
+    (var:Y 1) math:sum var:A.
+}
+
+# sum (x=1)
+_:bng_5 log:isImpliedBy _:bng_6.
+
+_:bng_5 {
+    (1 var:Y var:Z) :ackermann var:A.
+}
+
+_:bng_6 {
+    [] rdf:value true; log:callWithCut true.
+    (var:Y var:Z) math:sum var:A.
+}
+
+# product (x=2)
+_:bng_7 log:isImpliedBy _:bng_8.
+
+_:bng_7 {
+    (2 var:Y var:Z) :ackermann var:A.
+}
+
+_:bng_8 {
+    [] rdf:value true; log:callWithCut true.
+    (var:Y var:Z) math:product var:A.
+}
+
+# exponentiation (x=3), tetration (x=4), pentation (x=5), hexation (x=6), etc
+_:bng_9 log:isImpliedBy _:bng_10.
+
+_:bng_9 {
+    (var:X 0 var:Z) :ackermann 1.
+}
+
+_:bng_10 {
+    [] rdf:value true; log:callWithCut true.
+}
+
+_:bng_11 log:isImpliedBy _:bng_12.
+
+_:bng_11 {
+    (var:X var:Y var:Z) :ackermann var:A.
+}
+
+_:bng_12 {
+    (var:Y 1) math:difference var:B.
+    (var:X var:B var:Z) :ackermann var:C.
+    (var:X 1) math:difference var:D.
+    (var:D var:C var:Z) :ackermann var:A.
+}
+
+# query
+_:bng_14 log:query _:bng_14.
+
+_:bng_14 {
+    (0 0) :ackermann var:A0.
+    (0 6) :ackermann var:A1.
+    (1 2) :ackermann var:A2.
+    (1 7) :ackermann var:A3.
+    (2 2) :ackermann var:A4.
+    (2 9) :ackermann var:A5.
+    (3 4) :ackermann var:A6.
+    (3 14) :ackermann var:A7.
+    (4 0) :ackermann var:A8.
+    (4 1) :ackermann var:A9.
+    (4 2) :ackermann var:A10.
+}

reasoning/gsm/acp.trig

@@ -0,0 +1,89 @@
+# -----------------------------
+# Access control policy example
+# -----------------------------
+
+@prefix list: <http://www.w3.org/2000/10/swap/list#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+@prefix : <#>.
+
+:test1 :policy :PolicyX;
+    :has :A, :B, :C.
+
+:PolicyX a :Policy;
+    :allOf :A, :B;
+    :anyOf :C;
+    :noneOf :D.
+
+_:bng_1 log:isImpliedBy _:bng_2.
+
+_:bng_1 {
+    var:Pol :pass :allOfTest.
+}
+
+_:bng_2 {
+    var:Test :policy var:Pol.
+    var:Pol a :Policy.
+    (_:bng_3 _:bng_4) log:forAllIn var:X.
+}
+
+_:bng_3 {
+    var:Pol :allOf var:Field.
+}
+
+_:bng_4 {
+    var:Test :has var:Field.
+}
+
+_:bng_5 log:isImpliedBy _:bng_6.
+
+_:bng_5 {
+    var:Pol :pass :anyOfTest.
+}
+
+_:bng_6 {
+    var:Test :policy var:Pol.
+    var:Pol a :Policy.
+    (var:Field _:bng_7 var:List) log:collectAllIn var:X.
+    var:List list:length var:L.
+    (var:L) log:notEqualTo (0).
+}
+
+_:bng_7 {
+    var:Pol :anyOf var:Field.
+    var:Test :has var:Field.
+}
+
+_:bng_8 log:isImpliedBy _:bng_9.
+
+_:bng_8 {
+    var:Pol :pass :noneOfTest.
+}
+
+_:bng_9 {
+    var:Test :policy var:Pol.
+    var:Pol a :Policy.
+    (var:Field _:bng_10 var:List) log:collectAllIn var:X.
+    var:List list:length var:L.
+    (var:L) log:equalTo (0).
+}
+
+_:bng_10 {
+    var:Pol :noneOf var:Field.
+    var:Test :has var:Field.
+}
+
+# query
+_:bng_11 log:query _:bng_12.
+
+_:bng_11 {
+    var:Pol a :Policy.
+    var:Pol :pass :allOfTest.
+    var:Pol :pass :anyOfTest.
+    var:Pol :pass :noneOfTest.
+}
+
+_:bng_12 {
+    :test :for var:Pol.
+    :test :is true.
+}

reasoning/gsm/cobbler.trig

@@ -0,0 +1,20 @@
+# ------------
+# Good Cobbler
+# ------------
+#
+# Example from https://shs.hal.science/halshs-04148373/document
+# Using functional logic http://intrologic.stanford.edu/chapters/chapter_11.html
+
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+@prefix : <#>.
+
+# some x is a good cobbler
+_:x :is (:good :Cobbler).
+
+# is there some x which is good at some y
+_:bng_1 log:query _:bng_1.
+
+_:bng_1 {
+    var:x :is (:good var:y).
+}