adding proof-by-contradiction/example2

eyereasoner · Dec 20, 2024 · 22f49ed · 22f49ed
1 parent 950ef5e
commit 22f49ed
Show file tree

Hide file tree

Showing 7 changed files with 406 additions and 7 deletions.
diff --git a/reasoning/proof-by-contradiction/example1-proof.n3 b/reasoning/proof-by-contradiction/example1-proof.n3
@@ -2,8 +2,8 @@
 @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 n3: <http://www.w3.org/2004/06/rei#>.
-@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 @prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix var: <http://www.w3.org/2000/10/swap/var#>.
 
 skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma1;
@@ -27,20 +27,19 @@ skolem:lemma2 a r:Inference;
     };
     r:evidence (
         skolem:lemma4
-        [ a r:Fact; r:gives {@forSome var:x_0. {
+        [ a r:Fact; r:gives {{
             :Socrates a :Human.
             {
                 :Socrates a :Human.
             } => {
                 :Socrates a :Mortal.
             }.
             {
-                var:x_0 a :Mortal.
+                :Socrates a :Mortal.
             } => false.
         } log:satisfiable false}]
     );
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:Socrates"]];
-    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_0"]];
     r:rule skolem:lemma5.
 
 skolem:lemma3 a r:Extraction;
@@ -61,7 +60,7 @@ skolem:lemma4 a r:Extraction;
 
 skolem:lemma5 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1. {
+        @forAll var:x_0. {
             var:x_0 a :Human.
             {
                 var:x_0 a :Human.
@@ -71,7 +70,7 @@ skolem:lemma5 a r:Extraction;
                     var:x_0 a :Mortal.
                 }.
                 {
-                    var:x_1 a :Mortal.
+                    var:x_0 a :Mortal.
                 } => false.
             } log:satisfiable false.
         } => {

diff --git a/reasoning/proof-by-contradiction/example1.n3 b/reasoning/proof-by-contradiction/example1.n3
@@ -10,7 +10,7 @@
     {
         ?X a :Human.
         { ?X a :Human } => { ?X a :Mortal }.
-        { ?Y a :Mortal } => false.
+        { ?X a :Mortal } => false.
     } log:satisfiable false.
 } => {
     ?X a :Mortal.

diff --git a/reasoning/proof-by-contradiction/example2-answer.n3 b/reasoning/proof-by-contradiction/example2-answer.n3
@@ -0,0 +1,13 @@
+@prefix math: <http://www.w3.org/2000/10/swap/math#>.
+@prefix : <urn:example:>.
+
+0 a :Positive.
+1 a :Positive.
+2 a :Positive.
+3 a :Positive.
+4 a :Positive.
+5 a :Positive.
+6 a :Positive.
+7 a :Positive.
+8 a :Positive.
+9 a :Positive.