fixing log:satisfiable

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v10.30.17 (2024-12-11) fixing log:satisfiable
 v10.30.16 (2024-12-09) fixing string:substring
 v10.30.15 (2024-12-09) adding log:satisfiable built-in
 v10.30.14 (2024-12-09) fixing log:conclusion

VERSION

@@ -1 +1 @@
-10.30.16
+10.30.17

eye.pl

@@ -22,7 +22,7 @@
 :- catch(use_module(library(process)), _, true).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v10.30.16 (2024-12-09)').
+version_info('EYE v10.30.17 (2024-12-11)').
 
 license_info('MIT License
 
@@ -7890,7 +7890,7 @@
             ->  Quiet = '--quiet'
             ;   Quiet = ''
             ),
-            append([A1, A2, ['--nope', Quiet, Tmp1, '--pass-all', '>', Tmp2]], A4),
+            append([A1, A2, ['--nope', Quiet, Tmp1, '--pass-all', '>', Tmp2, '2> /dev/null']], A4),
             findall([G, ' '],
                 (   member(G, A4)
                 ),

reasoning/proof-by-contradiction/README

@@ -0,0 +1,5 @@
+----------------------
+Proof by contradiction
+----------------------
+
+Using log:implies false and log:satisfiable to deal with negation.

reasoning/proof-by-contradiction/example1-answer.n3

@@ -0,0 +1,3 @@
+@prefix : <urn:example:>.
+
+:Socrates a :Mortal.

reasoning/proof-by-contradiction/example1-proof.n3

@@ -0,0 +1,82 @@
+@prefix : <urn:example:>.
+@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#>.
+
+skolem:proof a r:Proof, r:Conjunction;
+    r:component skolem:lemma1;
+    r:gives {
+        :Socrates a :Mortal.
+    }.
+
+skolem:lemma1 a r:Inference;
+    r:gives {
+        :Socrates a :Mortal.
+    };
+    r:evidence (
+        skolem:lemma2
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:Socrates"]];
+    r:rule skolem:lemma3.
+
+skolem:lemma2 a r:Inference;
+    r:gives {
+        :Socrates a :Mortal.
+    };
+    r:evidence (
+        skolem:lemma4
+        [ a r:Fact; r:gives {@forSome var:x_0. {
+            :Socrates a :Human.
+            {
+                :Socrates a :Human.
+            } => {
+                :Socrates a :Mortal.
+            }.
+            {
+                var:x_0 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;
+    r:gives {
+        @forAll var:x_0. {
+            var:x_0 a :Mortal.
+        } => {
+            var:x_0 a :Mortal.
+        }.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contradiction/example1-query.n3>].
+
+skolem:lemma4 a r:Extraction;
+    r:gives {
+        :Socrates a :Human.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contradiction/example1.n3>].
+
+skolem:lemma5 a r:Extraction;
+    r:gives {
+        @forAll var:x_0, var:x_1. {
+            var:x_0 a :Human.
+            {
+                var:x_0 a :Human.
+                {
+                    var:x_0 a :Human.
+                } => {
+                    var:x_0 a :Mortal.
+                }.
+                {
+                    var:x_1 a :Mortal.
+                } => false.
+            } log:satisfiable false.
+        } => {
+            var:x_0 a :Mortal.
+        }.
+    };
+    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contradiction/example1.n3>].
+

reasoning/proof-by-contradiction/example1-query.n3

@@ -0,0 +1,8 @@
+@prefix : <urn:example:>.
+
+# query
+{
+    ?X a :Mortal.
+} => {
+    ?X a :Mortal.
+}.

reasoning/proof-by-contradiction/example1.n3

@@ -0,0 +1,19 @@
+@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:>.
+
+# facts
+:Socrates a :Human.
+
+# proof by contradiction
+{
+    ?X a :Human.
+    {
+        ?X a :Human.
+        { ?X a :Human } => { ?X a :Mortal }.
+        { ?Y a :Mortal } => false.
+    } log:satisfiable false.
+} => {
+    ?X a :Mortal.
+}.

reasoning/proof-by-contradiction/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-contradiction/example1.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-contradiction/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-contradiction/example1.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-contradiction/example1-query.n3 --output example1-proof.n3