refreshing

eyereasoner · Dec 12, 2024 · ddfd17d · ddfd17d
1 parent dbbdb9f
commit ddfd17d
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 11 deletions.
diff --git a/reasoning/proof-by-contrapositive/example2-proof.n3 b/reasoning/proof-by-contrapositive/example2-proof.n3
@@ -26,15 +26,8 @@ skolem:lemma2 a r:Inference;
         :ground :is :wet.
     };
     r:evidence (
-        [ a r:Fact; r:gives {{
-            {
-                :ground :is :wet.
-            } => false.
-        } => false}]
+        [ a r:Fact; r:gives true]
     );
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
-        :ground :is :wet.
-    }];
     r:rule skolem:lemma4.
 
 skolem:lemma3 a r:Extraction;
@@ -47,13 +40,33 @@ skolem:lemma3 a r:Extraction;
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2-query.n3>].
 
-skolem:lemma4 a r:Extraction;
+skolem:lemma4 a r:Inference;
+    r:gives {
+        true => {
+            :ground :is :wet.
+        }.
+    };
+    r:evidence (
+        [ a r:Fact; r:gives {{
+            {
+                :ground :is :wet.
+            } => false.
+        } => false}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
+        :ground :is :wet.
+    }];
+    r:rule skolem:lemma5.
+
+skolem:lemma5 a r:Extraction;
     r:gives {
         @forAll var:x_0. {
             {
                 var:x_0 => false.
             } => false.
-        } => var:x_0.
+        } => {
+            true => var:x_0.
+        }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2.n3>].
 
diff --git a/reasoning/proof-by-contrapositive/example2.n3 b/reasoning/proof-by-contrapositive/example2.n3
@@ -5,4 +5,4 @@
 { { :ground :is :wet } => false } => false.
 
 # proof by contrapositive
-{ { ?P => false } => false } => ?P.
+{ { ?P => false } => false } => { true => ?P }.