fixing negative surfaces to backward rules

eyereasoner · Mar 29, 2024 · 3904b9b · 3904b9b
1 parent 7289a4e
commit 3904b9b
Show file tree

Hide file tree

Showing 6 changed files with 116 additions and 4 deletions.
diff --git a/RELEASE b/RELEASE
@@ -1,5 +1,6 @@
                                   EYE release
 
+v10.0.2 (2024-03-29) fixing negative surfaces to backward rules
 v10.0.1 (2024-03-29) fixing --pass-all and --pass-all-ground
 v10.0.0 (2024-03-28) supporting RDF Surfaces, RDF N-Quads and RDF TriG with global scope for blank nodes
 v9.11.4 (2024-03-04) adding log:query built-in and tested with (un)named graphs

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-10.0.1
+10.0.2
diff --git a/eye.pl b/eye.pl
@@ -21,7 +21,7 @@
 :- use_module(library(pcre)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v10.0.1 (2024-03-29)').
+version_info('EYE v10.0.2 (2024-03-29)').
 
 license_info('MIT License
 
@@ -468,6 +468,7 @@
             is_graph(G),
             conj_list(G, L),
             list_to_set(L, B),
+            \+member('<http://www.w3.org/2000/10/swap/log#nand>'(_, triple(_, _, _)), B),
             findall(1,
                 (   member('<http://www.w3.org/2000/10/swap/log#nand>'(_, _), B)
                 ),
@@ -482,6 +483,7 @@
             is_graph(F),
             conj_list(F, K),
             list_to_set(K, N),
+            \+member('<http://www.w3.org/2000/10/swap/log#nand>'(_, triple(_, _, _)), N),
             length(N, 2),
             makevars(N, J, beta(Wl)),
             select('<http://www.w3.org/2000/10/swap/log#nand>'(U, C), J, [P]),
@@ -510,8 +512,11 @@
             conj_list(G, L),
             list_to_set(L, B),
             select('<http://www.w3.org/2000/10/swap/log#nand>'(_, H), B, K),
+            H \= triple(_, _, _),
             conj_list(R, K),
-            makevars([R, H], [Q, S], beta(Vl)),
+            find_graffiti(K, D),
+            append(Vl, D, U),
+            makevars([R, H], [Q, S], beta(U)),
             findvars(S, W, beta),
             makevars(S, I, beta(W))
             ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
@@ -523,6 +528,7 @@
             is_graph(G),
             conj_list(G, L),
             list_to_set(L, B),
+            \+member('<http://www.w3.org/2000/10/swap/log#nand>'(_, _), B),
             \+member(exopred(_, _, _), B),
             (   length(B, O),
                 O =< 2
@@ -539,10 +545,35 @@
                 Z
             ),
             E = '<http://www.w3.org/2000/10/swap/log#nand>'(Z, T),
-            makevars([R, E], [Q, S], beta(Vl)),
+            find_graffiti([R], D),
+            append(Vl, D, U),
+            makevars([R, E], [Q, S], beta(U)),
             findvars(S, W, beta),
             makevars(S, I, beta(W))
             ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
+    % convert negative surfaces to backward rule
+    assertz(implies((
+            '<http://www.w3.org/2000/10/swap/log#nand>'(V, G),
+            getlist(V, Vl),
+            is_list(Vl),
+            is_graph(G),
+            conj_list(G, L),
+            list_to_set(L, B),
+            select('<http://www.w3.org/2000/10/swap/log#nand>'(_, triple(Hs, Hp, Ho)), B, K),
+            Tt =.. [Hp, Hs, Ho],
+            conj_list(R, K),
+            conjify(R, S),
+            find_graffiti([R], D),
+            append(Vl, D, U),
+            makevars(':-'(Tt, S), C, beta(U)),
+            copy_term_nat(C, CC),
+            labelvars(CC, 0, _, avar),
+            (   \+cc(CC)
+            ->  assertz(cc(CC)),
+                assertz(C),
+                retractall(brake)
+            ;   true
+            )), true, '<>')),
     % convert negative surfaces to universal statements
     assertz(implies((
             '<http://www.w3.org/2000/10/swap/log#nand>'(V, G),
@@ -577,6 +608,7 @@
                 is_list(Vl),
                 is_graph(G),
                 conj_list(G, L),
+                \+member('<http://www.w3.org/2000/10/swap/log#nand>'(_, triple(_, _, _)), L),
                 makevars(G, H, beta(Vl)),
                 (   H = '<http://www.w3.org/2000/10/swap/log#nand>'(_, false),
                     J = true
@@ -11874,6 +11906,30 @@
 findvar(A, eta) :-
     sub_atom(A, 0, _, _, allv).
 
+find_graffiti(A, []) :-
+    atomic(A),
+    !.
+find_graffiti([], []) :-
+    !.
+find_graffiti([A|B], C) :-
+    !,
+    find_graffiti(A, D),
+    find_graffiti(B, E),
+    append(D, E, C).
+find_graffiti(A, B) :-
+    A =.. [C, D, E],
+    regex('^<.*#on.*Surface>$', C, _),
+    is_list(D),
+    is_graph(E),
+    !,
+    find_graffiti(E, F),
+    findvars(E, G, beta),
+    intersection(D, G, H),
+    append(H, F, B).
+find_graffiti(A, B) :-
+    A =.. C,
+    find_graffiti(C, B).
+
 raw_type(A, '<http://www.w3.org/2000/10/swap/log#ForAll>') :-
     var(A),
     !.

diff --git a/eye.zip b/eye.zip
diff --git a/reasoning/rdfsurfaces/fibonacci.n3 b/reasoning/rdfsurfaces/fibonacci.n3
@@ -0,0 +1,47 @@
+# -----------------
+# Fibonacci numbers
+# -----------------
+#
+# See https://en.wikipedia.org/wiki/Fibonacci_number
+
+@prefix math: <http://www.w3.org/2000/10/swap/math#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <#>.
+
+(_:X _:Y) log:nand {
+    () log:nand <<_:X :fibonacci _:Y>>.
+    (_:X 0 1) :fib _:Y.
+}.
+
+(_:A _:B) log:nand {
+    () log:nand <<(0 _:A _:B) :fib _:A>>.
+}.
+
+(_:A _:B) log:nand {
+    () log:nand <<(1 _:A _:B) :fib _:B>>.
+}.
+
+(_:A _:B _:C _:D _:X _:Y) log:nand {
+    () log:nand <<(_:X _:A _:B) :fib _:Y>>.
+    _:X math:greaterThan 1.
+    (_:X 1) math:difference _:C.
+    (_:A _:B) math:sum _:D.
+    (_:C _:B _:D) :fib _:Y.
+}.
+
+# query
+{
+    1 :fibonacci ?X1.
+    2 :fibonacci ?X2.
+    3 :fibonacci ?X3.
+    91 :fibonacci ?X91.
+    283 :fibonacci ?X283.
+    3674 :fibonacci ?X3674.
+} log:query {
+    1 :fibonacci ?X1.
+    2 :fibonacci ?X2.
+    3 :fibonacci ?X3.
+    91 :fibonacci ?X91.
+    283 :fibonacci ?X283.
+    3674 :fibonacci ?X3674.
+}.
diff --git a/reasoning/rdfsurfaces/output/fibonacci.n3 b/reasoning/rdfsurfaces/output/fibonacci.n3
@@ -0,0 +1,8 @@
+@prefix : <file:///home/jdroo/github.com/eyereasoner/eye/reasoning/rdfsurfaces/fibonacci.n3#>.
+
+1 :fibonacci 1 .
+2 :fibonacci 1 .
+3 :fibonacci 2 .
+91 :fibonacci 4660046610375530309 .
+283 :fibonacci 62232491515607091882574410635924603070626544377175485625797 .
+3674 :fibonacci 295872959797101479478634366815157108100573212705250690577871041398423606408217262643449728342664061812585639168722421830407677671667740585806703531229882783069925750619720511808616484846128237251921414441458265138672827487722512845223115526738192067144721087756159352711138340620702266509343657403678256247195010013499661223527119909308682062873140767135468966093474944529418214755911968500799987099146489838560114063096775586903976827512299123202488315139397181279903459556726060805948910609527571241968534269554079076649680403030083743420820438603816095671532163428933363322524736324029745871445486444623006627119156710782085648303485296149604974010598940800770684835758031137479033374229914629583184427269638360355586190323578625395157899987377625662075558684705457 .