adding proof by cases example

eyereasoner · Dec 11, 2024 · 1e35a80 · 1e35a80
1 parent a772ec3
commit 1e35a80
Show file tree

Hide file tree

Showing 6 changed files with 231 additions and 0 deletions.
diff --git a/reasoning/proof-by-cases/README b/reasoning/proof-by-cases/README
@@ -0,0 +1,5 @@
+--------------
+Proof by cases
+--------------
+
+See https://en.wikipedia.org/wiki/Proof_by_exhaustion
diff --git a/reasoning/proof-by-cases/example1-answer.n3 b/reasoning/proof-by-cases/example1-answer.n3
@@ -0,0 +1,5 @@
+@prefix : <urn:example:>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+
+:theorem1 :isProvenFor var:X.
+:theorem3 :isProvenFor var:X.
diff --git a/reasoning/proof-by-cases/example1-proof.n3 b/reasoning/proof-by-cases/example1-proof.n3
@@ -0,0 +1,170 @@
+@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
+@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+@prefix : <urn:example:>.
+@prefix n3: <http://www.w3.org/2004/06/rei#>.
+@prefix list: <http://www.w3.org/2000/10/swap/list#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+
+skolem:proof a r:Proof, r:Conjunction;
+    r:component skolem:lemma1;
+    r:component skolem:lemma2;
+    r:gives {
+        @forSome var:X. :theorem1 :isProvenFor var:X.
+        @forSome var:X. :theorem3 :isProvenFor var:X.
+    }.
+
+skolem:lemma1 a r:Inference;
+    r:gives {
+        @forSome var:X. :theorem1 :isProvenFor var:X.
+    };
+    r:evidence (
+        skolem:lemma3
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:theorem1"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/var#X"]];
+    r:rule skolem:lemma4.
+
+skolem:lemma2 a r:Inference;
+    r:gives {
+        @forSome var:X. :theorem3 :isProvenFor var:X.
+    };
+    r:evidence (
+        skolem:lemma5
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:theorem3"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/var#X"]];
+    r:rule skolem:lemma4.
+
+skolem:lemma3 a r:Inference;
+    r:gives {
+        @forSome var:X. :theorem1 :isProvenFor var:X.
+    };
+    r:evidence (
+        skolem:lemma6
+        skolem:lemma7
+        [ a r:Fact; r:gives {@forSome var:X. ({
+            ({
+                var:X a :Negative.
+            } {
+                var:X a :Zero.
+            } {
+                var:X a :Positive.
+            }) list:member {
+                var:X a _:sk_0.
+            }.
+        } {
+            {
+                var:X a _:sk_0.
+            } => {
+                :theorem1 :isProvenFor var:X.
+            }.
+        }) log:forAllIn ((<https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>) 1)}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({
+        var:X a :Negative.
+    } {
+        var:X a :Zero.
+    } {
+        var:X a :Positive.
+    })];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/var#X"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:theorem1"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
+    r:rule skolem:lemma8.
+
+skolem:lemma4 a r:Extraction;
+    r:gives {
+        @forAll var:x_0, var:x_1. {
+            var:x_0 :isProvenFor var:x_1.
+        } => {
+            var:x_0 :isProvenFor var:x_1.
+        }.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1-query.n3>].
+
+skolem:lemma5 a r:Inference;
+    r:gives {
+        @forSome var:X. :theorem3 :isProvenFor var:X.
+    };
+    r:evidence (
+        skolem:lemma6
+        skolem:lemma9
+        [ a r:Fact; r:gives {@forSome var:X. ({
+            ({
+                var:X a :Negative.
+            } {
+                var:X a :Zero.
+            } {
+                var:X a :Positive.
+            }) list:member {
+                var:X a _:sk_1.
+            }.
+        } {
+            {
+                var:X a _:sk_1.
+            } => {
+                :theorem3 :isProvenFor var:X.
+            }.
+        }) log:forAllIn ((<https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>) 1)}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({
+        var:X a :Negative.
+    } {
+        var:X a :Zero.
+    } {
+        var:X a :Positive.
+    })];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/var#X"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:theorem3"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_1"]];
+    r:rule skolem:lemma8.
+
+skolem:lemma6 a r:Extraction;
+    r:gives {
+        @forSome var:X. (var:X) log:allPossibleCases ({
+            var:X a :Negative.
+        } {
+            var:X a :Zero.
+        } {
+            var:X a :Positive.
+        }).
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>].
+
+skolem:lemma7 a r:Extraction;
+    r:gives {
+        :theorem1 a :Theorem.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>].
+
+skolem:lemma8 a r:Extraction;
+    r:gives {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. {
+            (var:x_0) log:allPossibleCases var:x_1.
+            var:x_2 a :Theorem.
+            ({
+                var:x_1 list:member {
+                    var:x_0 a var:x_3.
+                }.
+            } {
+                {
+                    var:x_0 a var:x_3.
+                } => {
+                    var:x_2 :isProvenFor var:x_0.
+                }.
+            }) log:forAllIn var:x_4.
+        } => {
+            var:x_2 :isProvenFor var:x_0.
+        }.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>].
+
+skolem:lemma9 a r:Extraction;
+    r:gives {
+        :theorem3 a :Theorem.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3>].
+
diff --git a/reasoning/proof-by-cases/example1-query.n3 b/reasoning/proof-by-cases/example1-query.n3
@@ -0,0 +1,8 @@
+@prefix : <urn:example:>.
+
+# query
+{
+    ?T :isProvenFor ?X.
+} => {
+    ?T :isProvenFor ?X.
+}.
diff --git a/reasoning/proof-by-cases/example1.n3 b/reasoning/proof-by-cases/example1.n3
@@ -0,0 +1,40 @@
+@prefix list: <http://www.w3.org/2000/10/swap/list#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
+@prefix : <urn:example:>.
+
+# closed set of possible cases
+(var:X) log:allPossibleCases (
+    { var:X a :Negative }
+    { var:X a :Zero }
+    { var:X a :Positive }
+).
+
+# theorems
+:theorem1 a :Theorem.
+:theorem2 a :Theorem.
+:theorem3 a :Theorem.
+
+# prove for possible cases
+{ ?X a :Negative } => { :theorem1 :isProvenFor ?X }.
+{ ?X a :Zero } => { :theorem1 :isProvenFor ?X }.
+{ ?X a :Positive } => { :theorem1 :isProvenFor ?X }.
+
+{ ?X a :Negative } => { :theorem2 :isProvenFor ?X }.
+{ ?X a :Positive } => { :theorem2 :isProvenFor ?X }.
+
+{ ?X a :Negative } => { :theorem3 :isProvenFor ?X }.
+{ ?X a :Zero } => { :theorem3 :isProvenFor ?X }.
+{ ?X a :Positive } => { :theorem3 :isProvenFor ?X }.
+
+# proof by cases
+{
+    (?X) log:allPossibleCases ?Y.
+    ?T a :Theorem.
+    (
+        { ?Y list:member { ?X a ?Z } }
+        { { ?X a ?Z } => { ?T :isProvenFor ?X } }
+    ) log:forAllIn ?SCOPE.
+} => {
+    ?T :isProvenFor ?X.
+}.
diff --git a/reasoning/proof-by-cases/test b/reasoning/proof-by-cases/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/proof-by-cases/example1.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1-query.n3 --output example1-answer.n3
+eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-cases/example1-query.n3 --output example1-proof.n3