From c16ba697f2086032c29e0e11119814a65d6637ff Mon Sep 17 00:00:00 2001 From: josd Date: Wed, 18 Dec 2024 23:37:28 +0100 Subject: [PATCH] refreshing --- reasoning/nand/README | 13 - reasoning/nand/ab-answer.n3 | 3 - reasoning/nand/ab-proof.n3 | 923 ------------------ reasoning/nand/ab.n3 | 17 - reasoning/nand/nand.n3 | 50 - reasoning/nand/query.n3 | 7 - reasoning/nand/test | 23 - reasoning/nand/test1-answer.n3 | 3 - reasoning/nand/test1-proof.n3 | 379 -------- reasoning/nand/test1.n3 | 15 - reasoning/nand/test2-answer.n3 | 3 - reasoning/nand/test2-proof.n3 | 384 -------- reasoning/nand/test2.n3 | 21 - reasoning/nand/test3-answer.n3 | 3 - reasoning/nand/test3-proof.n3 | 843 ----------------- reasoning/nand/test3.n3 | 24 - reasoning/nand/test4-answer.n3 | 3 - reasoning/nand/test4-proof.n3 | 1596 -------------------------------- reasoning/nand/test4.n3 | 31 - reasoning/nand/test5-answer.n3 | 3 - reasoning/nand/test5-proof.n3 | 650 ------------- reasoning/nand/test5.n3 | 24 - reasoning/nand/test6-answer.n3 | 3 - reasoning/nand/test6-proof.n3 | 418 --------- reasoning/nand/test6.n3 | 24 - reasoning/nand/v1-answer.n3 | 0 reasoning/nand/v1-fuse.err | 17 - reasoning/nand/v1.n3 | 25 - 28 files changed, 5505 deletions(-) delete mode 100644 reasoning/nand/README delete mode 100644 reasoning/nand/ab-answer.n3 delete mode 100644 reasoning/nand/ab-proof.n3 delete mode 100644 reasoning/nand/ab.n3 delete mode 100644 reasoning/nand/nand.n3 delete mode 100644 reasoning/nand/query.n3 delete mode 100755 reasoning/nand/test delete mode 100644 reasoning/nand/test1-answer.n3 delete mode 100644 reasoning/nand/test1-proof.n3 delete mode 100644 reasoning/nand/test1.n3 delete mode 100644 reasoning/nand/test2-answer.n3 delete mode 100644 reasoning/nand/test2-proof.n3 delete mode 100644 reasoning/nand/test2.n3 delete mode 100644 reasoning/nand/test3-answer.n3 delete mode 100644 reasoning/nand/test3-proof.n3 delete mode 100644 reasoning/nand/test3.n3 delete mode 100644 reasoning/nand/test4-answer.n3 delete mode 100644 reasoning/nand/test4-proof.n3 delete mode 100644 reasoning/nand/test4.n3 delete mode 100644 reasoning/nand/test5-answer.n3 delete mode 100644 reasoning/nand/test5-proof.n3 delete mode 100644 reasoning/nand/test5.n3 delete mode 100644 reasoning/nand/test6-answer.n3 delete mode 100644 reasoning/nand/test6-proof.n3 delete mode 100644 reasoning/nand/test6.n3 delete mode 100644 reasoning/nand/v1-answer.n3 delete mode 100644 reasoning/nand/v1-fuse.err delete mode 100644 reasoning/nand/v1.n3 diff --git a/reasoning/nand/README b/reasoning/nand/README deleted file mode 100644 index 8082d7e87..000000000 --- a/reasoning/nand/README +++ /dev/null @@ -1,13 +0,0 @@ ----- -NAND ----- - -Expressing nand as { triples } => false. - -We define NAND logic in nand.n3 similarly to how we define other logic -systems, such as RDFS, OWL, Fuzzy Logic, etc. This approach serves two -main purposes: first, to enable the generation of valid proofs, and -second, to facilitate the selection of rules and queries for subsequent -reasoning processes. - -The tests are from Patric Hochstenbach. diff --git a/reasoning/nand/ab-answer.n3 b/reasoning/nand/ab-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/ab-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/ab-proof.n3 b/reasoning/nand/ab-proof.n3 deleted file mode 100644 index 7166606d6..000000000 --- a/reasoning/nand/ab-proof.n3 +++ /dev/null @@ -1,923 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix n3: . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:test"]]; - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {{ - { - { - :B :is true. - } => false. - } => false. - { - :test :is true. - } => false. - } => false}] - [ a r:Fact; r:gives {{ - { - { - :B :is true. - } => false. - } => false. - { - :test :is true. - } => false. - } graph:list ({ - { - { - :B :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - { - :B :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - }) list:notMember { - log:equalTo . - }}] - [ a r:Fact; r:gives {({ - { - { - :B :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - }) list:select ({ - { - { - :B :is true. - } => false. - } => false. - } ({ - { - :test :is true. - } => false. - }))}] - skolem:lemma6 - [ a r:Fact; r:gives {({ - ({ - { - :test :is true. - } => false. - }) list:member { - { - :test :is true. - } => false. - }. - } { - ({ - { - :test :is true. - } => false. - }) log:equalTo ({ - { - :test :is true. - } => false. - }). - } { - ({ - { - :test :is true. - } => false. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - { - :test :is true. - } => false. - })). - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - { - :B :is true. - } => false. - } => false. - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - { - :B :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo { - { - :B :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ({ - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ({ - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:rule skolem:lemma7. - -skolem:lemma5 a r:Inference; - r:gives { - @forAll var:x_3. { - { - { - var:x_3 :is true. - } => false. - } => false. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {@forSome var:x_3. { - { - { - var:x_3 :is true. - } => false. - } => false. - { - :test :is true. - } => false. - } => false}] - [ a r:Fact; r:gives {@forSome var:x_3. { - { - { - var:x_3 :is true. - } => false. - } => false. - { - :test :is true. - } => false. - } graph:list ({ - { - { - var:x_3 :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })}] - [ a r:Fact; r:gives {@forSome var:x_3. ({ - { - { - var:x_3 :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - { - { - var:x_3 :is true. - } => false. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {@forSome var:x_3. { - { - { - var:x_3 :is true. - } => false. - } => false. - } graph:list ({ - { - { - var:x_3 :is true. - } => false. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - { - var:x_3 :is true. - } => false. - } => false. - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - { - var:x_3 :is true. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - { - var:x_3 :is true. - } => false. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - { - var:x_3 :is true. - } => false. - } => false. - }]; - r:rule skolem:lemma8. - -skolem:lemma6 a r:Inference; - r:gives { - { - { - :B :is true. - } => false. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - { - :B :is true. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - { - :B :is true. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :B :is true. - } => false. - } graph:list ({ - { - :B :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - { - :B :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :B :is true. - } => false. - }]; - r:rule skolem:lemma8. - -skolem:lemma7 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7, var:x_8. { - log:equalTo . - var:x_0 => var:x_1. - var:x_0 graph:list var:x_2. - var:x_2 list:notMember { - log:equalTo . - }. - var:x_2 list:select ({ - var:x_3 => false. - } var:x_4). - var:x_3 => var:x_5. - ({ - var:x_4 list:member { - var:x_5 => false. - }. - } { - var:x_6 log:equalTo var:x_4. - } { - var:x_6 list:firstRest ({ - var:x_5 => false. - } var:x_4). - }) log:ifThenElseIn var:x_7. - var:x_8 graph:list var:x_6. - } => { - var:x_8 => var:x_1. - }. - }; - r:because [ a r:Parsing; r:source ]. - -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_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma9 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - { - :B :is true. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma10 - [ a r:Fact; r:gives {{ - { - :A :is true. - } => false. - { - :B :is true. - } => false. - } graph:list ({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - }) list:notMember { - log:equalTo . - }}] - [ a r:Fact; r:gives {({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - }) list:select ({ - { - :A :is true. - } => false. - } ({ - { - :B :is true. - } => false. - }))}] - [ a r:Fact; r:gives {{ - :A :is true. - } => { - :test :is true. - }}] - [ a r:Fact; r:gives {({ - ({ - { - :B :is true. - } => false. - }) list:member { - { - :test :is true. - } => false. - }. - } { - ({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - }) log:equalTo ({ - { - :B :is true. - } => false. - }). - } { - ({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - { - :B :is true. - } => false. - })). - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - { - :B :is true. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :A :is true. - } => false. - { - :B :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo { - :A :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ({ - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo { - { - :test :is true. - } => false. - { - :B :is true. - } => false. - }]; - r:rule skolem:lemma7. - -skolem:lemma10 a r:Inference; - r:gives { - { - { - :A :is true. - } => false. - { - :B :is true. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma11 - [ a r:Fact; r:gives {{ - :A :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :B :is true. - } => false. - } graph:list ({ - { - :B :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - }) list:firstRest ({ - { - :A :is true. - } => false. - } ({ - { - :B :is true. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - :A :is true. - } => false. - { - :B :is true. - } => false. - } graph:list ({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :B :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :A :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :A :is true. - } => false. - { - :B :is true. - } => false. - }]; - r:rule skolem:lemma12. - -skolem:lemma11 a r:Inference; - r:gives { - { - { - :B :is true. - } => false. - } => { - :A :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma10 - [ a r:Fact; r:gives {{ - { - :A :is true. - } => false. - { - :B :is true. - } => false. - } graph:list ({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - }) list:select ({ - { - :A :is true. - } => false. - } ({ - { - :B :is true. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :A :is true. - } => false. - } log:equalTo { - { - :A :is true. - } => false. - }. - } true { - { - :A :is true. - } log:equalTo { - { - { - :A :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :B :is true. - } => false. - } graph:list ({ - { - :B :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :A :is true. - } => false. - { - :B :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :A :is true. - } => false. - } { - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :A :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :B :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :A :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :B :is true. - } => false. - }]; - r:rule skolem:lemma8. - -skolem:lemma12 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - diff --git a/reasoning/nand/ab.n3 b/reasoning/nand/ab.n3 deleted file mode 100644 index f049e5ad3..000000000 --- a/reasoning/nand/ab.n3 +++ /dev/null @@ -1,17 +0,0 @@ -@prefix : . -@prefix log: . - -{ - { - :A :is true . - } => false . - { - :B :is true . - } => false . -} => false . - -{ - ?X :is true . -} => { - :test :is true . -} . diff --git a/reasoning/nand/nand.n3 b/reasoning/nand/nand.n3 deleted file mode 100644 index af31ec4b6..000000000 --- a/reasoning/nand/nand.n3 +++ /dev/null @@ -1,50 +0,0 @@ -# ------------------------ -# NAND rules -- Jos De Roo -# ------------------------ - -@prefix list: . -@prefix graph: . -@prefix log: . - -# contrapositive rule -{ - <#nand> log:equalTo <#nand>. - ?P => false. - ?P graph:list ?L. - ?L list:select (?A ?B). - ( { ?A log:equalTo { ?C => false } } - true - { ?C log:equalTo { ?A => false } } - ) log:ifThenElseIn ?SCOPE. - ?E graph:list ?B. -} => { - ?E => ?C. -}. - -{ - <#nand> log:equalTo <#nand>. - ?P => ?C. - ?C log:notEqualTo false. - ?P graph:list ?L. - ?M list:firstRest ({ ?C => false } ?L). - ?E graph:list ?M. -} => { - ?E => false. -}. - -# resolution rule -{ - <#nand> log:equalTo <#nand>. - ?P => ?C. - ?P graph:list ?L. - ?L list:notMember { <#nand> log:equalTo <#nand> }. - ?L list:select ({ ?A => false } ?B). - ?A => ?D. - ( { ?B list:member { ?D => false } } - { ?M log:equalTo ?B } - { ?M list:firstRest ({ ?D => false } ?B) } - ) log:ifThenElseIn ?SCOPE. - ?E graph:list ?M. -} => { - ?E => ?C. -}. diff --git a/reasoning/nand/query.n3 b/reasoning/nand/query.n3 deleted file mode 100644 index d17566670..000000000 --- a/reasoning/nand/query.n3 +++ /dev/null @@ -1,7 +0,0 @@ -@prefix : . - -{ - :test :is true. -} => { - :test :is true. -}. diff --git a/reasoning/nand/test b/reasoning/nand/test deleted file mode 100755 index 051f17ad1..000000000 --- a/reasoning/nand/test +++ /dev/null @@ -1,23 +0,0 @@ -#!/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/nand/test1.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test1-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/test1.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test1-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/test2.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test2-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/test2.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test2-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/test3.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test3-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/test3.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test3-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/test4.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test4-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/test4.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test4-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/test5.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test5-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/test5.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test5-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/test6.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test6-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/test6.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output test6-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/ab.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output ab-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/nand/ab.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --query https://eyereasoner.github.io/eye/reasoning/nand/query.n3 --output ab-proof.n3 - -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/nand/v1.n3 https://eyereasoner.github.io/eye/reasoning/nand/nand.n3 --pass --output v1-answer.n3 2> v1-fuse.err diff --git a/reasoning/nand/test1-answer.n3 b/reasoning/nand/test1-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/test1-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/test1-proof.n3 b/reasoning/nand/test1-proof.n3 deleted file mode 100644 index 29cdb9f0a..000000000 --- a/reasoning/nand/test1-proof.n3 +++ /dev/null @@ -1,379 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix n3: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - :P a :Test. - }; - r:evidence ( - [ a r:Fact; r:gives true] - ); - r:rule skolem:lemma6. - -skolem:lemma5 a r:Inference; - r:gives { - { - :P a :Test. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma7 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :P a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :P a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :P a :Test. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - :P a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :P a :Test. - } graph:list ({ - :P a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :P a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :P a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :P a :Test. - }]; - r:rule skolem:lemma8. - -skolem:lemma6 a r:Inference; - r:gives { - true => { - :P a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - }) list:select ({ - { - :P a :Test. - } => false. - } ())}] - [ a r:Fact; r:gives {({ - { - { - :P a :Test. - } => false. - } log:equalTo { - { - :P a :Test. - } => false. - }. - } true { - { - :P a :Test. - } log:equalTo { - { - { - :P a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {true graph:list ()}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true]; - r:rule skolem:lemma8. - -skolem:lemma7 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - :P a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma5 - [ a r:Fact; r:gives {{ - :test :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - :P a :Test. - } graph:list ({ - :P a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :P a :Test. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - :P a :Test. - }))}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :P a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :P a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - :P a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :P a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :test :is true. - } => false. - :P a :Test. - }]; - r:rule skolem:lemma10. - -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_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma9 a r:Inference; - r:gives { - { - { - :P a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma6 - [ a r:Fact; r:gives {{ - :P a :Test. - } log:notEqualTo false}] - [ a r:Fact; r:gives {true graph:list ()}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - }) list:firstRest ({ - { - :P a :Test. - } => false. - } ())}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo true]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ()]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma10 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - diff --git a/reasoning/nand/test1.n3 b/reasoning/nand/test1.n3 deleted file mode 100644 index 86536d5af..000000000 --- a/reasoning/nand/test1.n3 +++ /dev/null @@ -1,15 +0,0 @@ -@prefix : . - -# ~~P -{ - { :P a :Test } => false . -} => false . - -# |= P -{ - :P a :Test . -} -=> -{ - :test :is true . -} . diff --git a/reasoning/nand/test2-answer.n3 b/reasoning/nand/test2-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/test2-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/test2-proof.n3 b/reasoning/nand/test2-proof.n3 deleted file mode 100644 index 40b8dadb6..000000000 --- a/reasoning/nand/test2-proof.n3 +++ /dev/null @@ -1,384 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix n3: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - :R a :Test. - }; - r:evidence ( - skolem:lemma6 - skolem:lemma7 - ); - r:rule skolem:lemma8. - -skolem:lemma5 a r:Inference; - r:gives { - { - :R a :Test. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :R a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :R a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :R a :Test. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - :R a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :R a :Test. - } graph:list ({ - :R a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :R a :Test. - }]; - r:rule skolem:lemma10. - -skolem:lemma6 a r:Extraction; - r:gives { - :P a :Test. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma7 a r:Extraction; - r:gives { - :Q a :Test. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma8 a r:Inference; - r:gives { - { - :P a :Test. - :Q a :Test. - } => { - :R a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - { - :R a :Test. - } => false. - } => false}] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - { - :R a :Test. - } => false. - } graph:list ({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - }) list:select ({ - { - :R a :Test. - } => false. - } ({ - :P a :Test. - } { - :Q a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - { - :R a :Test. - } => false. - } log:equalTo { - { - :R a :Test. - } => false. - }. - } true { - { - :R a :Test. - } log:equalTo { - { - { - :R a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - } graph:list ({ - :P a :Test. - } { - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :P a :Test. - :Q a :Test. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :P a :Test. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :P a :Test. - :Q a :Test. - }]; - r:rule skolem:lemma10. - -skolem:lemma9 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - :R a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma5 - [ a r:Fact; r:gives {{ - :test :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - :R a :Test. - } graph:list ({ - :R a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :R a :Test. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - :R a :Test. - }))}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :R a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :R a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :test :is true. - } => false. - :R a :Test. - }]; - r:rule skolem:lemma11. - -skolem:lemma10 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma11 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - diff --git a/reasoning/nand/test2.n3 b/reasoning/nand/test2.n3 deleted file mode 100644 index 6e56dd83e..000000000 --- a/reasoning/nand/test2.n3 +++ /dev/null @@ -1,21 +0,0 @@ -@prefix : . -@prefix log: . - -:P a :Test . -:Q a :Test . - -# P & Q -> R -{ - :P a :Test . - :Q a :Test . - { :R a :Test } => false . -} => false . - -# |= R -{ - :R a :Test . -} -=> -{ - :test :is true . -} . \ No newline at end of file diff --git a/reasoning/nand/test3-answer.n3 b/reasoning/nand/test3-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/test3-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/test3-proof.n3 b/reasoning/nand/test3-proof.n3 deleted file mode 100644 index 5348b6eb8..000000000 --- a/reasoning/nand/test3-proof.n3 +++ /dev/null @@ -1,843 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix n3: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - :Q a :Test. - }; - r:evidence ( - skolem:lemma6 - skolem:lemma7 - ); - r:rule skolem:lemma8. - -skolem:lemma5 a r:Inference; - r:gives { - { - :Q a :Test. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :Q a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :Q a :Test. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - :Q a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :Q a :Test. - } graph:list ({ - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :Q a :Test. - }]; - r:rule skolem:lemma10. - -skolem:lemma6 a r:Inference; - r:gives { - { - :P a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives true] - ); - r:rule skolem:lemma11. - -skolem:lemma7 a r:Inference; - r:gives { - { - :R a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives true] - ); - r:rule skolem:lemma12. - -skolem:lemma8 a r:Inference; - r:gives { - { - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - } => { - :Q a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma13 - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:select ({ - { - :Q a :Test. - } => false. - } ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :Q a :Test. - } => false. - } log:equalTo { - { - :Q a :Test. - } => false. - }. - } true { - { - :Q a :Test. - } log:equalTo { - { - { - :Q a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma9 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - :Q a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma5 - [ a r:Fact; r:gives {{ - :test :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - :Q a :Test. - } graph:list ({ - :Q a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :Q a :Test. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - :Q a :Test. - }))}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :Q a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :test :is true. - } => false. - :Q a :Test. - }]; - r:rule skolem:lemma14. - -skolem:lemma10 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma11 a r:Inference; - r:gives { - true => { - { - :P a :Test. - } => false. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma6 - [ a r:Fact; r:gives {{ - :P a :Test. - } graph:list ({ - :P a :Test. - })}] - [ a r:Fact; r:gives {({ - :P a :Test. - }) list:select ({ - :P a :Test. - } ())}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } log:equalTo { - { - { - :P a :Test. - } => false. - } => false. - }. - } true { - { - { - :P a :Test. - } => false. - } log:equalTo { - { - :P a :Test. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {true graph:list ()}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :P a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true]; - r:rule skolem:lemma10. - -skolem:lemma12 a r:Inference; - r:gives { - true => { - { - :R a :Test. - } => false. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma7 - [ a r:Fact; r:gives {{ - :R a :Test. - } graph:list ({ - :R a :Test. - })}] - [ a r:Fact; r:gives {({ - :R a :Test. - }) list:select ({ - :R a :Test. - } ())}] - [ a r:Fact; r:gives {({ - { - :R a :Test. - } log:equalTo { - { - { - :R a :Test. - } => false. - } => false. - }. - } true { - { - { - :R a :Test. - } => false. - } log:equalTo { - { - :R a :Test. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {true graph:list ()}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true]; - r:rule skolem:lemma10. - -skolem:lemma13 a r:Inference; - r:gives { - { - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma15 - [ a r:Fact; r:gives {{ - :P a :Test. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:firstRest ({ - { - :P a :Test. - } => false. - } ({ - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:rule skolem:lemma14. - -skolem:lemma14 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma15 a r:Inference; - r:gives { - { - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } => { - :P a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma13 - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:select ({ - { - :P a :Test. - } => false. - } ({ - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :P a :Test. - } => false. - } log:equalTo { - { - :P a :Test. - } => false. - }. - } true { - { - :P a :Test. - } log:equalTo { - { - { - :P a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - } => false. - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :Q a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :Q a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:rule skolem:lemma10. - diff --git a/reasoning/nand/test3.n3 b/reasoning/nand/test3.n3 deleted file mode 100644 index 5434687f7..000000000 --- a/reasoning/nand/test3.n3 +++ /dev/null @@ -1,24 +0,0 @@ -@prefix : . -@prefix log: . - -# P v Q v R -{ - { :P a :Test } => false . - { :Q a :Test } => false . - { :R a :Test } => false . -} => false . - -# ~P -{ :P a :Test } => false . - -# ~R -{ :R a :Test } => false . - -# |= Q -{ - :Q a :Test . -} -=> -{ - :test :is true . -} . \ No newline at end of file diff --git a/reasoning/nand/test4-answer.n3 b/reasoning/nand/test4-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/test4-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/test4-proof.n3 b/reasoning/nand/test4-proof.n3 deleted file mode 100644 index f8dce8078..000000000 --- a/reasoning/nand/test4-proof.n3 +++ /dev/null @@ -1,1596 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix n3: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - { - { - :Q a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma6 - [ a r:Fact; r:gives {{ - { - { - :P a :Test. - } => false. - } => false. - { - :Q a :Test. - } => false. - } graph:list ({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - }) list:notMember { - log:equalTo . - }}] - [ a r:Fact; r:gives {({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - }) list:select ({ - { - { - :P a :Test. - } => false. - } => false. - } ({ - { - :Q a :Test. - } => false. - }))}] - skolem:lemma7 - [ a r:Fact; r:gives {({ - ({ - { - :Q a :Test. - } => false. - }) list:member { - { - :Q a :Test. - } => false. - }. - } { - ({ - { - :Q a :Test. - } => false. - }) log:equalTo ({ - { - :Q a :Test. - } => false. - }). - } { - ({ - { - :Q a :Test. - } => false. - }) list:firstRest ({ - { - :Q a :Test. - } => false. - } ({ - { - :Q a :Test. - } => false. - })). - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - { - :P a :Test. - } => false. - } => false. - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ({ - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ({ - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:rule skolem:lemma8. - -skolem:lemma5 a r:Inference; - r:gives { - { - { - { - :Q a :Test. - } => false. - } => false. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - { - { - :Q a :Test. - } => false. - } => false. - { - :test :is true. - } => false. - } graph:list ({ - { - { - :Q a :Test. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - { - :Q a :Test. - } => false. - } => false. - } { - { - :test :is true. - } => false. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - { - { - :Q a :Test. - } => false. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - { - :Q a :Test. - } => false. - } => false. - } graph:list ({ - { - { - :Q a :Test. - } => false. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - { - :Q a :Test. - } => false. - } => false. - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - { - :Q a :Test. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - { - :Q a :Test. - } => false. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - { - :Q a :Test. - } => false. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma6 a r:Inference; - r:gives { - { - { - { - :P a :Test. - } => false. - } => false. - { - :Q a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma11 - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - }) list:firstRest ({ - { - { - :P a :Test. - } => false. - } => false. - } ({ - { - :Q a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - { - :P a :Test. - } => false. - } => false. - { - :Q a :Test. - } => false. - } graph:list ({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - { - :P a :Test. - } => false. - } => false. - } { - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - { - :P a :Test. - } => false. - } => false. - { - :Q a :Test. - } => false. - }]; - r:rule skolem:lemma12. - -skolem:lemma7 a r:Inference; - r:gives { - { - { - :P a :Test. - } => false. - } => { - :Q a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma13 - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - { - :P a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - }) list:select ({ - { - :Q a :Test. - } => false. - } ({ - { - :P a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :Q a :Test. - } => false. - } log:equalTo { - { - :Q a :Test. - } => false. - }. - } true { - { - :Q a :Test. - } log:equalTo { - { - { - :Q a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :Q a :Test. - } => false. - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:rule skolem:lemma10. - -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_5, var:x_6, var:x_7, var:x_8. { - log:equalTo . - var:x_0 => var:x_1. - var:x_0 graph:list var:x_2. - var:x_2 list:notMember { - log:equalTo . - }. - var:x_2 list:select ({ - var:x_3 => false. - } var:x_4). - var:x_3 => var:x_5. - ({ - var:x_4 list:member { - var:x_5 => false. - }. - } { - var:x_6 log:equalTo var:x_4. - } { - var:x_6 list:firstRest ({ - var:x_5 => false. - } var:x_4). - }) log:ifThenElseIn var:x_7. - var:x_8 graph:list var:x_6. - } => { - var:x_8 => var:x_1. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma9 a r:Inference; - r:gives { - { - { - { - :Q a :Test. - } => false. - } => false. - { - :test :is true. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma14 - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - { - :Q a :Test. - } => false. - } => false. - } { - { - :test :is true. - } => false. - }) list:firstRest ({ - { - { - :Q a :Test. - } => false. - } => false. - } ({ - { - :test :is true. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - { - :Q a :Test. - } => false. - } => false. - { - :test :is true. - } => false. - } graph:list ({ - { - { - :Q a :Test. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - { - :Q a :Test. - } => false. - } => false. - } { - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - { - :Q a :Test. - } => false. - } => false. - { - :test :is true. - } => false. - }]; - r:rule skolem:lemma12. - -skolem:lemma10 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma11 a r:Inference; - r:gives { - { - { - :Q a :Test. - } => false. - } => { - { - :P a :Test. - } => false. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {{ - :P a :Test. - { - :Q a :Test. - } => false. - } => false}] - [ a r:Fact; r:gives {{ - :P a :Test. - { - :Q a :Test. - } => false. - } graph:list ({ - :P a :Test. - } { - { - :Q a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - :P a :Test. - } { - { - :Q a :Test. - } => false. - }) list:select ({ - :P a :Test. - } ({ - { - :Q a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } log:equalTo { - { - { - :P a :Test. - } => false. - } => false. - }. - } true { - { - { - :P a :Test. - } => false. - } log:equalTo { - { - :P a :Test. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :P a :Test. - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :P a :Test. - } { - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma12 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma13 a r:Inference; - r:gives { - { - { - :Q a :Test. - } => false. - { - :P a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma15 - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:notMember { - log:equalTo . - }}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:select ({ - { - :R a :Test. - } => false. - } ({ - { - :P a :Test. - } => false. - }))}] - skolem:lemma16 - [ a r:Fact; r:gives {({ - ({ - { - :P a :Test. - } => false. - }) list:member { - { - :Q a :Test. - } => false. - }. - } { - ({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - }) log:equalTo ({ - { - :P a :Test. - } => false. - }). - } { - ({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - }) list:firstRest ({ - { - :Q a :Test. - } => false. - } ({ - { - :P a :Test. - } => false. - })). - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :Q a :Test. - } => false. - { - :P a :Test. - } => false. - } graph:list ({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ({ - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ({ - { - :Q a :Test. - } => false. - } { - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo { - { - :Q a :Test. - } => false. - { - :P a :Test. - } => false. - }]; - r:rule skolem:lemma8. - -skolem:lemma14 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - } => { - { - :Q a :Test. - } => false. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma17 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :Q a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :Q a :Test. - }) list:select ({ - :Q a :Test. - } ({ - { - :test :is true. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - :Q a :Test. - } log:equalTo { - { - { - :Q a :Test. - } => false. - } => false. - }. - } true { - { - { - :Q a :Test. - } => false. - } log:equalTo { - { - :Q a :Test. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma15 a r:Inference; - r:gives { - { - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma18 - [ a r:Fact; r:gives {{ - :P a :Test. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :R a :Test. - } => false. - } graph:list ({ - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:firstRest ({ - { - :P a :Test. - } => false. - } ({ - { - :R a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:rule skolem:lemma12. - -skolem:lemma16 a r:Inference; - r:gives { - { - :R a :Test. - } => { - :Q a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {{ - :R a :Test. - { - :Q a :Test. - } => false. - } => false}] - [ a r:Fact; r:gives {{ - :R a :Test. - { - :Q a :Test. - } => false. - } graph:list ({ - :R a :Test. - } { - { - :Q a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - :R a :Test. - } { - { - :Q a :Test. - } => false. - }) list:select ({ - { - :Q a :Test. - } => false. - } ({ - :R a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - { - :Q a :Test. - } => false. - } log:equalTo { - { - :Q a :Test. - } => false. - }. - } true { - { - :Q a :Test. - } log:equalTo { - { - { - :Q a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :R a :Test. - } graph:list ({ - :R a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :R a :Test. - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :R a :Test. - } { - { - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :R a :Test. - }]; - r:rule skolem:lemma10. - -skolem:lemma17 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - :Q a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma19 - [ a r:Fact; r:gives {{ - :test :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - :Q a :Test. - } graph:list ({ - :Q a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :Q a :Test. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - :Q a :Test. - }))}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :Q a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :test :is true. - } => false. - :Q a :Test. - }]; - r:rule skolem:lemma12. - -skolem:lemma18 a r:Inference; - r:gives { - { - { - :R a :Test. - } => false. - } => { - :P a :Test. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma15 - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - }) list:select ({ - { - :P a :Test. - } => false. - } ({ - { - :R a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :P a :Test. - } => false. - } log:equalTo { - { - :P a :Test. - } => false. - }. - } true { - { - :P a :Test. - } log:equalTo { - { - { - :P a :Test. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :R a :Test. - } => false. - } graph:list ({ - { - :R a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - } => false. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :P a :Test. - } => false. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :R a :Test. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma19 a r:Inference; - r:gives { - { - :Q a :Test. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma17 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - :Q a :Test. - } graph:list ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - :Q a :Test. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - :Q a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :Q a :Test. - } graph:list ({ - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :Q a :Test. - }]; - r:rule skolem:lemma10. - diff --git a/reasoning/nand/test4.n3 b/reasoning/nand/test4.n3 deleted file mode 100644 index 8c30260ef..000000000 --- a/reasoning/nand/test4.n3 +++ /dev/null @@ -1,31 +0,0 @@ -@prefix : . -@prefix log: . - -# (P -> Q) . (R -> Q ) . (P v R ) |- Q - -# P -> Q -{ - :P a :Test . - { :Q a :Test } => false . -} => false . - -# R -> Q -{ - :R a :Test . - { :Q a :Test } => false . -} => false . - -# P v R -{ - { :P a :Test } => false . - { :R a :Test } => false . -} => false . - -# |= Q -{ - :Q a :Test . -} -=> -{ - :test :is true . -} . \ No newline at end of file diff --git a/reasoning/nand/test5-answer.n3 b/reasoning/nand/test5-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/test5-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/test5-proof.n3 b/reasoning/nand/test5-proof.n3 deleted file mode 100644 index 2d1904146..000000000 --- a/reasoning/nand/test5-proof.n3 +++ /dev/null @@ -1,650 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix n3: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - { - :P a :Test. - :Q a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma6 - [ a r:Fact; r:gives {{ - false => false. - :P a :Test. - :Q a :Test. - } graph:list ({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - })}] - [ a r:Fact; r:gives {({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - }) list:select ({ - false => false. - } ({ - :P a :Test. - } { - :Q a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - false => false. - } log:equalTo { - false => false. - }. - } true { - false log:equalTo { - { - false => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - } graph:list ({ - :P a :Test. - } { - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - false => false. - :P a :Test. - :Q a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - false => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :P a :Test. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :P a :Test. - :Q a :Test. - }]; - r:rule skolem:lemma7. - -skolem:lemma5 a r:Inference; - r:gives { - { - { - :P a :Test. - :Q a :Test. - } => false. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma8 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - { - :P a :Test. - :Q a :Test. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - :Q a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - :Q a :Test. - } => false. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - { - :P a :Test. - :Q a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - :Q a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - :Q a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - { - :P a :Test. - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :P a :Test. - :Q a :Test. - } => false. - }]; - r:rule skolem:lemma7. - -skolem:lemma6 a r:Inference; - r:gives { - { - false => false. - :P a :Test. - :Q a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - { - :R a :Test. - } => false. - } => false}] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - { - :R a :Test. - } => false. - } graph:list ({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - }) list:notMember { - log:equalTo . - }}] - [ a r:Fact; r:gives {({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - }) list:select ({ - { - :R a :Test. - } => false. - } ({ - :P a :Test. - } { - :Q a :Test. - }))}] - skolem:lemma9 - [ a r:Fact; r:gives {({ - ({ - :P a :Test. - } { - :Q a :Test. - }) list:member { - false => false. - }. - } { - ({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - }) log:equalTo ({ - :P a :Test. - } { - :Q a :Test. - }). - } { - ({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - }) list:firstRest ({ - false => false. - } ({ - :P a :Test. - } { - :Q a :Test. - })). - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - false => false. - :P a :Test. - :Q a :Test. - } graph:list ({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :P a :Test. - :Q a :Test. - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - :P a :Test. - } { - :Q a :Test. - } { - { - :R a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ({ - :P a :Test. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo false]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ({ - false => false. - } { - :P a :Test. - } { - :Q a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo { - false => false. - :P a :Test. - :Q a :Test. - }]; - r:rule skolem:lemma10. - -skolem:lemma7 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma8 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - { - :P a :Test. - :Q a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma5 - [ a r:Fact; r:gives {{ - :test :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - :Q a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - :Q a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - :Q a :Test. - } => false. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - { - :P a :Test. - :Q a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - { - :P a :Test. - :Q a :Test. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - :Q a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - :Q a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :P a :Test. - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - :Q a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :test :is true. - } => false. - { - :P a :Test. - :Q a :Test. - } => false. - }]; - r:rule skolem:lemma11. - -skolem:lemma9 a r:Inference; - r:gives { - { - :R a :Test. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives true] - ); - r:rule skolem:lemma12. - -skolem:lemma10 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7, var:x_8. { - log:equalTo . - var:x_0 => var:x_1. - var:x_0 graph:list var:x_2. - var:x_2 list:notMember { - log:equalTo . - }. - var:x_2 list:select ({ - var:x_3 => false. - } var:x_4). - var:x_3 => var:x_5. - ({ - var:x_4 list:member { - var:x_5 => false. - }. - } { - var:x_6 log:equalTo var:x_4. - } { - var:x_6 list:firstRest ({ - var:x_5 => false. - } var:x_4). - }) log:ifThenElseIn var:x_7. - var:x_8 graph:list var:x_6. - } => { - var:x_8 => var:x_1. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma11 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma12 a r:Inference; - r:gives { - true => { - { - :R a :Test. - } => false. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - :R a :Test. - } graph:list ({ - :R a :Test. - })}] - [ a r:Fact; r:gives {({ - :R a :Test. - }) list:select ({ - :R a :Test. - } ())}] - [ a r:Fact; r:gives {({ - { - :R a :Test. - } log:equalTo { - { - { - :R a :Test. - } => false. - } => false. - }. - } true { - { - { - :R a :Test. - } => false. - } log:equalTo { - { - :R a :Test. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {true graph:list ()}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :R a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true]; - r:rule skolem:lemma7. - diff --git a/reasoning/nand/test5.n3 b/reasoning/nand/test5.n3 deleted file mode 100644 index 531d8f5cc..000000000 --- a/reasoning/nand/test5.n3 +++ /dev/null @@ -1,24 +0,0 @@ -@prefix : . -@prefix log: . - -# P & Q -> R -{ - :P a :Test . - :Q a :Test . - { :R a :Test } => false . -} => false . - -# ~R -{ :R a :Test } => false . - -# |= ~(P & Q) -{ - { - :P a :Test . - :Q a :Test . - } => false . -} -=> -{ - :test :is true . -} . \ No newline at end of file diff --git a/reasoning/nand/test6-answer.n3 b/reasoning/nand/test6-answer.n3 deleted file mode 100644 index 7843b3f86..000000000 --- a/reasoning/nand/test6-answer.n3 +++ /dev/null @@ -1,3 +0,0 @@ -@prefix : . - -:test :is true. diff --git a/reasoning/nand/test6-proof.n3 b/reasoning/nand/test6-proof.n3 deleted file mode 100644 index df6da518e..000000000 --- a/reasoning/nand/test6-proof.n3 +++ /dev/null @@ -1,418 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix log: . -@prefix graph: . -@prefix list: . -@prefix n3: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:gives { - :test :is true. - }. - -skolem:lemma1 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma2 - ); - r:rule skolem:lemma3. - -skolem:lemma2 a r:Inference; - r:gives { - :test :is true. - }; - r:evidence ( - skolem:lemma4 - ); - r:rule skolem:lemma5. - -skolem:lemma3 a r:Extraction; - r:gives { - { - :test :is true. - } => { - :test :is true. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma4 a r:Inference; - r:gives { - { - :P a :Test. - } => false. - }; - r:evidence ( - skolem:lemma6 - skolem:lemma7 - ); - r:rule skolem:lemma8. - -skolem:lemma5 a r:Inference; - r:gives { - { - { - :P a :Test. - } => false. - } => { - :test :is true. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma9 - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - { - :P a :Test. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - } => false. - }) list:select ({ - { - :test :is true. - } => false. - } ({ - { - :P a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {({ - { - { - :test :is true. - } => false. - } log:equalTo { - { - :test :is true. - } => false. - }. - } true { - { - :test :is true. - } log:equalTo { - { - { - :test :is true. - } => false. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :test :is true. - } => false. - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - { - :test :is true. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:rule skolem:lemma10. - -skolem:lemma6 a r:Extraction; - r:gives { - :Q a :Test. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma7 a r:Extraction; - r:gives { - :R a :Test. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma8 a r:Inference; - r:gives { - { - :Q a :Test. - :R a :Test. - } => { - { - :P a :Test. - } => false. - }. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - :R a :Test. - } => false}] - [ a r:Fact; r:gives {{ - :P a :Test. - :Q a :Test. - :R a :Test. - } graph:list ({ - :P a :Test. - } { - :Q a :Test. - } { - :R a :Test. - })}] - [ a r:Fact; r:gives {({ - :P a :Test. - } { - :Q a :Test. - } { - :R a :Test. - }) list:select ({ - :P a :Test. - } ({ - :Q a :Test. - } { - :R a :Test. - }))}] - [ a r:Fact; r:gives {({ - { - :P a :Test. - } log:equalTo { - { - { - :P a :Test. - } => false. - } => false. - }. - } true { - { - { - :P a :Test. - } => false. - } log:equalTo { - { - :P a :Test. - } => false. - }. - }) log:ifThenElseIn (( ) 1)}] - [ a r:Fact; r:gives {{ - :Q a :Test. - :R a :Test. - } graph:list ({ - :Q a :Test. - } { - :R a :Test. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - :P a :Test. - :Q a :Test. - :R a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ({ - :P a :Test. - } { - :Q a :Test. - } { - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo { - :P a :Test. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - :Q a :Test. - } { - :R a :Test. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo { - :Q a :Test. - :R a :Test. - }]; - r:rule skolem:lemma10. - -skolem:lemma9 a r:Inference; - r:gives { - { - { - :test :is true. - } => false. - { - :P a :Test. - } => false. - } => false. - }; - r:evidence ( - [ a r:Fact; r:gives { log:equalTo }] - skolem:lemma5 - [ a r:Fact; r:gives {{ - :test :is true. - } log:notEqualTo false}] - [ a r:Fact; r:gives {{ - { - :P a :Test. - } => false. - } graph:list ({ - { - :P a :Test. - } => false. - })}] - [ a r:Fact; r:gives {({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - } => false. - }) list:firstRest ({ - { - :test :is true. - } => false. - } ({ - { - :P a :Test. - } => false. - }))}] - [ a r:Fact; r:gives {{ - { - :test :is true. - } => false. - { - :P a :Test. - } => false. - } graph:list ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - } => false. - })}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { - { - :P a :Test. - } => false. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo { - :test :is true. - }]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ({ - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({ - { - :test :is true. - } => false. - } { - { - :P a :Test. - } => false. - })]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo { - { - :test :is true. - } => false. - { - :P a :Test. - } => false. - }]; - r:rule skolem:lemma11. - -skolem:lemma10 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. { - log:equalTo . - var:x_0 => false. - var:x_0 graph:list var:x_1. - var:x_1 list:select (var:x_2 var:x_3). - ({ - var:x_2 log:equalTo { - var:x_4 => false. - }. - } true { - var:x_4 log:equalTo { - var:x_2 => false. - }. - }) log:ifThenElseIn var:x_5. - var:x_6 graph:list var:x_3. - } => { - var:x_6 => var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma11 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - log:equalTo . - var:x_0 => var:x_1. - var:x_1 log:notEqualTo false. - var:x_0 graph:list var:x_2. - var:x_3 list:firstRest ({ - var:x_1 => false. - } var:x_2). - var:x_4 graph:list var:x_3. - } => { - var:x_4 => false. - }. - }; - r:because [ a r:Parsing; r:source ]. - diff --git a/reasoning/nand/test6.n3 b/reasoning/nand/test6.n3 deleted file mode 100644 index 1b737156b..000000000 --- a/reasoning/nand/test6.n3 +++ /dev/null @@ -1,24 +0,0 @@ -@prefix : . -@prefix log: . - -# P & Q & R -> false -{ - :P a :Test . - :Q a :Test . - :R a :Test . -} => false . - -# Q -:Q a :Test . - -# R -:R a :Test . - -# |= ~P -{ - { :P a :Test . } => false . -} -=> -{ - :test :is true . -} . \ No newline at end of file diff --git a/reasoning/nand/v1-answer.n3 b/reasoning/nand/v1-answer.n3 deleted file mode 100644 index e69de29bb..000000000 diff --git a/reasoning/nand/v1-fuse.err b/reasoning/nand/v1-fuse.err deleted file mode 100644 index 9a884d0d0..000000000 --- a/reasoning/nand/v1-fuse.err +++ /dev/null @@ -1,17 +0,0 @@ -** ERROR ** eam ** inference_fuse( -@prefix : . -@prefix log: . -@prefix list: . -@prefix graph: . -@prefix r: . -@prefix var: . -@prefix skolem: . -@prefix n3: . - -:Result :is :A. -:Result :is :B. -# inference fuse -{ - :Result :is :B. -} => false. -) diff --git a/reasoning/nand/v1.n3 b/reasoning/nand/v1.n3 deleted file mode 100644 index b58daef87..000000000 --- a/reasoning/nand/v1.n3 +++ /dev/null @@ -1,25 +0,0 @@ -@prefix : . -@prefix log: . - -{ - { :X a :Test } => { :Y a :Test } . -} -=> -{ - :Result :is :A . - { :Result :is :B } => false . -} . - -{ - { - :X a :Test . - { :Y a :Test } => false . - } => false . -} -=> -{ - { :Result :is :A } => false . - :Result :is :B . -} . - -{ :X a :Test } => { :Y a :Test } .