working reasoning time generated sequents

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v5.0.5 (2023-10-07) working reasoning time generated sequents
 v5.0.4 (2023-10-05) reverting sequents and using rdfsurfaces instead
 v5.0.3 (2023-10-04) adding contrapositive for sequents
 v5.0.2 (2023-10-04) using set notation ($ $) for sequents

VERSION

@@ -1 +1 @@
-5.0.4
+5.0.5

eye.pl

@@ -21,7 +21,7 @@
 :- use_module(library(pcre)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v5.0.4 (2023-10-05)').
+version_info('EYE v5.0.5 (2023-10-07)').
 
 license_info('MIT License
 
@@ -626,6 +626,43 @@
     ;   true
     ).
 
+%
+% Sequents
+% See https://en.wikipedia.org/wiki/Sequent
+%
+
+sequents :-
+    % resolution
+    assertz(implies((
+            implies(A, set(B), _),
+            nonvar(B),
+            select(C, B, D),
+            implies(C, E, _),
+            E \= set(_)
+            ), '<http://www.w3.org/2000/10/swap/log#implies>'(A, set([E|D])), '<>')),
+    % factoring
+    assertz(implies((
+            implies(A, set(B), _),
+            nonvar(B),
+            list_to_set(B, [C])
+            ), '<http://www.w3.org/2000/10/swap/log#implies>'(A, C), '<>')),
+    % contrapositive
+    assertz(implies((
+            implies(A, set(B), _),
+            nonvar(B),
+            select(C, B, D),
+            E = ('<http://www.w3.org/2000/10/swap/log#implies>'(C, set([])), A)
+            ), '<http://www.w3.org/2000/10/swap/log#implies>'(E, set(D)), '<>')),
+    % double negation
+    assertz(implies((
+            implies('<http://www.w3.org/2000/10/swap/log#implies>'(A, set([])), set([]), _)
+            ), A, '<>')),
+    % inference fuse
+    assertz(implies((
+            '<http://www.w3.org/2000/10/swap/log#implies>'(A, set([])),
+            A
+            ), false, '<>')).
+
 %
 % RDF Surfaces
 % See https://w3c-cg.github.io/blogic/
@@ -1421,6 +1458,12 @@
         ->  nb_setval(current_scope, Scope)
         ;   true
         ),
