adding non-unit resolution for blogic

eyereasoner · Feb 15, 2023 · 9792285 · 9792285
1 parent 4273854
commit 9792285
Show file tree

Hide file tree

Showing 16 changed files with 59 additions and 16 deletions.
diff --git a/RELEASE b/RELEASE
@@ -1,5 +1,6 @@
                                   EYE release
 
+[v2.11.0] adding non-unit resolution for blogic
 [v2.10.3] adding blogic negative surface redundancy removal
 [v2.10.2] using log:onQuerySurface instead of log:onConstructSurface
 [v2.10.1] fixing https://github.com/eyereasoner/Notation3-By-Example/blob/main/log/blogic/negativeSurface3.n3

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-2.10.3
+2.11.0
diff --git a/eye.pl b/eye.pl
@@ -20,7 +20,7 @@
 :- use_module(library(semweb/turtle)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v2.10.3 josd').
+version_info('EYE v2.11.0 josd').
 
 license_info('MIT License
 
@@ -740,6 +740,28 @@
                     ->  assertz('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, H))
                     ;   true
                     )), true, '<>')),
+    % non-unit resolution
+    assertz(implies(('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, G),
+                    conj_list(G, L),
+                    \+member('<http://www.w3.org/2000/10/swap/log#onPositiveSurface>'(_, _), L),
+                    \+member('<http://www.w3.org/2000/10/swap/log#onQuerySurface>'(_, _), L),
+                    findall(1,
+                        (   member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _), L)
+                        ),
+                        D
+                    ),
+                    length(D, E),
+                    E < 4,
+                    '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, F),
+                    conj_list(F, K),
+                    length(K, 2),
+                    select('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(U, C), K, [P]),
+                    select('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, P), L, M),
+                    conj_list(H, ['<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(U, C)|M]),
+                    (   \+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, H)
+                    ->  assertz('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, H))
+                    ;   true
+                    )), true, '<>')),
     % adjust graffiti
     assertz(implies(('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, G),
                     findvars(G, U, beta),

diff --git a/eye.zip b/eye.zip
diff --git a/reasoning/blogic/beetle.n3 b/reasoning/blogic/beetle.n3
@@ -32,6 +32,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :beetle :is :beautiful.
+(_:S _:O) log:onQuerySurface {
+    _:S :is _:O.
 }.
diff --git a/reasoning/blogic/beetle10a-answer.n3 b/reasoning/blogic/beetle10a-answer.n3
@@ -40,6 +40,14 @@ log:onNegativeSurface :is :beautiful.
         _:e_O_1 a rdfs:Resource.
     }.
 } :is :beautiful.
+{
+    () log:onNegativeSurface {
+        _:e_A_1 :is :beautiful.
+    }.
+    () log:onNegativeSurface {
+        _:e_A_1 :is :beautiful.
+    }.
+} :is :beautiful.
 (_:e_S_1 _:e_O_1) :is :beautiful.
 log:onQuerySurface :is :beautiful.
 {

diff --git a/reasoning/blogic/beetle12.n3 b/reasoning/blogic/beetle12.n3
@@ -129,6 +129,9 @@
 }.
 
 # query
+# (_:S _:O) log:onQuerySurface {
+#     _:S :is _:O.
+# }
 () log:onAskSurface {
     :beetle :is :beautiful.
 }.
diff --git a/reasoning/blogic/beetle12a.n3 b/reasoning/blogic/beetle12a.n3
@@ -45,6 +45,9 @@
 }.
 
 # query
+# (_:S _:O) log:onQuerySurface {
+#     _:S :is _:O.
+# }
 () log:onAskSurface {
     :beetle :is :beautiful.
 }.
diff --git a/reasoning/blogic/beetle14.n3 b/reasoning/blogic/beetle14.n3
@@ -28,6 +28,9 @@
 }.
 
 # query
+# (_:S _:O) log:onQuerySurface {
+#     _:S :is _:O.
+# }
 () log:onAskSurface {
     :herbie :is :beautiful.
 }.
diff --git a/reasoning/blogic/beetle2.n3 b/reasoning/blogic/beetle2.n3
@@ -43,6 +43,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :beetle :is :beautiful.
+(_:S _:O) log:onQuerySurface {
+    _:S :is _:O.
 }.
diff --git a/reasoning/blogic/beetle3.n3 b/reasoning/blogic/beetle3.n3
@@ -40,6 +40,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :beetle :is :beautiful.
+(_:S _:O) log:onQuerySurface {
+    _:S :is _:O.
 }.
diff --git a/reasoning/blogic/beetle4.n3 b/reasoning/blogic/beetle4.n3
@@ -40,6 +40,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :beetle :is :beautiful.
+(_:S _:O) log:onQuerySurface {
+    _:S :is _:O.
 }.
diff --git a/reasoning/blogic/beetle5.n3 b/reasoning/blogic/beetle5.n3
@@ -51,6 +51,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :beetle :is :beautiful.
+(_:S _:O) log:onQuerySurface {
+    _:S :is _:O.
 }.
diff --git a/reasoning/blogic/beetle8.n3 b/reasoning/blogic/beetle8.n3
@@ -40,6 +40,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :beetle :is :beautiful.
+(_:S _:O) log:onQuerySurface {
+    _:S :is _:O.
 }.
diff --git a/reasoning/blogic/beetle9.n3 b/reasoning/blogic/beetle9.n3
@@ -32,6 +32,9 @@
 }.
 
 # query
+# (_:S _:O) log:onQuerySurface {
+#     _:S :is _:O.
+# }
 () log:onAskSurface {
     :beetle :is :beautiful.
 }.
diff --git a/reasoning/blogic/disj-elim.n3 b/reasoning/blogic/disj-elim.n3
@@ -32,6 +32,6 @@
 }.
 
 # query
-() log:onAskSurface {
-    :bob :saying :C.
+(_:S _:O) log:onQuerySurface {
+    _:S :saying _:O.
 }.