Merge branch 'master' of https://github.com/eyereasoner/eye

eyereasoner · Aug 14, 2024 · 8c81b58 · 8c81b58
2 parents e382c4f + ef9960c
commit 8c81b58
Show file tree

Hide file tree

Showing 18 changed files with 120 additions and 101 deletions.
diff --git a/RELEASE b/RELEASE
@@ -1,5 +1,12 @@
                                   EYE release
 
+v10.19.2 (2024-08-13) functional terms again as lists (functor args)
+v10.19.1 (2024-08-13) output only used namespace prefixes
+v10.19.0 (2024-08-12) changing functional terms to [| functor args |]
+v10.18.6 (2024-08-12) autodetecting single answer for rdfsurfaces
+v10.18.5 (2024-08-12) supporting log:Component for rdfsurfaces
+v10.18.4 (2024-08-11) further fixing rdfsurfaces conversion
+v10.18.3 (2024-08-11) fixing rdfsurfaces conversion
 v10.18.2 (2024-08-10) supporting log:onNegativeSurface via prepare_builtins/0 and dropping log:onQuerySurface
 v10.18.1 (2024-08-09) testing universality
 v10.18.0 (2024-08-08) replace log:onNegativeQuestionSurface with log:onNegativeSurface

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-10.18.2
+10.19.2
diff --git a/eye.pl b/eye.pl
@@ -22,7 +22,7 @@
 :- catch(use_module(library(process)), _, true).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v10.18.2 (2024-08-10)').
+version_info('EYE v10.19.2 (2024-08-13)').
 
 license_info('MIT License
 
@@ -2114,11 +2114,6 @@
     {   sort(List, Distinct)
     },
     ['$', ')'].
-pathitem(fterm(List), Triples) -->
-    ['(', '|'],
-    !,
-    pathlist(List, Triples),
-    ['|', ')'].
 pathitem(List, Triples) -->
     ['('],
     !,
@@ -3494,6 +3489,27 @@
         )
     ).
 
+w4 :-
+    open_null_stream(Ws),
+    tell(Ws),
+    nb_getval(wn, Wn),
+    w3,
+    retractall(pfx(_, _)),
+    retractall(wpfx(_)),
+    nb_setval(wn, Wn),
+    nb_setval(output_statements, 0),
+    nb_setval(lemma_cursor, 0),
+    forall(
+        apfx(Pfx, Uri),
+        assertz(pfx(Pfx, Uri))
+    ),
+    told,
+    (   flag('output', Output)
+    ->  tell(Output)
+    ;   true
+    ),
+    w3.
+
 w3 :-
     wh,
     nb_setval(fdepth, 0),
@@ -4030,11 +4046,6 @@
     write('($'),
     wl(X),
     write(' $)').
-wt1(fterm(X)) :-
-    !,
-    write('(|'),
-    wl(X),
-    write(' |)').
 wt1('$VAR'(X)) :-
     !,
     write('?V'),
@@ -4883,7 +4894,7 @@
             AnswerCount >= AnswerLimit
         ->  (   flag(strings)
             ->  true
-            ;   w3
+            ;   w4
             )
         ;   retract(brake),
             fail
@@ -4903,25 +4914,7 @@
             ->  true
             ;   (   flag('pass-only-new')
                 ->  true
-                ;   open_null_stream(Ws),
-                    tell(Ws),
-                    nb_getval(wn, Wn),
-                    w3,
-                    retractall(pfx(_, _)),
-                    retractall(wpfx(_)),
-                    nb_setval(wn, Wn),
-                    nb_setval(output_statements, 0),
-                    nb_setval(lemma_cursor, 0),
-                    forall(
-                        apfx(Pfx, Uri),
-                        assertz(pfx(Pfx, Uri))
-                    ),
-                    told,
-                    (   flag('output', Output)
-                    ->  tell(Output)
-                    ;   true
-                    ),
-                    w3
+                ;   w4
                 )
             )
         ;   true
@@ -5177,6 +5170,7 @@
 %
 
 prepare_builtins :-
+    % log:onNegativeSurface
     (   '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _)
     ->  retractall(flag(rdfsurfaces)),
         assertz(flag(rdfsurfaces)),
@@ -5228,7 +5222,7 @@
                 is_list(Vl),
                 is_graph(G),
                 conj_list(G, Gl),
-                \+find_universality(Gl, _, _),
+                \+find_component(Gl, _, _),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _), Gl),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), Gl),
                 makevars([Vl, Gl], [Vv, Gv], beta(Vl)),
@@ -5268,7 +5262,7 @@
                 is_graph(G),
                 conj_list(G, L),
                 list_to_set(L, B),
-                \+find_universality(B, _, _),
+                \+find_component(B, _, _),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), B),
                 findall(1,
                     (   member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _), B)
@@ -5287,7 +5281,7 @@
                 is_graph(F),
                 conj_list(F, K),
                 list_to_set(K, N),
