Skip to content

Commit

Permalink
refreshing
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Dec 12, 2024
1 parent 16294e1 commit dbbdb9f
Show file tree
Hide file tree
Showing 9 changed files with 135 additions and 21 deletions.
3 changes: 3 additions & 0 deletions reasoning/proof-by-contrapositive/example1-answer.n3
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
@prefix : <urn:example:>.

{
:ground :is :wet.
} => false.
{
:it :is :raining.
} => false.
62 changes: 45 additions & 17 deletions reasoning/proof-by-contrapositive/example1-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,11 @@

skolem:proof a r:Proof, r:Conjunction;
r:component skolem:lemma1;
r:component skolem:lemma2;
r:gives {
{
:ground :is :wet.
} => false.
{
:it :is :raining.
} => false.
Expand All @@ -15,13 +19,16 @@ skolem:proof a r:Proof, r:Conjunction;
skolem:lemma1 a r:Inference;
r:gives {
{
:it :is :raining.
:ground :is :wet.
} => false.
};
r:evidence (
skolem:lemma2
[ a r:Fact; r:gives {{
:ground :is :wet.
} => false}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:raining"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:ground"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:wet"]];
r:rule skolem:lemma3.

skolem:lemma2 a r:Inference;
Expand All @@ -31,36 +38,57 @@ skolem:lemma2 a r:Inference;
} => false.
};
r:evidence (
[ a r:Fact; r:gives {{
:ground :is :wet.
} => false}]
skolem:lemma4
);
r:rule skolem:lemma4.
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:it"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:raining"]];
r:rule skolem:lemma3.

skolem:lemma3 a r:Extraction;
r:gives {
@forAll var:x_0. {
@forAll var:x_0, var:x_1. {
{
:it :is var:x_0.
var:x_0 :is var:x_1.
} => false.
} => {
{
:it :is var:x_0.
var:x_0 :is var:x_1.
} => false.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example1-query.n3>].

skolem:lemma4 a r:Extraction;
skolem:lemma4 a r:Inference;
r:gives {
{
{
:ground :is :wet.
} => false.
:it :is :raining.
} => false.
};
r:evidence (
[ a r:Fact; r:gives {{
:it :is :raining.
} => {
{
:it :is :raining.
} => false.
:ground :is :wet.
}}]
[ a r:Fact; r:gives {{
:ground :is :wet.
} => false}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
:it :is :raining.
}];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo {
:ground :is :wet.
}];
r:rule skolem:lemma5.

skolem:lemma5 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {
var:x_0 => var:x_1.
var:x_1 => false.
} => {
var:x_0 => false.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example1.n3>].
Expand Down
4 changes: 2 additions & 2 deletions reasoning/proof-by-contrapositive/example1-query.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

# query
{
{ :it :is ?X } => false.
{ ?X :is ?Y } => false.
} => {
{ :it :is ?X } => false.
{ ?X :is ?Y } => false.
}.
7 changes: 5 additions & 2 deletions reasoning/proof-by-contrapositive/example1.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,8 @@
# the ground is not wet
{ :ground :is :wet } => false.

# contrapositive of "if it is raining, then the ground is wet".
{ { :ground :is :wet } => false } => { { :it :is :raining } => false }.
# if it is raining, then the ground is wet
{ :it :is :raining } => { :ground :is :wet }.

# proof by contrapositive
{ ?P => ?C. ?C => false } => { ?P => false }.
3 changes: 3 additions & 0 deletions reasoning/proof-by-contrapositive/example2-answer.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
@prefix : <urn:example:>.

:ground :is :wet.
59 changes: 59 additions & 0 deletions reasoning/proof-by-contrapositive/example2-proof.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix : <urn:example:>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.

skolem:proof a r:Proof, r:Conjunction;
r:component skolem:lemma1;
r:gives {
:ground :is :wet.
}.

skolem:lemma1 a r:Inference;
r:gives {
:ground :is :wet.
};
r:evidence (
skolem:lemma2
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:ground"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:wet"]];
r:rule skolem:lemma3.

skolem:lemma2 a r:Inference;
r:gives {
:ground :is :wet.
};
r:evidence (
[ a r:Fact; r:gives {{
{
:ground :is :wet.
} => false.
} => false}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
:ground :is :wet.
}];
r:rule skolem:lemma4.

skolem:lemma3 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {
var:x_0 :is var:x_1.
} => {
var:x_0 :is var:x_1.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2-query.n3>].

skolem:lemma4 a r:Extraction;
r:gives {
@forAll var:x_0. {
{
var:x_0 => false.
} => false.
} => var:x_0.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2.n3>].

8 changes: 8 additions & 0 deletions reasoning/proof-by-contrapositive/example2-query.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
@prefix : <urn:example:>.

# query
{
?X :is ?Y.
} => {
?X :is ?Y.
}.
8 changes: 8 additions & 0 deletions reasoning/proof-by-contrapositive/example2.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <urn:example:>.

# the ground is not not wet
{ { :ground :is :wet } => false } => false.

# proof by contrapositive
{ { ?P => false } => false } => ?P.
2 changes: 2 additions & 0 deletions reasoning/proof-by-contrapositive/test
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
#!/bin/bash
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example1.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example1-query.n3 --output example1-answer.n3
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example1.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example1-query.n3 --output example1-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/proof-by-contrapositive/example2.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2-query.n3 --output example2-answer.n3
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2.n3 --query https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2-query.n3 --output example2-proof.n3

0 comments on commit dbbdb9f

Please sign in to comment.