fixing universal statements and adding steps case

eyereasoner · Aug 26, 2024 · 1198816 · 1198816
1 parent fb9bc0e
commit 1198816
Show file tree

Hide file tree

Showing 4 changed files with 364 additions and 5 deletions.
diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-1.2.4
+1.2.5
diff --git a/etc/output/steps.trig b/etc/output/steps.trig
@@ -0,0 +1,231 @@
+PREFIX : <https://eyereasoner.github.io/lingua/etc/steps.trig#>
+PREFIX lingua: <http://www.w3.org/2000/10/swap/lingua#>
+PREFIX log: <http://www.w3.org/2000/10/swap/log#>
+PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
+PREFIX list: <http://www.w3.org/2000/10/swap/list#>
+PREFIX vcard: <http://www.w3.org/2006/vcard/ns#>
+
+:model :is (_:bng_1 _:bng_2).
+:model :is (_:bng_1 _:bng_3 _:bng_2).
+
+#
+# lingua explanation
+#
+
+_:bng_4 lingua:explanation _:bng_5.
+_:bng_6 lingua:explanation _:bng_7.
+_:bng_8 lingua:explanation _:bng_9.
+_:bng_9 lingua:explanation _:bng_10.
+_:bng_4 lingua:explanation _:bng_11.
+_:bng_12 lingua:explanation _:bng_13.
+_:bng_14 lingua:explanation _:bng_15.
+_:bng_16 lingua:explanation _:bng_17.
+_:bng_17 lingua:explanation _:bng_18.
+
+GRAPH _:bng_19 {
+    :Pat a vcard:Individual.
+    :Pat :canDo :E.
+}
+
+GRAPH _:bng_20 {
+    _:bng_24 log:sequent (_:bng_1 _:bng_25).
+}
+
+GRAPH _:bng_21 {
+    _:bng_22 log:sequent (_:bng_2 _:bng_3).
+}
+
+GRAPH _:bng_1 {
+    :Pat :canDo :A.
+}
+
+GRAPH _:bng_2 {
+    :Pat :canDo :E.
+}
+
+GRAPH _:bng_27 {
+    _:bng_28 log:sequent (_:bng_2 _:bng_29).
+}
+
+GRAPH _:bng_3 {
+    :Pat :canDo :D.
+}
+
+GRAPH _:bng_4 {
+    _:bng_19 log:call true.
+    [] rdf:value true; log:callWithCut true.
+}
+
+GRAPH _:bng_5 {
+    _:bng_19 :findModel ((_:bng_20 _:bng_21) (_:bng_1 _:bng_2) (_:bng_1 _:bng_2)).
+}
+
+GRAPH _:bng_6 {
+    _:bng_22 log:sequent (_:bng_2 _:bng_3).
+    (_:bng_2 _:bng_3) list:member _:bng_2.
+    _:bng_22 log:call true.
+    (_:bng_20) list:notMember _:bng_21.
+    ((_:bng_20) (_:bng_21)) list:append (_:bng_20 _:bng_21).
+    ((_:bng_1) (_:bng_2)) list:append (_:bng_1 _:bng_2).
+    [] rdf:value true; log:becomes _:bng_2.
+    _:bng_5 log:callWithCleanup _:bng_23.
+}
+
+GRAPH _:bng_7 {
+    _:bng_19 :findModel ((_:bng_20) (_:bng_1) (_:bng_1 _:bng_2)).
+}
+
+GRAPH _:bng_8 {
+    _:bng_24 log:sequent (_:bng_1 _:bng_25).
+    (_:bng_1 _:bng_25) list:member _:bng_1.
+    _:bng_24 log:call true.
+    () list:notMember _:bng_20.
+    (() (_:bng_20)) list:append (_:bng_20).
+    (() (_:bng_1)) list:append (_:bng_1).
+    [] rdf:value true; log:becomes _:bng_1.
+    _:bng_7 log:callWithCleanup _:bng_26.
+}
+
+GRAPH _:bng_9 {
+    _:bng_19 :findModel (() () (_:bng_1 _:bng_2)).
+}
+
+GRAPH _:bng_10 {
+    :model :is (_:bng_1 _:bng_2).
+}
+
+GRAPH _:bng_11 {
+    _:bng_19 :findModel ((_:bng_20 _:bng_21 _:bng_27) (_:bng_1 _:bng_3 _:bng_2) (_:bng_1 _:bng_3 _:bng_2)).
+}
+
+GRAPH _:bng_12 {
+    _:bng_28 log:sequent (_:bng_2 _:bng_29).
+    (_:bng_2 _:bng_29) list:member _:bng_2.
+    _:bng_28 log:call true.
+    (_:bng_20 _:bng_21) list:notMember _:bng_27.
+    ((_:bng_20 _:bng_21) (_:bng_27)) list:append (_:bng_20 _:bng_21 _:bng_27).
+    ((_:bng_1 _:bng_3) (_:bng_2)) list:append (_:bng_1 _:bng_3 _:bng_2).
+    [] rdf:value true; log:becomes _:bng_2.
+    _:bng_11 log:callWithCleanup _:bng_23.
+}
+
+GRAPH _:bng_13 {
+    _:bng_19 :findModel ((_:bng_20 _:bng_21) (_:bng_1 _:bng_3) (_:bng_1 _:bng_3 _:bng_2)).
+}
+
+GRAPH _:bng_14 {
+    _:bng_22 log:sequent (_:bng_2 _:bng_3).
+    (_:bng_2 _:bng_3) list:member _:bng_3.
+    _:bng_22 log:call true.
+    (_:bng_20) list:notMember _:bng_21.
+    ((_:bng_20) (_:bng_21)) list:append (_:bng_20 _:bng_21).
+    ((_:bng_1) (_:bng_3)) list:append (_:bng_1 _:bng_3).
+    [] rdf:value true; log:becomes _:bng_3.
+    _:bng_13 log:callWithCleanup _:bng_30.
+}
+
+GRAPH _:bng_15 {
+    _:bng_19 :findModel ((_:bng_20) (_:bng_1) (_:bng_1 _:bng_3 _:bng_2)).
+}
+
+GRAPH _:bng_16 {
+    _:bng_24 log:sequent (_:bng_1 _:bng_25).
+    (_:bng_1 _:bng_25) list:member _:bng_1.
+    _:bng_24 log:call true.
+    () list:notMember _:bng_20.
+    (() (_:bng_20)) list:append (_:bng_20).
+    (() (_:bng_1)) list:append (_:bng_1).
+    [] rdf:value true; log:becomes _:bng_1.
+    _:bng_15 log:callWithCleanup _:bng_26.
+}
+
+GRAPH _:bng_17 {
+    _:bng_19 :findModel (() () (_:bng_1 _:bng_3 _:bng_2)).
+}
+
+GRAPH _:bng_18 {
+    :model :is (_:bng_1 _:bng_3 _:bng_2).
+}
+
+GRAPH _:bng_24 {
+    :Pat a vcard:Individual.
+}
+
+GRAPH _:bng_25 {
+    :Pat :canDo :B.
+}
+
+GRAPH _:bng_22 {
+    :Pat a vcard:Individual.
+    :Pat :canDo :A.
+}
+
+GRAPH _:bng_28 {
+    :Pat a vcard:Individual.
+    :Pat :canDo :D.
+}
+
+GRAPH _:bng_2 {
+    :Pat :canDo :E.
+}
+
+GRAPH _:bng_29 {
+    :Pat :canDo :F.
+}
+
+GRAPH _:bng_19 {
+    :Pat a vcard:Individual.
+    :Pat :canDo :E.
+}
+
+GRAPH _:bng_20 {
+    _:bng_24 log:sequent (_:bng_1 _:bng_25).
+}
+
+GRAPH _:bng_21 {
+    _:bng_22 log:sequent (_:bng_2 _:bng_3).
+}
+
+GRAPH _:bng_1 {
+    :Pat :canDo :A.
+}
+
+GRAPH _:bng_3 {
+    :Pat :canDo :D.
+}
+
+GRAPH _:bng_5 {
+    _:bng_19 :findModel ((_:bng_20 _:bng_21) (_:bng_1 _:bng_2) (_:bng_1 _:bng_2)).
+}
+
+GRAPH _:bng_23 {
+    _:bng_2 log:becomes true.
+}
+
+GRAPH _:bng_7 {
+    _:bng_19 :findModel ((_:bng_20) (_:bng_1) (_:bng_1 _:bng_2)).
+}
+
+GRAPH _:bng_26 {
+    _:bng_1 log:becomes true.
+}
+
+GRAPH _:bng_27 {
+    _:bng_28 log:sequent (_:bng_2 _:bng_29).
+}
+
+GRAPH _:bng_11 {
+    _:bng_19 :findModel ((_:bng_20 _:bng_21 _:bng_27) (_:bng_1 _:bng_3 _:bng_2) (_:bng_1 _:bng_3 _:bng_2)).
+}
+
+GRAPH _:bng_13 {
+    _:bng_19 :findModel ((_:bng_20 _:bng_21) (_:bng_1 _:bng_3) (_:bng_1 _:bng_3 _:bng_2)).
+}
+
+GRAPH _:bng_30 {
+    _:bng_3 log:becomes true.
+}
+
+GRAPH _:bng_15 {
+    _:bng_19 :findModel ((_:bng_20) (_:bng_1) (_:bng_1 _:bng_3 _:bng_2)).
+}
diff --git a/etc/steps.trig b/etc/steps.trig
@@ -0,0 +1,120 @@
+# ----------------------------
+# Policy model finding example
+# ----------------------------
+#
+# Inspired by gps.trig
+
+PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
+PREFIX list: <http://www.w3.org/2000/10/swap/list#>
+PREFIX log: <http://www.w3.org/2000/10/swap/log#>
+PREFIX vcard: <http://www.w3.org/2006/vcard/ns#>
+PREFIX lingua: <http://www.w3.org/2000/10/swap/lingua#>
+PREFIX var: <http://www.w3.org/2000/10/swap/var#>
+PREFIX : <#>
+
+# Pat is an individual
+:Pat a vcard:Individual.
+
+# if X is an individual then X can do A or B
+_:bng_1 log:sequent (_:bng_2 _:bng_3).
+
+GRAPH _:bng_1 {
+    var:X a vcard:Individual.
+}
+
+GRAPH _:bng_2 {
+    var:X :canDo :A.
+}
+
+GRAPH _:bng_3 {
+    var:X :canDo :B.
+}
+
+# if X is an individual who can do A then X can do E or D
+_:bng_4 log:sequent (_:bng_5 _:bng_6).
+
+GRAPH _:bng_4 {
+    var:X a vcard:Individual.
+    var:X :canDo :A.
+}
+
+GRAPH _:bng_5 {
+    var:X :canDo :E.
+}
+
+GRAPH _:bng_6 {
+    var:X :canDo :D.
+}
+
+# if X is an individual who can do D then X can do E or F
+_:bng_7 log:sequent (_:bng_8 _:bng_9).
+
+GRAPH _:bng_7 {
+    var:X a vcard:Individual.
+    var:X :canDo :D.
+}
+
+GRAPH _:bng_8 {
+    var:X :canDo :E.
+}
+
+GRAPH _:bng_9 {
+    var:X :canDo :F.
+}
+
+# find model reaching goal
+_:bng_10 lingua:backward _:bng_11.
+
+GRAPH _:bng_10 {
+    var:Goal :findModel (var:Steps var:Model var:Model).
+}
+
+GRAPH _:bng_11 {
+    var:Goal log:call true.
+    [] rdf:value true; log:callWithCut true.
+}
+
+_:bng_12 lingua:backward _:bng_13.
+
+GRAPH _:bng_12 {
+    var:Goal :findModel (var:Steps1 var:Model1 var:Model).
+}
+
+GRAPH _:bng_13 {
+    var:Prem log:sequent var:Cases.
+    var:Cases list:member var:Case.
+    var:Prem log:call true.
+    var:Steps1 list:notMember _:bng_14.
+    (var:Steps1 (_:bng_14)) list:append var:Steps2.
+    (var:Model1 (var:Case)) list:append var:Model2.
+    [] rdf:value true; log:becomes var:Case.
+    _:bng_15 log:callWithCleanup _:bng_16.
+}
+
+GRAPH _:bng_14 {
+    var:Prem log:sequent var:Cases.
+}
+
+GRAPH _:bng_15 {
+    var:Goal :findModel (var:Steps2 var:Model2 var:Model).
+}
+
+GRAPH _:bng_16 {
+    var:Case log:becomes true.
+}
+
+# query: find model where X is an individual who can do E
+_:bng_17 lingua:answer _:bng_18.
+
+GRAPH _:bng_17 {
+    _:bng_19 :findModel (() () var:Model).
+}
+
+GRAPH _:bng_18 {
+    :model :is var:Model.
+}
+
+GRAPH _:bng_19 {
+    var:X a vcard:Individual.
+    var:X :canDo :E.
+}
diff --git a/lingua.pl b/lingua.pl
@@ -19,7 +19,7 @@
 :- use_module(library(semweb/turtle)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('lingua v1.2.4').
+version_info('lingua v1.2.5').
 
 help_info('Usage: lingua <options>* <data>*
 
@@ -302,7 +302,7 @@
 
     % create universal statements
     (   pred(P),
-        \+atom_concat('<http://www.w3.org/2000/10/swap/', _, P),
+        \+atom_concat('<http://www.w3.org/2000/10/swap/lingua#', _, P),
         X =.. [P, _, _],
         call(X),
         findvars(X, V, alpha),
@@ -439,7 +439,11 @@
             trig_term(P, Predicate),
             trig_term(O, Object),
             Triple =.. [Predicate, Subject, Object],
-            djiti_assertz(Triple)
+            djiti_assertz(Triple),
+            (   current_predicate(Predicate/2)
+            ->  true
+            ;   dynamic(Predicate/2)
+            )
         )
     ),
     forall(
@@ -449,7 +453,11 @@
             trig_term(O, Object),
             G = H:_,
             trig_term(H, Graph),
-            assertz(quad(Subject, Predicate, Object, Graph))
+            assertz(quad(Subject, Predicate, Object, Graph)),
+            (   current_predicate(Predicate/2)
+            ->  true
+            ;   dynamic(Predicate/2)
+            )
         )
     ),
     args(Args).