-                \+find_universality(N, _, _),
+                \+find_component(N, _, _),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), N),
                 length(N, 2),
                 makevars(N, J, beta(Wl)),
@@ -5317,18 +5311,17 @@
                 is_graph(G),
                 conj_list(G, L),
                 list_to_set(L, B),
-                \+find_universality(B, _, _),
+                \+find_component(B, _, _),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), B),
-                select('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(X, H), B, K),
+                select('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(Z, H), B, K),
                 (   H \= '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], _)
-                ;   X = []
+                ;   Z = []
                 ),
                 conj_list(R, K),
                 find_graffiti(K, D),
                 append(Vl, D, U),
                 makevars([R, H], [Q, S], beta(U)),
-                findvars(S, W, beta),
-                makevars(S, I, beta(W))
+                makevars(S, I, beta(Z))
                 ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
 
         % convert negative surfaces to forward contrapositive rules
@@ -5339,7 +5332,7 @@
                 is_graph(G),
                 conj_list(G, L),
                 list_to_set(L, B),
-                \+find_universality(B, _, _),
+                \+find_component(B, _, _),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _), B),
                 \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), B),
                 \+member(exopred(_, _, _), B),
@@ -5361,8 +5354,7 @@
                 find_graffiti([R], D),
                 append(Vl, D, U),
                 makevars([R, E], [Q, S], beta(U)),
-                findvars(S, W, beta),
-                makevars(S, I, beta(W))
+                makevars(S, I, beta(Z))
                 ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
 
         % convert negative surfaces to backward rules
@@ -5373,7 +5365,7 @@
                 is_graph(G),
                 conj_list(G, L),
                 list_to_set(L, B),
-                find_universality(B, T, K),
+                find_component(B, T, K),
                 conj_list(R, K),
                 conjify(R, S),
                 find_graffiti([R], D),
@@ -5433,6 +5425,19 @@
                 conj_list(G, L),
                 list_to_set(L, B),
                 select('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, H), B, K),
+                (   conj_list(H, [H]),
+                    findvars(H, [], beta),
+                    findall(1,
+                        (   '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, Gf),
+                            conj_list(Gf, Lf),
+                            select('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), Lf, _)
+                        ),
+                        [1]
+                    )
+                ->  retractall(flag('limited-answer', _)),
+                    assertz(flag('limited-answer', 1))
+                ;   true
+                ),
                 conj_list(I, K),
                 djiti_answer(answer(H), J),
                 find_graffiti(K, D),
@@ -5456,7 +5461,7 @@
                     is_list(Vl),
                     is_graph(G),
                     conj_list(G, L),
-                    \+find_universality(L, _, _),
+                    \+find_component(L, _, _),
                     makevars(G, H, beta(Vl)),
                     (   H = '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, false),
                         J = true
@@ -12272,15 +12277,18 @@
     A =.. C,
     find_graffiti(C, B).
 
-find_universality(B, T, K) :-
+find_component(B, T, K) :-
     select('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], T), B, K),
     conj_list(T, [T]),
     \+member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _), K),
     \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), K),
-    findvars(T, Tv, beta),
-    findvars(K, Kv, beta),
-    member(Tm, Tv),
-    \+member(Tm, Kv).
+    (   T =.. [P, _, _],
+        '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(P, '<http://www.w3.org/2000/10/swap/log#Component>')
+    ;   findvars(T, Tv, beta),
+        findvars(K, Kv, beta),
+        member(Tm, Tv),
+        \+member(Tm, Kv)
+    ).
 
 raw_type(A, '<http://www.w3.org/2000/10/swap/log#ForAll>') :-
     var(A),
@@ -12309,8 +12317,6 @@
     !.
 raw_type(set(_), '<http://www.w3.org/2000/10/swap/log#Set>') :-
     !.
-raw_type(fterm(_), '<http://www.w3.org/2000/10/swap/log#FunctionalTerm>') :-
-    !.
 raw_type(A, '<http://www.w3.org/2000/10/swap/log#Formula>') :-
     functor(A, B, C),
     B \= ':',

diff --git a/eye.zip b/eye.zip
diff --git a/reasoning/4color/4color_answer.n3 b/reasoning/4color/4color_answer.n3
@@ -1,11 +1,4 @@
 @prefix : <https://eyereasoner.github.io/eye/reasoning/4color#>.