+        (   \+flag(sequents),
+            Rt = '<http://www.w3.org/2000/10/swap/log#implies>'(_, set(_))
+        ->  assertz(flag(sequents)),
+            sequents
+        ;   true
+        ),
         (   functor(Rt, F, _),
             regex('^<.*#on.*Surface>$', F, _),
             \+flag(blogic)
@@ -1863,6 +1906,12 @@
     tr_n3p(Z, Src, query).
 tr_n3p(['\'<http://www.w3.org/2000/10/swap/log#implies>\''(X, Y)|Z], Src, Mode) :-
     !,
+    (   \+flag(sequents),
+        Y = set(_)
+    ->  assertz(flag(sequents)),
+        sequents
+    ;   true
+    ),
     (   flag(tactic, 'linear-select')
     ->  write(implies(X, '\'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#transaction>\''(X, Y), Src)),
         writeln('.'),
@@ -5100,6 +5149,7 @@
         ;   djiti_assertz(Dn),
             (   flag('pass-only-new'),
                 Dn \= answer(_, _, _),
+                \+ (flag(sequents), Dn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
                 \+ (flag(blogic), Dn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
                 \+pass_only_new(Dn)
             ->  assertz(pass_only_new(Dn))
@@ -5137,6 +5187,7 @@
             ;   djiti_assertz(Cn),
                 (   flag('pass-only-new'),
                     Cn \= answer(_, _, _),
+                    \+ (flag(sequents), Cn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
                     \+ (flag(blogic), Cn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
                     \+pass_only_new(Cn)
                 ->  assertz(pass_only_new(Cn))
@@ -5257,9 +5308,18 @@
     !.
 djiti_fact('<http://www.w3.org/2000/10/swap/log#implies>'(A, B), C) :-
     nonvar(B),
+    (   \+flag(sequents),
+        B = set(_)
+    ->  assertz(flag(sequents)),
+        sequents
+    ;   true
+    ),
     (   conj_list(B, D)
     ->  true
-    ;   D = B
+    ;   (   B = set(D)
+        ->  true
+        ;   D = B
+        )
     ),
     forall(
         member(E, D),

reasoning/blogic/version.n3s.out

@@ -1,3 +1,3 @@
 @prefix log: <http://www.w3.org/2000/10/swap/log#>.
 
-() log:version "EYE v5.0.4 (2023-10-05)".
+() log:version "EYE v5.0.5 (2023-10-07)".

reasoning/sequents/README

@@ -0,0 +1,25 @@
+--------
+Sequents
+--------
+
+See https://en.wikipedia.org/wiki/Sequent
+
+E.g.
+
+# all cars are green or blue
+{
+    ?A a :Car.
+} => ($
+    {
+        ?A :is :green.
+    }
+    {
+        ?A :is :blue.
+    }
+$).
+
+# negation
+{
+    ?A a :Car.
+    ?A a :Horse.
+} => ($ $).

reasoning/sequents/abc.n3

@@ -0,0 +1,22 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# i element of A
+:i a :A.
+
+# i not element of C
+{
+    :i a :C.
+} => ($ $).
+
+# all A are B or C
+{
+    ?S a :A.
+} => ($
+    {
+        ?S a :B.
+    }
+    {
+        ?S a :C.
+    }
+$).

reasoning/sequents/abc.n3.out

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

reasoning/sequents/beetle.n3

@@ -0,0 +1,36 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# beetle is a car
+:beetle a :Car.
+
+# all cars are green or blue
+{
+    ?A a :Car.
+} => ($
+    {
+        ?A :is :green.
+    }
+    {
+        ?A :is :blue.
+    }
+$).
+
+# green things are beautiful
+{
+    ?A :is :green.
+} => {
+    ?A :is :beautiful.
+}.
+
+# blue things are beautiful
+{
+    ?A :is :blue.
+} => {
+    ?A :is :beautiful.
+}.
+
+# everything is not beautiful would be inconsistent
+#{
+#    ?A :is :beautiful.
+#} => ($ $).

reasoning/sequents/beetle.n3.out

@@ -0,0 +1,3 @@
+@prefix : <http://example.org/ns#>.
+
+:beetle :is :beautiful.

reasoning/sequents/beetle12.n3

@@ -0,0 +1,156 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# beetle is a car
+:beetle a :Car.
+
+# all cars are green or blue
+{
+    ?A a :Car.
+} => ($
+    {
+        ?A :is :green.
+    }
+    {
+        ?A :is :blue.
+    }
+$).
+
+# green things are nice or pretty
+{
+    ?A :is :green.
+} => ($
+    {
+        ?A :is :nice.
+    }
+    {
+        ?A :is :pretty.
+    }
+$).
+
+# pretty things are pretty 1 or pretty 2
+{
+    ?A :is :pretty.
+} => ($
+    {
+        ?A :is :pretty1.
+    }
+    {
+        ?A :is :pretty2.
+    }
+$).
+
+# nice things are nice 1 or nice 2
+{
+    ?A :is :nice.
+} => ($
+    {
+        ?A :is :nice1.
+    }
+    {
+        ?A :is :nice2.
+    }
+$).
+
+# pretty 1 things are pretty 11 or pretty 12
+{
+    ?A :is :pretty1.
+} => ($
+    {
+        ?A :is :pretty11.
+    }
+    {
+        ?A :is :pretty12.
+    }
+$).
+
+# pretty 2 things are pretty 21 or pretty 22
+{
+    ?A :is :pretty2.
+} => ($
+    {
+        ?A :is :pretty21.
+    }
+    {
+        ?A :is :pretty22.
+    }
+$).
+
+# nice 1 things are nice 11 or nice 12
+{
+    ?A :is :nice1.
+} => ($
+    {
+        ?A :is :nice11.
+    }
+    {
+        ?A :is :nice12.
+    }
+$).
+
+# nice 2 things are nice 21 or nice 22
+{
+    ?A :is :nice2.
+} => ($
+    {
+        ?A :is :nice21.
+    }
+    {
+        ?A :is :nice22.
+    }
+$).
+
+# pretty or nice or blue things are beautiful
+{
+    ?A :is :pretty11.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :pretty12.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :pretty21.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :pretty22.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice11.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice12.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice21.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice22.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :blue.
+} => {
+    ?A :is :beautiful.
+}.

reasoning/sequents/beetle12.n3.out

@@ -0,0 +1,3 @@
+@prefix : <http://example.org/ns#>.
+
+:beetle :is :beautiful.