Skip to content

Commit

Permalink
refreshing
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Dec 13, 2024
1 parent 718dcdf commit 65ae898
Show file tree
Hide file tree
Showing 7 changed files with 140 additions and 255 deletions.
4 changes: 2 additions & 2 deletions reasoning/nand/nand.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@
?P => false.
?P graph:list ?L.
?L list:select (?A ?B).
( { ?A log:notIsomorphic { ?X => false } }
( { ?A log:equalTo { ?C => false } }
true
{ ?C log:equalTo { ?A => false } }
{ ?A log:equalTo { ?C => false } }
) log:ifThenElseIn ?SCOPE.
?R graph:list ?B.
} => {
Expand Down
43 changes: 15 additions & 28 deletions reasoning/nand/test1-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,10 +96,12 @@ skolem:lemma6 a r:Inference;
{
:P a :Test.
} => false.
} log:notIsomorphic {
_:sk_0 => false.
} log:equalTo {
{
:P a :Test.
} => false.
}.
} {
} true {
{
:P a :Test.
} log:equalTo {
Expand All @@ -109,16 +111,6 @@ skolem:lemma6 a r:Inference;
} => false.
} => false.
}.
} {
{
{
:P a :Test.
} => false.
} log:equalTo {
{
:P a :Test.
} => 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 {true graph:list ()}]
);
Expand All @@ -138,37 +130,32 @@ skolem:lemma6 a r:Inference;
} => 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_6"]; 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 [ a r:Existential; n3:nodeId "_:sk_0"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
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 {
:P a :Test.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
r:rule skolem:lemma7.

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. {
@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>.
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:notIsomorphic {
var:x_2 log:equalTo {
var:x_4 => false.
}.
} {
var:x_5 log:equalTo {
} true {
var:x_4 log:equalTo {
var:x_2 => false.
}.
} {
var:x_2 log:equalTo {
var:x_5 => false.
}.
}) log:ifThenElseIn var:x_6.
var:x_7 graph:list var:x_3.
}) log:ifThenElseIn var:x_5.
var:x_6 graph:list var:x_3.
} => {
var:x_7 => var:x_5.
var:x_6 => var:x_4.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
Expand Down
43 changes: 15 additions & 28 deletions reasoning/nand/test2-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,10 +128,12 @@ skolem:lemma8 a r:Inference;
{
:R a :Test.
} => false.
} log:notIsomorphic {
_:sk_2 => false.
} log:equalTo {
{
:R a :Test.
} => false.
}.
} {
} true {
{
:R a :Test.
} log:equalTo {
Expand All @@ -141,16 +143,6 @@ skolem:lemma8 a r:Inference;
} => false.
} => false.
}.
} {
{
{
:R a :Test.
} => false.
} log:equalTo {
{
:R a :Test.
} => false.
}.
}) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test2.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
[ a r:Fact; r:gives {{
:P a :Test.
Expand Down Expand Up @@ -187,40 +179,35 @@ skolem:lemma8 a r:Inference;
} {
:Q a :Test.
})];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test2.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 [ a r:Existential; n3:nodeId "_:sk_2"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
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/test2.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 {
:R a :Test.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
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:lemma9.

skolem:lemma9 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. {
@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>.
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:notIsomorphic {
var:x_2 log:equalTo {
var:x_4 => false.
}.
} {
var:x_5 log:equalTo {
} true {
var:x_4 log:equalTo {
var:x_2 => false.
}.
} {
var:x_2 log:equalTo {
var:x_5 => false.
}.
}) log:ifThenElseIn var:x_6.
var:x_7 graph:list var:x_3.
}) log:ifThenElseIn var:x_5.
var:x_6 graph:list var:x_3.
} => {
var:x_7 => var:x_5.
var:x_6 => var:x_4.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
Expand Down
97 changes: 35 additions & 62 deletions reasoning/nand/test3-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,10 +162,12 @@ skolem:lemma8 a r:Inference;
{
:Q a :Test.
} => false.
} log:notIsomorphic {
_:sk_1 => false.
} log:equalTo {
{
:Q a :Test.
} => false.
}.
} {
} true {
{
:Q a :Test.
} log:equalTo {
Expand All @@ -175,16 +177,6 @@ skolem:lemma8 a r:Inference;
} => false.
} => false.
}.
} {
{
{
:Q a :Test.
} => false.
} log:equalTo {
{
:Q a :Test.
} => false.
}.
}) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
[ a r:Fact; r:gives {{
{
Expand Down Expand Up @@ -241,12 +233,11 @@ skolem:lemma8 a r:Inference;
:R a :Test.
} => false.
})];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.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 [ a r:Existential; n3:nodeId "_:sk_1"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
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/test3.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 {
:Q a :Test.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
{
:P a :Test.
} => false.
Expand Down Expand Up @@ -280,10 +271,14 @@ skolem:lemma9 a r:Inference;
[ a r:Fact; r:gives {({
{
:P a :Test.
} log:notIsomorphic {
_:sk_3 => false.
} log:equalTo {
{
{
:P a :Test.
} => false.
} => false.
}.
} {
} true {
{
{
:P a :Test.
Expand All @@ -293,16 +288,6 @@ skolem:lemma9 a r:Inference;
:P a :Test.
} => false.
}.
} {
{
:P a :Test.
} log:equalTo {
{
{
:P a :Test.
} => false.
} => false.
}.
}) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
[ a r:Fact; r:gives {true graph:list ()}]
);
Expand All @@ -316,14 +301,13 @@ skolem:lemma9 a r:Inference;
: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_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.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 [ a r:Existential; n3:nodeId "_:sk_3"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
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/test3.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 {
{
:P a :Test.
} => false.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
r:rule skolem:lemma11.

skolem:lemma10 a r:Inference;
Expand All @@ -350,10 +334,14 @@ skolem:lemma10 a r:Inference;
[ a r:Fact; r:gives {({
{
:R a :Test.
} log:notIsomorphic {
_:sk_4 => false.
} log:equalTo {
{
{
:R a :Test.
} => false.
} => false.
}.
} {
} true {
{
{
:R a :Test.
Expand All @@ -363,16 +351,6 @@ skolem:lemma10 a r:Inference;
:R a :Test.
} => false.
}.
} {
{
:R a :Test.
} log:equalTo {
{
{
:R a :Test.
} => false.
} => false.
}.
}) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
[ a r:Fact; r:gives {true graph:list ()}]
);
Expand All @@ -386,39 +364,34 @@ skolem:lemma10 a r:Inference;
: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_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.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 [ a r:Existential; n3:nodeId "_:sk_4"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
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/test3.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 {
{
:R a :Test.
} => false.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
r:rule skolem:lemma11.

skolem:lemma11 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. {
@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>.
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:notIsomorphic {
var:x_2 log:equalTo {
var:x_4 => false.
}.
} {
var:x_5 log:equalTo {
} true {
var:x_4 log:equalTo {
var:x_2 => false.
}.
} {
var:x_2 log:equalTo {
var:x_5 => false.
}.
}) log:ifThenElseIn var:x_6.
var:x_7 graph:list var:x_3.
}) log:ifThenElseIn var:x_5.
var:x_6 graph:list var:x_3.
} => {
var:x_7 => var:x_5.
var:x_6 => var:x_4.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
Expand Down
Loading

0 comments on commit 65ae898

Please sign in to comment.