From 486311e6fb0a7e887f3b39019fc2ce74806ef6a5 Mon Sep 17 00:00:00 2001
From: josd <josderoo@gmail.com>
Date: Sun, 16 Jun 2024 12:11:50 +0200
Subject: [PATCH] improving on universal quantification

---
 VERSION                                 |  2 +-
 rdfsurfaces/temp/da1-output.s           |  0
 rdfsurfaces/temp/da1.s                  | 11 +++++++++++
 rdfsurfaces/temp/test                   |  5 +++++
 rdfsurfaces/temp/universal_1_d-output.s |  1 +
 rdfsurfaces/temp/universal_1_d.s        | 10 ++++++++++
 rdfsurfaces/temp/universal_4_d-output.s |  1 +
 rdfsurfaces/temp/universal_4_d.s        |  9 +++++++++
 rdfsurfaces/temp/universal_5_s-output.s |  0
 rdfsurfaces/temp/universal_5_s.s        | 11 +++++++++++
 rdfsurfaces/temp/universal_6_d-output.s |  0
 rdfsurfaces/temp/universal_6_d.s        | 11 +++++++++++
 retina.pl                               | 19 +++++++++++++++----
 13 files changed, 75 insertions(+), 5 deletions(-)
 create mode 100644 rdfsurfaces/temp/da1-output.s
 create mode 100644 rdfsurfaces/temp/da1.s
 create mode 100755 rdfsurfaces/temp/test
 create mode 100644 rdfsurfaces/temp/universal_1_d-output.s
 create mode 100644 rdfsurfaces/temp/universal_1_d.s
 create mode 100644 rdfsurfaces/temp/universal_4_d-output.s
 create mode 100644 rdfsurfaces/temp/universal_4_d.s
 create mode 100644 rdfsurfaces/temp/universal_5_s-output.s
 create mode 100644 rdfsurfaces/temp/universal_5_s.s
 create mode 100644 rdfsurfaces/temp/universal_6_d-output.s
 create mode 100644 rdfsurfaces/temp/universal_6_d.s

