Skip to content

Commit

Permalink
fixing contrapositive
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Dec 14, 2024
1 parent be2acf7 commit 0134001
Show file tree
Hide file tree
Showing 13 changed files with 3,241 additions and 580 deletions.
717 changes: 572 additions & 145 deletions reasoning/nand/ab-proof.n3
View file

Large diffs are not rendered by default.

11 changes: 11 additions & 0 deletions reasoning/nand/nand.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,17 @@
?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>.
Expand Down
2 changes: 2 additions & 0 deletions reasoning/nand/test
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,3 +19,5 @@ eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https:/

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
235 changes: 226 additions & 9 deletions reasoning/nand/test1-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,15 +50,98 @@ skolem:lemma4 a r:Inference;
);
r:rule skolem:lemma6.

skolem:lemma5 a r:Extraction;
skolem:lemma5 a r:Inference;
r:gives {
{
:P a :Test.
} => {
:test :is true.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/test1.n3>].
r:evidence (
[ a r:Fact; r:gives {<https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>}]
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 ((<https://eyereasoner.github.io/eye/reasoning/nand/test1.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 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 ((<https://eyereasoner.github.io/eye/reasoning/nand/test1.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 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 {
Expand All @@ -68,11 +151,7 @@ skolem:lemma6 a r:Inference;
};
r:evidence (
[ a r:Fact; r:gives {<https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>}]
[ a r:Fact; r:gives {{
{
:P a :Test.
} => false.
} => false}]
skolem:lemma9
[ a r:Fact; r:gives {{
{
:P a :Test.
Expand Down Expand Up @@ -135,9 +214,79 @@ skolem:lemma6 a r:Inference;
: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:lemma7.
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 {<https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>}]
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:lemma7 a r:Extraction;
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. {
<https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
Expand All @@ -160,3 +309,71 @@ skolem:lemma7 a r:Extraction;
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].

skolem:lemma9 a r:Inference;
r:gives {
{
{
:P a :Test.
} => false.
} => false.
};
r:evidence (
[ a r:Fact; r:gives {<https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>}]
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. {
<https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
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 <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].

3 changes: 1 addition & 2 deletions reasoning/nand/test1.n3
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
@prefix : <urn:example:> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .

# ~~P
{
Expand All @@ -13,4 +12,4 @@
=>
{
:test :is true .
} .
} .
Loading

0 comments on commit 0134001

Please sign in to comment.