explanation via explicit question/answer

README.md

@@ -1,6 +1,6 @@
 # Second Eye of Euler - SEE
 
-Reasoning engine that is talking RDF 1.X as the web lingua.
+Reasoning engine that is talking RDF TriG as the web lingua.
 
 Examples are in [lingua](https://github.com/eyereasoner/see-lingua/tree/main/lingua) and their output in [lingua/output](https://github.com/eyereasoner/see-lingua/tree/main/lingua/output)
 

VERSION

@@ -1 +1 @@
-0.6.5
+0.7.0

lingua/README.md

@@ -15,10 +15,6 @@ _:conclusionname {
     RDF triples
 }
 ```
-and is able to give proof explanations as
-```
-:rulename lingua:bindings list of (var:name value) pairs.
-```
 
 A forward rule with `lingua:conclusion` false is an inference fuse.
 
@@ -35,10 +31,6 @@ _:bodyname {
     RDF triples
 }
 ```
-and is able to give proof explanations as
-```
-:rulename lingua:bindings list of (var:name value) pairs.
-```
 
 Lingua also supports querying with queries described in RDF as
 ```
@@ -53,10 +45,6 @@ _:answername {
     RDF triples
 }
 ```
-and is able to give proof explanations as
-```
-:queryname lingua:bindings list of (var:name value) pairs.
-```
 
 When `lingua:answer` is omitted it is the repetition of `lingua:question`.
 
@@ -66,3 +54,20 @@ in the "Semantic Web Area for Play" `http://www.w3.org/2000/10/swap/` URI.
 The `var:` prefix is `<http://www.w3.org/2000/10/swap/var#>` and is used for
 variables that are interpreted as universally quantified variables except for
 forward rule conclusion-only variables which are interpreted existentially.
+
+Lingua also supports blogic https://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk
+
+The top level surface is an implicit positive surface with implicit graffiti.
+
+`lingua:onPositiveSurface` is a positive surface.
+
+`lingua:onNegativeSurface` is a negative surface used to express NAND based logic:
+- nand (not and) is a `lingua:onNegativeSurface`
+- negation is a `lingua:onNegativeSurface`
+- disjunction is a `lingua:onNegativeSurface` containing only `lingua:onNegativeSurface`'s
+- => is a `lingua:onNegativeSurface` containing a `lingua:onNegativeSurface`
+- <= is a `lingua:onNegativeSurface` containing a `lingua:negativeTriple`
+
+`lingua:onQuestionSurface` is a question surface containing an optional `lingua:onAnswerSurface`.
+
+`lingua:onNeutralSurface` is a neutral surface.

lingua/output/ackermann.trig

@@ -1,8 +1,4 @@
 @prefix : <https://eyereasoner.github.io/see-lingua/lingua/ackermann.trig#>.
-@prefix lingua: <http://www.w3.org/2000/10/swap/lingua#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix log: <http://www.w3.org/2000/10/swap/log#>.
-@prefix math: <http://www.w3.org/2000/10/swap/math#>.
 
 (0 0) :ackermann 1 .
 (0 6) :ackermann 7 .
@@ -15,141 +11,3 @@
 (4 0) :ackermann 13 .
 (4 1) :ackermann 65533 .
 (5 0) :ackermann 65533 .
-
-:ackermann_rule0 lingua:body _:gn_1.
-:ackermann_rule0 lingua:headback _:gn_2.
-:ackermann_rule0 lingua:bindings ((var:Y 3) (var:A 4) (var:Z 2)).
-:ackermann_rule_main lingua:body _:gn_3.
-:ackermann_rule_main lingua:headback _:gn_4.
-:ackermann_rule_main lingua:bindings ((var:Y 0) (var:B 3) (var:X 0) (var:C 4) (var:A 1)).
-:ackermann_rule0 lingua:bindings ((var:Y 9) (var:A 10) (var:Z 2)).
-:ackermann_rule_main lingua:bindings ((var:Y 6) (var:B 9) (var:X 0) (var:C 10) (var:A 7)).
-:ackermann_rule1 lingua:body _:gn_5.
-:ackermann_rule1 lingua:headback _:gn_6.
-:ackermann_rule1 lingua:bindings ((var:Y 5) (var:Z 2) (var:A 7)).
-:ackermann_rule_main lingua:bindings ((var:Y 2) (var:B 5) (var:X 1) (var:C 7) (var:A 4)).
-:ackermann_rule1 lingua:bindings ((var:Y 10) (var:Z 2) (var:A 12)).
-:ackermann_rule_main lingua:bindings ((var:Y 7) (var:B 10) (var:X 1) (var:C 12) (var:A 9)).
-:ackermann_rule2 lingua:body _:gn_7.
-:ackermann_rule2 lingua:headback _:gn_8.
-:ackermann_rule2 lingua:bindings ((var:Y 5) (var:Z 2) (var:A 10)).
-:ackermann_rule_main lingua:bindings ((var:Y 2) (var:B 5) (var:X 2) (var:C 10) (var:A 7)).
-:ackermann_rule2 lingua:bindings ((var:Y 12) (var:Z 2) (var:A 24)).
-:ackermann_rule_main lingua:bindings ((var:Y 9) (var:B 12) (var:X 2) (var:C 24) (var:A 21)).
-:ackermann_rule3plus lingua:body _:gn_9.
-:ackermann_rule3plus lingua:headback _:gn_10.
-:ackermann_rule3plus lingua:bindings ((var:X 3) (var:Z 2)).
-:ackermann_rule2 lingua:bindings ((var:Y 1) (var:Z 2) (var:A 2)).
-:ackermann_rule_final lingua:body _:gn_11.
-:ackermann_rule_final lingua:headback _:gn_12.
-:ackermann_rule_final lingua:bindings ((var:Y 1) (var:B 0) (var:X 3) (var:Z 2) (var:C 1) (var:D 2) (var:A 2)).
-:ackermann_rule2 lingua:bindings ((var:Y 2) (var:Z 2) (var:A 4)).
-:ackermann_rule_final lingua:bindings ((var:Y 2) (var:B 1) (var:X 3) (var:Z 2) (var:C 2) (var:D 2) (var:A 4)).
-:ackermann_rule2 lingua:bindings ((var:Y 4) (var:Z 2) (var:A 8)).
-:ackermann_rule_final lingua:bindings ((var:Y 3) (var:B 2) (var:X 3) (var:Z 2) (var:C 4) (var:D 2) (var:A 8)).
-:ackermann_rule2 lingua:bindings ((var:Y 8) (var:Z 2) (var:A 16)).
-:ackermann_rule_final lingua:bindings ((var:Y 4) (var:B 3) (var:X 3) (var:Z 2) (var:C 8) (var:D 2) (var:A 16)).
-:ackermann_rule2 lingua:bindings ((var:Y 16) (var:Z 2) (var:A 32)).
-:ackermann_rule_final lingua:bindings ((var:Y 5) (var:B 4) (var:X 3) (var:Z 2) (var:C 16) (var:D 2) (var:A 32)).
-:ackermann_rule2 lingua:bindings ((var:Y 32) (var:Z 2) (var:A 64)).
-:ackermann_rule_final lingua:bindings ((var:Y 6) (var:B 5) (var:X 3) (var:Z 2) (var:C 32) (var:D 2) (var:A 64)).
-:ackermann_rule2 lingua:bindings ((var:Y 64) (var:Z 2) (var:A 128)).
-:ackermann_rule_final lingua:bindings ((var:Y 7) (var:B 6) (var:X 3) (var:Z 2) (var:C 64) (var:D 2) (var:A 128)).
-:ackermann_rule_main lingua:bindings ((var:Y 4) (var:B 7) (var:X 3) (var:C 128) (var:A 125)).
-:ackermann_rule2 lingua:bindings ((var:Y 128) (var:Z 2) (var:A 256)).
-:ackermann_rule_final lingua:bindings ((var:Y 8) (var:B 7) (var:X 3) (var:Z 2) (var:C 128) (var:D 2) (var:A 256)).
-:ackermann_rule2 lingua:bindings ((var:Y 256) (var:Z 2) (var:A 512)).
-:ackermann_rule_final lingua:bindings ((var:Y 9) (var:B 8) (var:X 3) (var:Z 2) (var:C 256) (var:D 2) (var:A 512)).
-:ackermann_rule2 lingua:bindings ((var:Y 512) (var:Z 2) (var:A 1024)).
-:ackermann_rule_final lingua:bindings ((var:Y 10) (var:B 9) (var:X 3) (var:Z 2) (var:C 512) (var:D 2) (var:A 1024)).
-:ackermann_rule2 lingua:bindings ((var:Y 1024) (var:Z 2) (var:A 2048)).
-:ackermann_rule_final lingua:bindings ((var:Y 11) (var:B 10) (var:X 3) (var:Z 2) (var:C 1024) (var:D 2) (var:A 2048)).
-:ackermann_rule2 lingua:bindings ((var:Y 2048) (var:Z 2) (var:A 4096)).
-:ackermann_rule_final lingua:bindings ((var:Y 12) (var:B 11) (var:X 3) (var:Z 2) (var:C 2048) (var:D 2) (var:A 4096)).
-:ackermann_rule2 lingua:bindings ((var:Y 4096) (var:Z 2) (var:A 8192)).
-:ackermann_rule_final lingua:bindings ((var:Y 13) (var:B 12) (var:X 3) (var:Z 2) (var:C 4096) (var:D 2) (var:A 8192)).
-:ackermann_rule2 lingua:bindings ((var:Y 8192) (var:Z 2) (var:A 16384)).
-:ackermann_rule_final lingua:bindings ((var:Y 14) (var:B 13) (var:X 3) (var:Z 2) (var:C 8192) (var:D 2) (var:A 16384)).
-:ackermann_rule2 lingua:bindings ((var:Y 16384) (var:Z 2) (var:A 32768)).
-:ackermann_rule_final lingua:bindings ((var:Y 15) (var:B 14) (var:X 3) (var:Z 2) (var:C 16384) (var:D 2) (var:A 32768)).
-:ackermann_rule2 lingua:bindings ((var:Y 32768) (var:Z 2) (var:A 65536)).
-:ackermann_rule_final lingua:bindings ((var:Y 16) (var:B 15) (var:X 3) (var:Z 2) (var:C 32768) (var:D 2) (var:A 65536)).
-:ackermann_rule2 lingua:bindings ((var:Y 65536) (var:Z 2) (var:A 131072)).
-:ackermann_rule_final lingua:bindings ((var:Y 17) (var:B 16) (var:X 3) (var:Z 2) (var:C 65536) (var:D 2) (var:A 131072)).
-:ackermann_rule_main lingua:bindings ((var:Y 14) (var:B 17) (var:X 3) (var:C 131072) (var:A 131069)).
-:ackermann_rule3plus lingua:bindings ((var:X 4) (var:Z 2)).
-:ackermann_rule_final lingua:bindings ((var:Y 1) (var:B 0) (var:X 4) (var:Z 2) (var:C 1) (var:D 3) (var:A 2)).
-:ackermann_rule_final lingua:bindings ((var:Y 2) (var:B 1) (var:X 4) (var:Z 2) (var:C 2) (var:D 3) (var:A 4)).
-:ackermann_rule_final lingua:bindings ((var:Y 3) (var:B 2) (var:X 4) (var:Z 2) (var:C 4) (var:D 3) (var:A 16)).
-:ackermann_rule_main lingua:bindings ((var:Y 0) (var:B 3) (var:X 4) (var:C 16) (var:A 13)).
-:ackermann_rule_final lingua:bindings ((var:Y 4) (var:B 3) (var:X 4) (var:Z 2) (var:C 16) (var:D 3) (var:A 65536)).
-:ackermann_rule_main lingua:bindings ((var:Y 1) (var:B 4) (var:X 4) (var:C 65536) (var:A 65533)).
-:ackermann_rule3plus lingua:bindings ((var:X 5) (var:Z 2)).
-:ackermann_rule_final lingua:bindings ((var:Y 1) (var:B 0) (var:X 5) (var:Z 2) (var:C 1) (var:D 4) (var:A 2)).
-:ackermann_rule_final lingua:bindings ((var:Y 2) (var:B 1) (var:X 5) (var:Z 2) (var:C 2) (var:D 4) (var:A 4)).
-:ackermann_rule_final lingua:bindings ((var:Y 3) (var:B 2) (var:X 5) (var:Z 2) (var:C 4) (var:D 4) (var:A 65536)).
-:ackermann_rule_main lingua:bindings ((var:Y 0) (var:B 3) (var:X 5) (var:C 65536) (var:A 65533)).
-:ackermann_query lingua:question _:gn_13.
-:ackermann_query lingua:answer _:gn_13.
-:ackermann_query lingua:bindings ((var:A0 1) (var:A1 7) (var:A2 4) (var:A3 9) (var:A4 7) (var:A5 21) (var:A6 125) (var:A7 131069) (var:A8 13) (var:A9 65533) (var:A11 65533)).
-_:gn_1 {
-    () log:equalTo ().
-    _:true log:callWithCut true.
-    (var:Y 1) math:sum var:A.
-}
-_:gn_2 {
-    (0 var:Y var:Z) :ackermann var:A.
-}
-_:gn_3 {
-    (var:Y 3) math:sum var:B.
-    (var:X var:B 2) :ackermann var:C.
-    (var:C 3) math:difference var:A.
-}
-_:gn_4 {
-    (var:X var:Y) :ackermann var:A.
-}
-_:gn_5 {
-    () log:equalTo ().
-    _:true log:callWithCut true.
-    (var:Y var:Z) math:sum var:A.
-}
-_:gn_6 {
-    (1 var:Y var:Z) :ackermann var:A.
-}
-_:gn_7 {
-    () log:equalTo ().
-    _:true log:callWithCut true.
-    (var:Y var:Z) math:product var:A.
-}
-_:gn_8 {
-    (2 var:Y var:Z) :ackermann var:A.
-}
-_:gn_9 {
-    () log:equalTo ().
-    _:true log:callWithCut true.
-}
-_:gn_10 {
-    (var:X 0 var:Z) :ackermann 1.
-}
-_:gn_11 {
-    (var:Y 1) math:difference var:B.
-    (var:X var:B var:Z) :ackermann var:C.
-    (var:X 1) math:difference var:D.
-    (var:D var:C var:Z) :ackermann var:A.
-}
-_:gn_12 {
-    (var:X var:Y var:Z) :ackermann var:A.
-}
-_:gn_13 {
-    (0 0) :ackermann var:A0.
-    (0 6) :ackermann var:A1.
-    (1 2) :ackermann var:A2.
-    (1 7) :ackermann var:A3.
-    (2 2) :ackermann var:A4.
-    (2 9) :ackermann var:A5.
-    (3 4) :ackermann var:A6.
-    (3 14) :ackermann var:A7.
-    (4 0) :ackermann var:A8.
-    (4 1) :ackermann var:A9.
-    (5 0) :ackermann var:A11.
-}

lingua/output/acp.trig

@@ -1,73 +1,4 @@
 @prefix : <https://eyereasoner.github.io/see-lingua/lingua/acp.trig#>.
-@prefix lingua: <http://www.w3.org/2000/10/swap/lingua#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix log: <http://www.w3.org/2000/10/swap/log#>.
-@prefix list: <http://www.w3.org/2000/10/swap/list#>.
 
 :test :for :PolicyX.
 :test :is true.
-
-:acp_rule1 lingua:body _:gn_1.
-:acp_rule1 lingua:headback _:node_1_1.
-:acp_rule1 lingua:bindings ((var:Test :test1) (var:Pol :PolicyX) (var:Field var:U_0) (var:X ((<https://eyereasoner.github.io/see-lingua/lingua/acp.trig>) 1))).
-:acp_rule2 lingua:body _:gn_2.
-:acp_rule2 lingua:headback _:node_7_1.
-:acp_rule2 lingua:bindings ((var:Test :test1) (var:Pol :PolicyX) (var:Field var:U_1) (var:List (:C)) (var:X ((<https://eyereasoner.github.io/see-lingua/lingua/acp.trig>) 1)) (var:L 1)).
-:acp_rule3 lingua:body _:gn_3.
-:acp_rule3 lingua:headback _:node_13_1.
-:acp_rule3 lingua:bindings ((var:Test :test1) (var:Pol :PolicyX) (var:Field var:U_2) (var:List ()) (var:X ((<https://eyereasoner.github.io/see-lingua/lingua/acp.trig>) 1)) (var:L 0)).
-:acp_query lingua:question _:node_19_1.
-:acp_query lingua:answer _:node_20_1.
-:acp_query lingua:bindings ((var:Pol :PolicyX)).
-_:gn_1 {
-    var:Test :policy var:Pol.
-    var:Pol a :Policy.
-    (_:node_4_1 _:node_6_1) log:forAllIn var:X.
-}
-_:node_1_1 {
-    var:Pol :pass :allOfTest.
-}
-_:gn_2 {
-    var:Test :policy var:Pol.
-    var:Pol a :Policy.
-    (var:Field _:node_11_1 var:List) log:collectAllIn var:X.
-    var:List list:length var:L.
-    var:L log:notEqualTo 0.
-}
-_:node_7_1 {
-    var:Pol :pass :anyOfTest.
-}
-_:gn_3 {
-    var:Test :policy var:Pol.
-    var:Pol a :Policy.
-    (var:Field _:node_17_1 var:List) log:collectAllIn var:X.
-    var:List list:length var:L.
-    var:L log:equalTo 0.
-}
-_:node_13_1 {
-    var:Pol :pass :noneOfTest.
-}
-_:node_19_1 {
-    var:Pol a :Policy.
-    var:Pol :pass :allOfTest.
-    var:Pol :pass :anyOfTest.
-    var:Pol :pass :noneOfTest.
-}
-_:node_20_1 {
-    :test :for var:Pol.
-    :test :is true.
-}
-_:node_4_1 {
-    var:Pol :allOf var:Field.
-}
-_:node_6_1 {
-    var:Test :has var:Field.
-}
-_:node_11_1 {
-    var:Pol :anyOf var:Field.
-    var:Test :has var:Field.
-}
-_:node_17_1 {
-    var:Pol :noneOf var:Field.
-    var:Test :has var:Field.
-}

lingua/output/backward.trig

@@ -1,22 +1,3 @@
 @prefix : <https://eyereasoner.github.io/see-lingua/lingua/backward.trig#>.
-@prefix lingua: <http://www.w3.org/2000/10/swap/lingua#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
-@prefix math: <http://www.w3.org/2000/10/swap/math#>.
 
 ("this" 5) :moreInterestingThan ("that" 3).
-
-:backward_rule lingua:body _:node_2_1.
-:backward_rule lingua:headback _:gn_1.
-:backward_rule lingua:bindings ((var:X 5) (var:Y 3)).
-:query lingua:question _:gn_2.
-:query lingua:answer _:gn_2.
-:query lingua:bindings ().
-_:node_2_1 {
-    var:X math:greaterThan var:Y.
-}
-_:gn_1 {
-    ("this" var:X) :moreInterestingThan ("that" var:Y).
-}
-_:gn_2 {
-    ("this" 5) :moreInterestingThan ("that" 3).
-}

lingua/output/beetle.trig

@@ -1,52 +1,3 @@
 @prefix : <https://eyereasoner.github.io/see-lingua/lingua/beetle.trig#>.
-@prefix lingua: <http://www.w3.org/2000/10/swap/lingua#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 
 :beetle :is :beautiful.
-
-_:rl_12976060 lingua:premise _:gn_1.
-_:rl_12976060 lingua:conclusion _:gn_2.
-_:rl_12976060 lingua:bindings ((var:node_2_1 :beetle)).
-_:rl_1850074 lingua:premise _:gn_1.
-_:rl_1850074 lingua:conclusion _:gn_3.
-_:rl_1850074 lingua:bindings ((var:node_2_1 :beetle)).
-_:rl_3586113 lingua:premise _:gn_1.
-_:rl_3586113 lingua:conclusion _:gn_4.
-_:rl_3586113 lingua:bindings ((var:node_2_1 :beetle)).
-_:rl_9331763 lingua:question _:gn_5.
-_:rl_9331763 lingua:answer _:gn_5.
-_:rl_9331763 lingua:bindings ((var:node_13_1 :beetle) (var:node_15_1 :beautiful)).
-_:rl_7283810 lingua:premise true.
-_:rl_7283810 lingua:conclusion _:gn_6.
-_:rl_7283810 lingua:bindings ().
-_:gn_9 {
-    var:node_2_1 :is :green.
-}
-_:gn_10 {
-    var:node_2_1 :is :blue.
-}
-_:gn_3 {
-    var:node_2_1 :is :beautiful.
-}
-_:gn_1 {
-    var:node_2_1 a :Car.
-}
-_:gn_2 {
-    () lingua:onNegativeSurface _:gn_7.
-}
-_:gn_4 {
-    () lingua:onNegativeSurface _:gn_8.
-}
-_:gn_5 {
-    var:node_13_1 :is var:node_15_1.
-}
-_:gn_6 {
-    :beetle :is :beautiful.
-}
-_:gn_7 {
-    () lingua:onNegativeSurface _:gn_9.
-    () lingua:onNegativeSurface _:gn_10.
-}
-_:gn_8 {
-    () lingua:onNegativeSurface _:gn_3.
-}