refreshing

eyereasoner · Nov 9, 2024 · 3df38da · 3df38da
1 parent b6f3938
commit 3df38da
Show file tree

Hide file tree

Showing 8 changed files with 26 additions and 24 deletions.
diff --git a/color/eulers-identity/eulers-identity-proof.n3 b/color/eulers-identity/eulers-identity-proof.n3
@@ -92,7 +92,7 @@ skolem:lemma4 a r:Extraction;
             ((var:x_0 var:x_1) (1 0)) complex:sum (var:x_2 var:x_3).
         }.
     };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity.n3>].
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity-query.n3>].
 
 skolem:lemma5 a r:Inference;
     r:gives {

diff --git a/color/eulers-identity/eulers-identity-query.n3 b/color/eulers-identity/eulers-identity-query.n3
@@ -0,0 +1,10 @@
+@prefix complex: <http://eyereasoner.github.io/eye/complex#>.
+
+# query
+{
+    ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation (?A ?B).
+    ((?A ?B) (1 0)) complex:sum (?C ?D).
+} => {
+    ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation (?A ?B).
+    ((?A ?B) (1 0)) complex:sum (?C ?D).
+}.
diff --git a/color/eulers-identity/eulers-identity.n3 b/color/eulers-identity/eulers-identity.n3
@@ -62,12 +62,3 @@
     (3.141592653589793 2) math:product ?Z1.
     (?Z1 ?T) math:difference ?Tp.
 }.
-
-# query
-{
-    ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation (?A ?B).
-    ((?A ?B) (1 0)) complex:sum (?C ?D).
-} =^ {
-    ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation (?A ?B).
-    ((?A ?B) (1 0)) complex:sum (?C ?D).
-}.
diff --git a/color/eulers-identity/test b/color/eulers-identity/test
@@ -1,3 +1,3 @@
 #!/bin/bash
-eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. --nope https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity.n3 --output eulers-identity-answer.n3
-eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity.n3 --output eulers-identity-proof.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. --nope https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity.n3 --query https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity-query.n3 --output eulers-identity-answer.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity.n3 --query https://eyereasoner.github.io/eye/color/eulers-identity/eulers-identity-query.n3 --output eulers-identity-proof.n3
diff --git a/color/peano/peano-proof.n3 b/color/peano/peano-proof.n3
@@ -71,7 +71,7 @@ skolem:lemma5 a r:Extraction;
             var:x_1 :factorial var:x_2.
         }.
     };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peano/peano.n3>].
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peano/peano-query.n3>].
 
 skolem:lemma6 a r:Inference;
     r:gives {

diff --git a/color/peano/peano-query.n3 b/color/peano/peano-query.n3
@@ -0,0 +1,10 @@
+@prefix : <http://example.org/#>.
+
+# query
+{
+    ((:s 0) (:s (:s 0))) :multiply ?A.
+    (?A (:s (:s (:s 0)))) :add ?B.
+    ?B :factorial ?C.
+} => {
+    ?B :factorial ?C.
+}.
diff --git a/color/peano/peano.n3 b/color/peano/peano.n3
@@ -27,12 +27,3 @@
     (?B (:s ?A)) :multiply ?D.
     (?A ?D) :fac ?C.
 }.
-
-# query
-{
-    ((:s 0) (:s (:s 0))) :multiply ?A.
-    (?A (:s (:s (:s 0)))) :add ?B.
-    ?B :factorial ?C.
-} =^ {
-    ?B :factorial ?C.
-}.
diff --git a/color/peano/test b/color/peano/test
@@ -1,3 +1,3 @@
 #!/bin/bash
-eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. --nope https://eyereasoner.github.io/eye/color/peano/peano.n3 --output peano-answer.n3
-eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. https://eyereasoner.github.io/eye/color/peano/peano.n3 --output peano-proof.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. --nope https://eyereasoner.github.io/eye/color/peano/peano.n3 --query https://eyereasoner.github.io/eye/color/peano/peano-query.n3 --output peano-answer.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. https://eyereasoner.github.io/eye/color/peano/peano.n3 --query https://eyereasoner.github.io/eye/color/peano/peano-query.n3 --output peano-proof.n3