diff --git a/VERSION b/VERSION
index d50359d..7acd1cb 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-5.5.0
+5.5.1
diff --git a/rdfsurfaces/temp/da1-output.s b/rdfsurfaces/temp/da1-output.s
new file mode 100644
index 0000000..e69de29
diff --git a/rdfsurfaces/temp/da1.s b/rdfsurfaces/temp/da1.s
new file mode 100644
index 0000000..10a07d8
--- /dev/null
+++ b/rdfsurfaces/temp/da1.s
@@ -0,0 +1,11 @@
+flag('quantify', 'https://eyereasoner.github.io/.well-known/genid/822db0e3-f01d-42ee-ba15-84359eb9c346#').
+scope('<file:///home/jdroo/temp/da1.n3s>').
+pfx('log:', '<http://www.w3.org/2000/10/swap/log#>').
+pfx(:, '<http://example.org/ns#>').
+:- dynamic('<http://example.org/ns#is>'/2).
+'<http://example.org/ns#is>'('<http://example.org/ns#sun>', '<http://example.org/ns#shining>').
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], ('<http://example.org/ns#is>'('<http://example.org/ns#sun>', '<http://example.org/ns#shining>'), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(['<https://eyereasoner.github.io/.well-known/genid/822db0e3-f01d-42ee-ba15-84359eb9c346#e_y_1_1_1>'], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/822db0e3-f01d-42ee-ba15-84359eb9c346#e_y_1_1_1>', '<http://example.org/ns#happy>')))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], ('<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/822db0e3-f01d-42ee-ba15-84359eb9c346#e_y_1>', '<http://example.org/ns#happy>'), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#Working>')))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#Working>')).
+scount(4).
+end_of_file.
diff --git a/rdfsurfaces/temp/test b/rdfsurfaces/temp/test
new file mode 100755
index 0000000..1be8506
--- /dev/null
+++ b/rdfsurfaces/temp/test
@@ -0,0 +1,5 @@
+#!/bin/bash
+for f in *.s
+do
+    ../../retina $f | tee ${f%.s}-output.s
+done
diff --git a/rdfsurfaces/temp/universal_1_d-output.s b/rdfsurfaces/temp/universal_1_d-output.s
new file mode 100644
index 0000000..0a5ab56
--- /dev/null
+++ b/rdfsurfaces/temp/universal_1_d-output.s
@@ -0,0 +1 @@
+inference_fuse('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([],'<http://example.org/ns#is>'('<http://example.org/ns#This>','<http://example.org/ns#working>')),'<http://example.org/ns#is>'('<http://example.org/ns#This>','<http://example.org/ns#working>')).
diff --git a/rdfsurfaces/temp/universal_1_d.s b/rdfsurfaces/temp/universal_1_d.s
new file mode 100644
index 0000000..e44cfae
--- /dev/null
+++ b/rdfsurfaces/temp/universal_1_d.s
@@ -0,0 +1,10 @@
+flag('quantify', 'https://eyereasoner.github.io/.well-known/genid/d7128d35-6347-4b72-b714-ffda03f0e782#').
+scope('<file:///home/jdroo/github.com/RebekkaMa/rs2fol/examples/sequent-calculus/combined-rules/universal-quantification/universal_1_d.n3s>').
+pfx('log:', '<http://www.w3.org/2000/10/swap/log#>').
+pfx(:, '<http://example.org/ns#>').
+:- dynamic('<http://example.org/ns#is>'/2).
+'<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#working1>').
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(['<https://eyereasoner.github.io/.well-known/genid/d7128d35-6347-4b72-b714-ffda03f0e782#e_x_1_1>', '<https://eyereasoner.github.io/.well-known/genid/d7128d35-6347-4b72-b714-ffda03f0e782#e_y_1_1>'], ('<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/d7128d35-6347-4b72-b714-ffda03f0e782#e_x_1_1>', '<http://example.org/ns#working1>'), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/d7128d35-6347-4b72-b714-ffda03f0e782#e_y_1_1>', '<http://example.org/ns#working>')))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#working>')).
+scount(3).
+end_of_file.
diff --git a/rdfsurfaces/temp/universal_4_d-output.s b/rdfsurfaces/temp/universal_4_d-output.s
new file mode 100644
index 0000000..0a5ab56
--- /dev/null
+++ b/rdfsurfaces/temp/universal_4_d-output.s
@@ -0,0 +1 @@
+inference_fuse('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([],'<http://example.org/ns#is>'('<http://example.org/ns#This>','<http://example.org/ns#working>')),'<http://example.org/ns#is>'('<http://example.org/ns#This>','<http://example.org/ns#working>')).
diff --git a/rdfsurfaces/temp/universal_4_d.s b/rdfsurfaces/temp/universal_4_d.s
new file mode 100644
index 0000000..f7a385d
--- /dev/null
+++ b/rdfsurfaces/temp/universal_4_d.s
@@ -0,0 +1,9 @@
+flag('quantify', 'https://eyereasoner.github.io/.well-known/genid/db7ad07a-838d-49e8-8188-13aa9ad1c28d#').
+scope('<file:///home/jdroo/github.com/RebekkaMa/rs2fol/examples/sequent-calculus/combined-rules/universal-quantification/universal_4_d.n3s>').
+pfx('log:', '<http://www.w3.org/2000/10/swap/log#>').
+pfx(:, '<http://example.org/ns#>').
+:- dynamic('<http://example.org/ns#is>'/2).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(['<https://eyereasoner.github.io/.well-known/genid/db7ad07a-838d-49e8-8188-13aa9ad1c28d#e_x_1_1>'], '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/db7ad07a-838d-49e8-8188-13aa9ad1c28d#e_x_1_1>', '<http://example.org/ns#working>'))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#working>')).
+scount(2).
+end_of_file.
diff --git a/rdfsurfaces/temp/universal_5_s-output.s b/rdfsurfaces/temp/universal_5_s-output.s
new file mode 100644
index 0000000..e69de29
diff --git a/rdfsurfaces/temp/universal_5_s.s b/rdfsurfaces/temp/universal_5_s.s
new file mode 100644
index 0000000..dcd3fa9
--- /dev/null
+++ b/rdfsurfaces/temp/universal_5_s.s
@@ -0,0 +1,11 @@
+flag('quantify', 'https://eyereasoner.github.io/.well-known/genid/37061b6c-295a-4019-9ebe-37c457e3f637#').
+scope('<file:///home/jdroo/github.com/RebekkaMa/rs2fol/examples/sequent-calculus/combined-rules/universal-quantification/universal_5_s.n3s>').
+pfx('log:', '<http://www.w3.org/2000/10/swap/log#>').
+pfx(:, '<http://example.org/ns#>').
+:- dynamic('<http://example.org/ns#is>'/2).
+'<http://example.org/ns#is>'('<http://example.org/ns#sun>', '<http://example.org/ns#shining>').
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], ('<http://example.org/ns#is>'('<http://example.org/ns#sun>', '<http://example.org/ns#shining>'), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(['<https://eyereasoner.github.io/.well-known/genid/37061b6c-295a-4019-9ebe-37c457e3f637#e_y_1_1_1>'], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/37061b6c-295a-4019-9ebe-37c457e3f637#e_y_1_1_1>', '<http://example.org/ns#happy>')))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], ('<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/37061b6c-295a-4019-9ebe-37c457e3f637#e_y_1>', '<http://example.org/ns#happy>'), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#Working>')))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#Working>')).
+scount(4).
+end_of_file.
diff --git a/rdfsurfaces/temp/universal_6_d-output.s b/rdfsurfaces/temp/universal_6_d-output.s
new file mode 100644
index 0000000..e69de29
diff --git a/rdfsurfaces/temp/universal_6_d.s b/rdfsurfaces/temp/universal_6_d.s
new file mode 100644
index 0000000..d7d516f
--- /dev/null
+++ b/rdfsurfaces/temp/universal_6_d.s
@@ -0,0 +1,11 @@
+flag('quantify', 'https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#').
+scope('<file:///home/jdroo/github.com/RebekkaMa/rs2fol/examples/sequent-calculus/combined-rules/universal-quantification/universal_6_d.n3s>').
+pfx('log:', '<http://www.w3.org/2000/10/swap/log#>').
+pfx(:, '<http://example.org/ns#>').
+:- dynamic('<http://example.org/ns#is>'/2).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(['<https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#e_x_1_1>', '<https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#e_y_1_1>'], ('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#e_x_1_1>', '<http://example.org/ns#working>')), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#e_y_1_1>', '<http://example.org/ns#working>')))).
+:- dynamic('<http://example.org/ns#are>'/2).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], ('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(['<https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#e_x_1_2_1>'], '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#is>'('<https://eyereasoner.github.io/.well-known/genid/f4084590-ffee-4d6a-824b-6ec1ee522069#e_x_1_2_1>', '<http://example.org/ns#working>'))), '<http://example.org/ns#is>'('<http://example.org/ns#This>', '<http://example.org/ns#working>'), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#are>'('<http://example.org/ns#we>', '<http://example.org/ns#happy>')))).
+'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], '<http://example.org/ns#are>'('<http://example.org/ns#we>', '<http://example.org/ns#happy>')).
+scount(3).
+end_of_file.
diff --git a/retina.pl b/retina.pl
index 5645128..bbf076e 100644
--- a/retina.pl
+++ b/retina.pl
@@ -25,7 +25,7 @@
 :- dynamic('<http://www.w3.org/2000/10/swap/log#onNegativeComponentSurface>'/2).
 :- dynamic('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'/2).
 
-version_info('retina v5.5.0 (2024-06-01)').
+version_info('retina v5.5.1 (2024-06-16)').
 
 % run
 run :-
@@ -390,8 +390,17 @@
         list_si(V),
         conj_list(G, L),
         list_to_set(L, B),
-        select('<http://www.w3.org/2000/10/swap/log#onNegativeComponentSurface>'(Z, T), B, K),
-        list_si(Z),
+        (   select('<http://www.w3.org/2000/10/swap/log#onNegativeComponentSurface>'([], T), B, K)
+        ;   select('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'([], T), B, K),
+            conj_list(T, [T]),
+            \+member('<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, _), K),
+            \+member('<http://www.w3.org/2000/10/swap/log#onNegativeComponentSurface>'(_, _), K),
+            \+member('<http://www.w3.org/2000/10/swap/log#onNegativeAnswerSurface>'(_, _), K),
+            findvars(T, Tv),
+            findvars(K, Kv),
+            member(Tm, Tv),
+            \+member(Tm, Kv)
+        ),
         conj_list(R, K),
         conjify(R, S),
         find_graffiti([R], D),
@@ -995,7 +1004,9 @@
     atomic(A),
     !,
     (   atom(A),
-        sub_atom(A, 0, 2, _, '_:')
+        (   sub_atom(A, 0, 2, _, '_:')
+        ;   sub_atom(A, _, 19, _, '/.well-known/genid/')
+        )
     ->  B = [A]
     ;   B = []
     ).