refreshing

eyereasoner · Nov 9, 2024 · ab7343e · ab7343e
1 parent d855925
commit ab7343e
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 10 deletions.
diff --git a/color/peasant-multiplication/peasant-multiplication-proof.n3 b/color/peasant-multiplication/peasant-multiplication-proof.n3
@@ -73,7 +73,7 @@ skolem:lemma5 a r:Extraction;
             (3 0) :prod var:x_0.
         }.
     };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication.n3>].
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication-query.n3>].
 
 skolem:lemma6 a r:Inference;
     r:gives {
@@ -103,7 +103,7 @@ skolem:lemma7 a r:Extraction;
             (5 6) :prod var:x_0.
         }.
     };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication.n3>].
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication-query.n3>].
 
 skolem:lemma8 a r:Inference;
     r:gives {
@@ -131,7 +131,7 @@ skolem:lemma9 a r:Extraction;
             (238 13) :prod var:x_0.
         }.
     };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication.n3>].
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication-query.n3>].
 
 skolem:lemma10 a r:Inference;
     r:gives {

diff --git a/color/peasant-multiplication/peasant-multiplication-query.n3 b/color/peasant-multiplication/peasant-multiplication-query.n3
@@ -0,0 +1,6 @@
+@prefix : <http://eexample.org/#>.
+
+# query
+{(3 0) :prod ?Z} => {(3 0) :prod ?Z}.
+{(5 6) :prod ?Z} => {(5 6) :prod ?Z}.
+{(238 13) :prod ?Z} => {(238 13) :prod ?Z}.
diff --git a/color/peasant-multiplication/peasant-multiplication.n3 b/color/peasant-multiplication/peasant-multiplication.n3
@@ -4,8 +4,3 @@
 {(0 ?Y) :prod 0} <= true.
 {(?X ?Y) :prod ?Z} <= {?X math:notEqualTo 0. (?X 2) math:remainder 0. ((?X 2)!math:integerQuotient (?Y ?Y)!math:sum) :prod ?Z}.
 {(?X ?Y) :prod ?Z} <= {?X math:notEqualTo 0. (?X 2) math:remainder 1. (((?X 2)!math:integerQuotient (?Y ?Y)!math:sum)!:prod ?Y) math:sum ?Z}.
-
-# query
-{(3 0) :prod ?Z} =^ {(3 0) :prod ?Z}.
-{(5 6) :prod ?Z} =^ {(5 6) :prod ?Z}.
-{(238 13) :prod ?Z} =^ {(238 13) :prod ?Z}.
diff --git a/color/peasant-multiplication/test b/color/peasant-multiplication/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/peasant-multiplication/peasant-multiplication.n3 --output peasant-multiplication-answer.n3
-eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication.n3 --output peasant-multiplication-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/peasant-multiplication/peasant-multiplication.n3 --query https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication-query.n3 --output peasant-multiplication-answer.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/color .. https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication.n3 --query https://eyereasoner.github.io/eye/color/peasant-multiplication/peasant-multiplication-query.n3 --output peasant-multiplication-proof.n3