Skip to content

Commit

Permalink
refreshing
Browse files Browse the repository at this point in the history
  • Loading branch information
josd committed Nov 9, 2024
1 parent 72f9085 commit d5d150c
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 17 deletions.
2 changes: 1 addition & 1 deletion color/age/age-answer.n3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
@prefix : <https://example.org/#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.

:patH :ageAbove "P75Y"^^xsd:duration.
:patH :ageAbove "P80Y"^^xsd:duration.
26 changes: 13 additions & 13 deletions color/age/age-proof.n3
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,19 @@
@prefix : <https://example.org/#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.
@prefix time: <http://www.w3.org/2000/10/swap/time#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.

skolem:proof a r:Proof, r:Conjunction;
r:component skolem:lemma1;
r:gives {
:patH :ageAbove "P75Y"^^xsd:duration.
:patH :ageAbove "P80Y"^^xsd:duration.
}.

skolem:lemma1 a r:Inference;
r:gives {
:patH :ageAbove "P75Y"^^xsd:duration.
:patH :ageAbove "P80Y"^^xsd:duration.
};
r:evidence (
skolem:lemma2
Expand All @@ -25,27 +25,27 @@ skolem:lemma1 a r:Inference;

skolem:lemma2 a r:Inference;
r:gives {
:patH :ageAbove "P75Y"^^xsd:duration.
:patH :ageAbove "P80Y"^^xsd:duration.
};
r:evidence (
skolem:lemma4
[ a r:Fact; r:gives {"" time:localTime "2024-11-09T22:55:46.629Z"^^xsd:dateTime}]
[ a r:Fact; r:gives {("2024-11-09T22:55:46.629Z"^^xsd:dateTime "1944-08-21"^^xsd:date) math:difference 2531602546.6289997}]
[ a r:Fact; r:gives {2531602546.6289997 math:greaterThan "P75Y"^^xsd:duration}]
[ a r:Fact; r:gives {"2024-08-21T00:00:00.0Z"^^xsd:dateTime log:equalTo "2024-08-21T00:00:00.0Z"^^xsd:dateTime}]
[ a r:Fact; r:gives {("2024-08-21T00:00:00.0Z"^^xsd:dateTime "1944-08-21"^^xsd:date) math:difference 2524608000.0}]
[ a r:Fact; r:gives {2524608000.0 math:greaterThan "P80Y"^^xsd:duration}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "https://example.org/#patH"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo "1944-08-21"^^xsd:date];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo "2024-11-09T22:55:46.629Z"^^xsd:dateTime];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 2531602546.6289997];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo "P75Y"^^xsd:duration];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo "2024-08-21T00:00:00.0Z"^^xsd:dateTime];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 2524608000.0];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo "P80Y"^^xsd:duration];
r:rule skolem:lemma5.

skolem:lemma3 a r:Extraction;
r:gives {
@forAll var:x_0. {
var:x_0 :ageAbove "P75Y"^^xsd:duration.
var:x_0 :ageAbove "P80Y"^^xsd:duration.
} => {
var:x_0 :ageAbove "P75Y"^^xsd:duration.
var:x_0 :ageAbove "P80Y"^^xsd:duration.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/age/age-query.n3>].
Expand All @@ -62,7 +62,7 @@ skolem:lemma5 a r:Extraction;
var:x_0 :ageAbove var:x_4.
} <= {
var:x_0 :birthDay var:x_1.
"" time:localTime var:x_2.
var:x_2 log:equalTo "2024-08-21T00:00:00.0Z"^^xsd:dateTime.
(var:x_2 var:x_1) math:difference var:x_3.
var:x_3 math:greaterThan var:x_4.
}.
Expand Down
4 changes: 2 additions & 2 deletions color/age/age-query.n3
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

# query
{
?S :ageAbove "P75Y"^^xsd:duration.
?S :ageAbove "P80Y"^^xsd:duration.
} => {
?S :ageAbove "P75Y"^^xsd:duration.
?S :ageAbove "P80Y"^^xsd:duration.
}.
4 changes: 3 additions & 1 deletion color/age/age.n3
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix time: <http://www.w3.org/2000/10/swap/time#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <https://example.org/#>.

# person data
Expand All @@ -9,7 +10,8 @@
# is the age of a person above some duration?
{ ?S :ageAbove ?A } <= {
?S :birthDay ?B.
"" time:localTime ?D.
#"" time:localTime ?D.
?D log:equalTo "2024-08-21T00:00:00.0Z"^^xsd:dateTime.
(?D ?B) math:difference ?F.
?F math:greaterThan ?A.
}.

0 comments on commit d5d150c

Please sign in to comment.