adding create sequent metarule for blogic

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v5.0.7 (2023-10-09) adding create sequent metarule for blogic
 v5.0.6 (2023-10-08) adding list:notMember built-in
 v5.0.5 (2023-10-07) working reasoning time generated sequents
 v5.0.4 (2023-10-05) reverting sequents and using rdfsurfaces instead

VERSION

@@ -1 +1 @@
-5.0.6
+5.0.7

eye.pl

@@ -21,7 +21,7 @@
 :- use_module(library(pcre)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v5.0.6 (2023-10-08)').
+version_info('EYE v5.0.7 (2023-10-09)').
 
 license_info('MIT License
 
@@ -779,6 +779,35 @@
             findvars(S, W, beta),
             makevars(S, I, beta(W))
             ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
+    % create sequent
+    assertz(implies((
+            '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, G),
+            is_list(V),
+            is_graph(G),
+            conj_list(G, L),
+            list_to_set(L, B),
+            \+member('<http://www.w3.org/2000/10/swap/log#onAnswerSurface>'(_, _), B),
+            \+member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, triple(_, _, _)), B),
+            findall(J,
+                (   member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, J), B)
+                ),
+                H
+            ),
+            length(H, N),
+            N >= 2,
+            findall(J,
+                (   member(J, B),
+                    J \= '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _)
+                ),
+                K
+            ),
+            conj_list(R, K),
+            find_graffiti(K, D),
+            append(V, 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, set(I)), '<>')),
     % create contrapositive rule
     assertz(implies((
             '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, G),
@@ -1459,6 +1488,7 @@
         ;   true
         ),
         (   \+flag(sequents),
+            \+flag(blogic),
             Rt = '<http://www.w3.org/2000/10/swap/log#implies>'(_, set(_))
         ->  assertz(flag(sequents)),
             sequents
@@ -1907,6 +1937,7 @@
 tr_n3p(['\'<http://www.w3.org/2000/10/swap/log#implies>\''(X, Y)|Z], Src, Mode) :-
     !,
     (   \+flag(sequents),
+        \+flag(blogic),
         Y = set(_)
     ->  assertz(flag(sequents)),
         sequents
@@ -5309,6 +5340,7 @@
 djiti_fact('<http://www.w3.org/2000/10/swap/log#implies>'(A, B), C) :-
     nonvar(B),
     (   \+flag(sequents),
+        \+flag(blogic),
         B = set(_)
     ->  assertz(flag(sequents)),
         sequents

reasoning/blogic/beetle10.n3s.out

@@ -1,4 +1,4 @@
 @prefix : <http://example.org/ns#>.
 
 :grannysmith :is :green.
-_:sk_42 :is :beautiful.
+_:sk_53 :is :beautiful.

reasoning/blogic/beetle10a.n3s.out

@@ -1,4 +1,4 @@
 @prefix : <http://example.org/ns#>.
 
 :grannysmith :is :green.
-_:sk_51 :is :beautiful.
+_:sk_62 :is :beautiful.

reasoning/blogic/beetle9a.n3s.out

@@ -1,3 +1,3 @@
 @prefix : <http://example.org/ns#>.
 
-_:sk_42 :is :beautiful.
+_:sk_53 :is :beautiful.

reasoning/blogic/graph-play2.n3s.out

@@ -13,7 +13,7 @@
     }.
 }.
 () log:onNegativeSurface {
-    _:sk_13 a <urn:example:C>.
+    _:sk_24 a <urn:example:C>.
 }.
 (_:e_S1_1_2 _:e_x_1_1 _:e_y_1_1) log:onNegativeSurface {
     () log:onNeutralSurface _:e_S1_1_2.

reasoning/blogic/model.n3s

@@ -0,0 +1,83 @@
+# ----------------------------
+# Policy model finding example
+# ----------------------------
+
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix list: <http://www.w3.org/2000/10/swap/list#>.
+@prefix graph: <http://www.w3.org/2000/10/swap/graph#>.
+@prefix vcard: <http://www.w3.org/2006/vcard/ns#>.
+@prefix : <http://example.org/ns#>.
+
+# Pat is an individual
+:Pat a vcard:Individual.
+
+# if X is an individual then X can do A or B
+(_:X) log:onNegativeSurface {
+    _:X a vcard:Individual.
+    () log:onNegativeSurface {
+        _:X :canDo :A.
+    }.
+    () log:onNegativeSurface {
+        _:X :canDo :B.
+    }.
+}.
+
+# if X is an individual who can do A then X can do E or D
+(_:X) log:onNegativeSurface {
+    #_:X a vcard:Individual.
+    _:X :canDo :A.
+    () log:onNegativeSurface {
+        _:X :canDo :E.
+    }.
+    () log:onNegativeSurface {
+        _:X :canDo :D.
+    }.
+}.
+
+# if X is an individual who can do D then X can do E or F
+(_:X) log:onNegativeSurface {
+    #_:X a vcard:Individual.
+    _:X :canDo :D.
+    () log:onNegativeSurface {
+        _:X :canDo :E.
+    }.
+    () log:onNegativeSurface {
+        _:X :canDo :F.
+    }.
+}.
+
+# find model reaching goal
+(_:Goal _:Sequents _:Model) log:onNegativeSurface {
+    () log:onNegativeSurface <<_:Goal :findModel (_:Sequents _:Model _:Model)>>.
+    _:Goal log:callWithCut true.
+}.
+
+(_:Goal _:Sequents1 _:Model1 _:Model _:Prem _:Cases _:Case _:Sequents2 _:Model2) log:onNegativeSurface {
+    () log:onNegativeSurface <<_:Goal :findModel (_:Sequents1 _:Model1 _:Model)>>.
+    _:Prem => _:Cases.
+    _:Cases list:member _:Case.
+    _:Prem log:call true.
+    _:Sequents1 list:notMember {_:Prem => _:Cases}.
+    (_:Sequents1 ({_:Prem => _:Cases})) list:append _:Sequents2.
+    (_:Model1 (_:Case)) list:append _:Model2.
+    true log:becomes _:Case.
+    {
+        _:Goal :findModel (_:Sequents2 _:Model2 _:Model).
+    } log:callWithCleanup {
+        _:Case log:becomes true.
+    }.
+}.
+
+# find model where X is an individual who can do E
+(_:X _:Model) log:onQuestionSurface {
+    {
+        _:X a vcard:Individual.
+        _:X :canDo :E.
+    } :findModel (() () _:Model).
+    () log:onAnswerSurface {
+        {
+            _:X a vcard:Individual.
+            _:X :canDo :E.
+        } :perModel _:Model.
+    }.
+}.

reasoning/blogic/model.n3s.out

@@ -0,0 +1,21 @@
+@prefix : <http://example.org/ns#>.
+@prefix vcard: <http://www.w3.org/2006/vcard/ns#>.
+
+{
+    :Pat a vcard:Individual.
+    :Pat :canDo :E.
+} :perModel ({
+    :Pat :canDo :A.
+} {
+    :Pat :canDo :E.
+}).
+{
+    :Pat a vcard:Individual.
+    :Pat :canDo :E.
+} :perModel ({
+    :Pat :canDo :A.
+} {
+    :Pat :canDo :D.
+} {
+    :Pat :canDo :E.
+}).

reasoning/blogic/version.n3s.out

@@ -1,3 +1,3 @@
 @prefix log: <http://www.w3.org/2000/10/swap/log#>.
 
-() log:version "EYE v5.0.6 (2023-10-08)".
+() log:version "EYE v5.0.7 (2023-10-09)".