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 bf2d9fd commit 718dcdf
Show file tree
Hide file tree
Showing 7 changed files with 523 additions and 141 deletions.
41 changes: 17 additions & 24 deletions reasoning/nand/nand.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,41 +6,34 @@
@prefix graph: <http://www.w3.org/2000/10/swap/graph#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

# contrapositive rules
# contrapositive rule
{
<#nand> log:equalTo <#nand>.
?P => false.
?P graph:list ?Q.
?Q list:select ({ ?A => false } ?B).
?R graph:list ?B.
} => {
?R => ?A.
}.

{
<#nand> log:equalTo <#nand>.
?P => false.
?P graph:list ?Q.
?Q list:select (?A ?B).
?A log:notIsomorphic { ?X => false }.
?P graph:list ?L.
?L list:select (?A ?B).
( { ?A log:notIsomorphic { ?X => false } }
{ ?C log:equalTo { ?A => false } }
{ ?A log:equalTo { ?C => false } }
) log:ifThenElseIn ?SCOPE.
?R graph:list ?B.
} => {
?R => { ?A => false }.
?R => ?C.
}.

# resolution rule
{
<#nand> log:equalTo <#nand>.
?A => ?B.
?A graph:list ?L.
?P => ?C.
?P graph:list ?L.
?L list:notMember { <#nand> log:equalTo <#nand> }.
?L list:select ({ ?C => false } ?M).
?C => ?E.
( { ?M list:member { ?E => false } }
{ ?N log:equalTo ?M }
{ ?N list:firstRest ({ ?E => false } ?M) }
?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.
?F graph:list ?N.
?R graph:list ?M.
} => {
?F => ?B.
?R => ?C.
}.
63 changes: 55 additions & 8 deletions reasoning/nand/test1-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,35 @@ skolem:lemma6 a r:Inference;
:P a :Test.
} => false.
} ())}]
[ a r:Fact; r:gives {({
{
{
:P a :Test.
} => false.
} log:notIsomorphic {
_:sk_0 => false.
}.
} {
{
:P a :Test.
} log:equalTo {
{
{
:P a :Test.
} => 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 ()}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
Expand All @@ -104,24 +133,42 @@ skolem:lemma6 a r:Inference;
} => false.
})];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo {
:P a :Test.
{
: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_4"]; r:boundTo true];
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 {
:P a :Test.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; 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. {
@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. {
<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 => false.
} var:x_3).
var:x_4 graph:list var:x_3.
var:x_1 list:select (var:x_2 var:x_3).
({
var:x_2 log:notIsomorphic {
var:x_4 => false.
}.
} {
var:x_5 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.
} => {
var:x_4 => var:x_2.
var:x_7 => var:x_5.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
Expand Down
63 changes: 55 additions & 8 deletions reasoning/nand/test2-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,35 @@ skolem:lemma8 a r:Inference;
} {
:Q a :Test.
}))}]
[ a r:Fact; r:gives {({
{
{
:R a :Test.
} => false.
} log:notIsomorphic {
_:sk_2 => false.
}.
} {
{
:R a :Test.
} log:equalTo {
{
{
:R a :Test.
} => 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.
:Q a :Test.
Expand All @@ -149,31 +178,49 @@ skolem:lemma8 a r:Inference;
} => false.
})];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo {
:R a :Test.
{
: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_4"]; 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/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 a :Test.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; 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. {
@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. {
<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 => false.
} var:x_3).
var:x_4 graph:list var:x_3.
var:x_1 list:select (var:x_2 var:x_3).
({
var:x_2 log:notIsomorphic {
var:x_4 => false.
}.
} {
var:x_5 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.
} => {
var:x_4 => var:x_2.
var:x_7 => var:x_5.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
Expand Down
Loading

0 comments on commit 718dcdf

Please sign in to comment.