refreshing

eyereasoner · Feb 28, 2025 · 4ddad65 · 4ddad65
1 parent 13a3a26
commit 4ddad65
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 20 deletions.
diff --git a/reasoning/good-cobbler/cobbler-answer.n3 b/reasoning/good-cobbler/cobbler-answer.n3
@@ -2,4 +2,4 @@
 @prefix log: <http://www.w3.org/2000/10/swap/log#>.
 
 :joe :is _:sk_0.
-("good(_X)" :Cobbler) log:term _:sk_0.
+("good(_)" :Cobbler) log:term _:sk_0.
diff --git a/reasoning/good-cobbler/cobbler-proof.n3 b/reasoning/good-cobbler/cobbler-proof.n3
@@ -9,44 +9,52 @@ skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma1;
     r:gives {
         :joe :is _:sk_0.
-        ("good(_X)" :Cobbler) log:term _:sk_0.
+        ("good(_)" :Cobbler) log:term _:sk_0.
     }.
 
 skolem:lemma1 a r:Inference;
     r:gives {
         :joe :is _:sk_0.
-        ("good(_X)" :Cobbler) log:term _:sk_0.
+        ("good(_)" :Cobbler) log:term _:sk_0.
     };
     r:evidence (
         skolem:lemma2
-        skolem:lemma3
+        [ a r:Fact; r:gives {("good(_)" :Cobbler) log:term "good('<https://eyereasoner.github.io/ns#Cobbler>')"}]
     );
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/ns#joe"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ a r:Existential; n3:nodeId "https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#e_2"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo "good('<https://eyereasoner.github.io/ns#Cobbler>')"];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/ns#Cobbler"]];
-    r:rule skolem:lemma4.
+    r:rule skolem:lemma3.
 
-skolem:lemma2 a r:Extraction;
+skolem:lemma2 a r:Inference;
     r:gives {
-        :joe :is skolem:e_2.
+        :joe :is "good('<https://eyereasoner.github.io/ns#Cobbler>')".
     };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/good-cobbler/cobbler.n3>].
+    r:evidence (
+        [ a r:Fact; r:gives {("good(_X)" :Cobbler) log:term "good('<https://eyereasoner.github.io/ns#Cobbler>')"}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo "good('<https://eyereasoner.github.io/ns#Cobbler>')"];
+    r:rule skolem:lemma4.
 
 skolem:lemma3 a r:Extraction;
-    r:gives {
-        ("good(_X)" :Cobbler) log:term skolem:e_2.
-    };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/good-cobbler/cobbler.n3>].
-
-skolem:lemma4 a r:Extraction;
     r:gives {
         @forAll var:x_0, var:x_1, var:x_2. @forSome var:x_3. {
             var:x_0 :is var:x_1.
-            ("good(_X)" var:x_2) log:term var:x_1.
+            ("good(_)" var:x_2) log:term var:x_1.
         } => {
             var:x_0 :is var:x_3.
-            ("good(_X)" var:x_2) log:term var:x_3.
+            ("good(_)" var:x_2) log:term var:x_3.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/good-cobbler/cobbler-query.n3>].
 
+skolem:lemma4 a r:Extraction;
+    r:gives {
+        @forAll var:x_0. {
+            ("good(_X)" :Cobbler) log:term var:x_0.
+        } => {
+            :joe :is var:x_0.
+        }.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/good-cobbler/cobbler.n3>].
+
diff --git a/reasoning/good-cobbler/cobbler-query.n3 b/reasoning/good-cobbler/cobbler-query.n3
@@ -3,7 +3,7 @@
 
 # is there some x which is good at some y
 {
-    ?x :is ("good(_X)" ?Y)!log:term.
+    ?x :is ("good(_)" ?Y)!log:term.
 } => {
-    ?x :is ("good(_X)" ?Y)!log:term.
+    ?x :is ("good(_)" ?Y)!log:term.
 }.
diff --git a/reasoning/good-cobbler/cobbler.n3 b/reasoning/good-cobbler/cobbler.n3
@@ -6,4 +6,4 @@
 @prefix : <https://eyereasoner.github.io/ns#>.
 
 # joe is a good cobbler
-:joe :is ("good(_X)" :Cobbler)!log:term.
+{ ("good(_X)" :Cobbler) log:term ?Term } => { :joe :is ?Term }.