adding collatz case

eyereasoner · Jan 6, 2025 · eebbe3d · eebbe3d
1 parent 4ad4b8b
commit eebbe3d
Show file tree

Hide file tree

Showing 6 changed files with 17,929 additions and 0 deletions.
diff --git a/reasoning/collatz/README b/reasoning/collatz/README
@@ -0,0 +1,5 @@
+------------------
+Collatz conjecture
+------------------
+
+See https://en.wikipedia.org/wiki/Collatz_conjecture
diff --git a/reasoning/collatz/collatz-answer.n3 b/reasoning/collatz/collatz-answer.n3
diff --git a/reasoning/collatz/collatz-proof.n3 b/reasoning/collatz/collatz-proof.n3
diff --git a/reasoning/collatz/collatz-query.n3 b/reasoning/collatz/collatz-query.n3
@@ -0,0 +1,11 @@
+@prefix math: <http://www.w3.org/2000/10/swap/math#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <urn:example:>.
+
+{
+    256 log:repeat ?N0.
+    (?N0 1) math:sum ?N.
+    ?N :collatz (1 ?M).
+} => {
+    ?N :collatz (1 ?M).
+}.
diff --git a/reasoning/collatz/collatz.n3 b/reasoning/collatz/collatz.n3
@@ -0,0 +1,17 @@
+@prefix math: <http://www.w3.org/2000/10/swap/math#>.
+@prefix list: <http://www.w3.org/2000/10/swap/list#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <urn:example:>.
+
+{ ?N :collatz (?N (?N)) } <= {
+    true log:callWithCut true.
+}.
+
+{ ?N0 :collatz (?N ?M)} <= {
+    (   { (?N0 2) math:remainder 0 }
+        { (?N0 2) math:integerQuotient ?N1 }
+        { ((3 ?N0)!math:product 1) math:sum ?N1 }
+    ) log:ifThenElseIn ?SCOPE.
+    ?N1 :collatz (?N ?J).
+    ?M list:firstRest (?N0 ?J).
+}.
diff --git a/reasoning/collatz/test b/reasoning/collatz/test
@@ -0,0 +1,3 @@
+#!/bin/bash
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/collatz/collatz.n3 --query https://eyereasoner.github.io/eye/reasoning/collatz/collatz-query.n3 --output collatz-answer.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/collatz/collatz.n3 --query https://eyereasoner.github.io/eye/reasoning/collatz/collatz-query.n3 --output collatz-proof.n3