improving on universal quantification

VERSION

@@ -1 +1 @@
-5.5.0
+5.5.1

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.

rdfsurfaces/temp/test

@@ -0,0 +1,5 @@
+#!/bin/bash
+for f in *.s
+do
+    ../../retina $f | tee ${f%.s}-output.s
+done

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>')).

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.

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>')).

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.

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.

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.

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 = []
     ).