-@prefix list: <http://www.w3.org/2000/10/swap/list#>.
-@prefix log: <http://www.w3.org/2000/10/swap/log#>.
-@prefix func: <http://www.w3.org/2007/rif-builtin-function#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
-@prefix n3: <http://www.w3.org/2004/06/rei#>.
 
 ((: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
@@ -1,11 +1,11 @@
+@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
+@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
 @prefix : <https://eyereasoner.github.io/eye/reasoning/4color#>.
-@prefix list: <http://www.w3.org/2000/10/swap/list#>.
 @prefix log: <http://www.w3.org/2000/10/swap/log#>.
 @prefix func: <http://www.w3.org/2007/rif-builtin-function#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
 @prefix n3: <http://www.w3.org/2004/06/rei#>.
+@prefix list: <http://www.w3.org/2000/10/swap/list#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 
 skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma1;

diff --git a/reasoning/diamond-property/diamond-property-answer.n3 b/reasoning/diamond-property/diamond-property-answer.n3
@@ -1,9 +1,4 @@
-@prefix log: <http://www.w3.org/2000/10/swap/log#>.
 @prefix : <https://eyereasoner.github.io/eye/reasoning/diamond-property/dpe#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
-@prefix n3: <http://www.w3.org/2004/06/rei#>.
 
 :b :re _:sk_1.
 :c :re _:sk_1.
diff --git a/reasoning/diamond-property/diamond-property-proof.n3 b/reasoning/diamond-property/diamond-property-proof.n3
@@ -1,9 +1,8 @@
-@prefix log: <http://www.w3.org/2000/10/swap/log#>.
-@prefix : <https://eyereasoner.github.io/eye/reasoning/diamond-property/dpe#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 @prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
+@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
+@prefix : <https://eyereasoner.github.io/eye/reasoning/diamond-property/dpe#>.
 @prefix n3: <http://www.w3.org/2004/06/rei#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 
 skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma1;

diff --git a/reasoning/dp/dpE.n3 b/reasoning/dp/dpE.n3
@@ -1,9 +1,9 @@
-@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
-@prefix : <https://eyereasoner.github.io/eye/reasoning#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 @prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
+@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
+@prefix : <https://eyereasoner.github.io/eye/reasoning#>.
+@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
 @prefix n3: <http://www.w3.org/2004/06/rei#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 
 skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma1;

diff --git a/reasoning/good-cobbler/README b/reasoning/good-cobbler/README
@@ -0,0 +1,6 @@
+------------
+Good Cobbler
+------------
+
+Example from https://shs.hal.science/halshs-04148373/document
+Using functional logic http://intrologic.stanford.edu/chapters/chapter_11.html
diff --git a/reasoning/good-cobbler/cobbler-answer.n3 b/reasoning/good-cobbler/cobbler-answer.n3
@@ -0,0 +1,3 @@
+@prefix : <urn:example:>.
+
+:test :is true.
diff --git a/reasoning/good-cobbler/cobbler.n3 b/reasoning/good-cobbler/cobbler.n3
@@ -0,0 +1,15 @@
+# Good Cobbler
+# Example from https://shs.hal.science/halshs-04148373/document
+# Using functional logic http://intrologic.stanford.edu/chapters/chapter_11.html
+
+@prefix : <urn:example:>.
+
+# some x is a good cobbler
+_:x :is (:good :Cobbler).
+
+# is there some x which is good at some y
+{
+    ?x :is (:good ?y).
+} =^ {
+    :test :is true.
+}.
diff --git a/reasoning/good-cobbler/test b/reasoning/good-cobbler/test
@@ -0,0 +1,2 @@
+#!/bin/bash
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/good-cobbler/cobbler.n3 --output cobbler-answer.n3
diff --git a/reasoning/mi/mi-answer.n3 b/reasoning/mi/mi-answer.n3
@@ -1,9 +1,4 @@
-@prefix list: <http://www.w3.org/2000/10/swap/list#>.
 @prefix : <https://eyereasoner.github.io/eye/ns#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
-@prefix n3: <http://www.w3.org/2004/06/rei#>.
 
 () :natnum (0).
 () :natnum (:s (0)).

diff --git a/reasoning/resto/resto-proof.n3 b/reasoning/resto/resto-proof.n3
@@ -1,16 +1,14 @@
-@prefix foaf: <http://xmlns.com/foaf/0.1/>.
+@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
+@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
 @prefix resto: <http://example.org/restaurant#>.
-@prefix : <http://example.org/vocab#>.
+@prefix n3: <http://www.w3.org/2004/06/rei#>.
 @prefix http: <http://www.w3.org/2011/http#>.
-@prefix con: <http://www.w3.org/2000/10/swap/pim/contact#>.
-@prefix tmpl: <http://purl.org/restdesc/http-template#>.
-@prefix dc: <http://purl.org/dc/terms/>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+@prefix : <http://example.org/vocab#>.
 @prefix geo: <http://www.w3.org/2003/01/geo/wgs84_pos#>.
 @prefix meteo: <http://purl.org/ns/meteo#>.
-@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
-@prefix n3: <http://www.w3.org/2004/06/rei#>.
+@prefix foaf: <http://xmlns.com/foaf/0.1/>.
+@prefix con: <http://www.w3.org/2000/10/swap/pim/contact#>.
 
 skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma1;
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		#!/bin/bash
		eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/good-cobbler/cobbler.n3 --output cobbler-answer.n3