Skip to content

Commit

Permalink
beautifying the output of graph literals
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Jan 22, 2023
1 parent e0bb8a3 commit 355ca83
Show file tree
Hide file tree
Showing 75 changed files with 35,670 additions and 9,654 deletions.
1 change: 1 addition & 0 deletions RELEASE
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
EYE release

[v2.3.5] beautifying the output of graph literals
[v2.3.4] adding experimental log:graffiti built-in as used in https://github.com/eyereasoner/eye/blob/master/reasoning/blogic/parteval.n3
[v2.3.3] fixing https://github.com/eyereasoner/eye/blob/master/reasoning/blogic/beetle13.n3 (obs from Dörthe Arndt)
[v2.3.2] improving readability of blogic graphs (obs from Ruben Dedecker)
Expand Down
2 changes: 1 addition & 1 deletion VERSION
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
2.3.4
2.3.5
23 changes: 20 additions & 3 deletions eye.pl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
:- use_module(library(semweb/turtle)).
:- catch(use_module(library(http/http_open)), _, true).

version_info('EYE v2.3.4 josd').
version_info('EYE v2.3.5 josd').

license_info('MIT License

Expand Down Expand Up @@ -4362,13 +4362,30 @@
)
)
-> write('{'),
indentation(1),
indentation(4),
( ( flag(strings)
; flag(nope),
\+flag(blogic)
)
-> true
; nl,
indent
),
nb_getval(fdepth, D),
E is D+1,
nb_setval(fdepth, E),
wt(X),
nb_setval(fdepth, D),
indentation(-1),
indentation(-4),
( ( flag(strings)
; flag(nope),
\+flag(blogic)
)
-> true
; write('.'),
nl,
indent
),
write('}')
; wt(X)
).
Expand Down
Binary file modified eye.zip
View file
Binary file not shown.
156 changes: 115 additions & 41 deletions reasoning/3outof5/answer.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,16 +19,26 @@ skolem:lemma1 a r:Inference;
};
r:evidence (
skolem:lemma2
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {1 log:equalTo 0}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p2 true.
0 log:equalTo 1}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
1 log:equalTo 0.
}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p2 true.
0 log:equalTo 1.
}}]
skolem:lemma3
skolem:lemma4
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {1 log:equalTo 0}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
1 log:equalTo 0.
}}]
skolem:lemma5
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {1 log:equalTo 0}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p5 true.
0 log:equalTo 1}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
1 log:equalTo 0.
}}]
[ a r:Fact; r:gives {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p5 true.
0 log:equalTo 1.
}}]
skolem:lemma3
[ a r:Fact; r:gives {(1 0 1 1 0) math:sum 3}]
[ a r:Fact; r:gives {3 math:notLessThan 3}]
Expand All @@ -44,71 +54,135 @@ skolem:lemma1 a r:Inference;

skolem:lemma2 a r:Inference;
r:gives {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p1 true.
1 log:equalTo 1}.
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p1 true.
1 log:equalTo 1.
}.
};
r:evidence (
skolem:lemma7
[ a r:Fact; r:gives {1 log:equalTo 1}]
);
r:rule [ a r:Fact; r:gives {{:s :p1 true.
1 log:equalTo 1} => {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p1 true.
1 log:equalTo 1}}}].
r:rule [ a r:Fact; r:gives {
{
:s :p1 true.
1 log:equalTo 1.
} => {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p1 true.
1 log:equalTo 1.
}.
}.
}].

skolem:lemma3 a r:Inference;
r:gives {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {0 log:equalTo 0}.
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
0 log:equalTo 0.
}.
};
r:evidence (
[ a r:Fact; r:gives {0 log:equalTo 0}]
);
r:rule [ a r:Fact; r:gives {{0 log:equalTo 0} => {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {0 log:equalTo 0}}}].
r:rule [ a r:Fact; r:gives {
{
0 log:equalTo 0.
} => {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
0 log:equalTo 0.
}.
}.
}].

skolem:lemma4 a r:Inference;
r:gives {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p3 true.
1 log:equalTo 1}.
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p3 true.
1 log:equalTo 1.
}.
};
r:evidence (
skolem:lemma8
[ a r:Fact; r:gives {1 log:equalTo 1}]
);
r:rule [ a r:Fact; r:gives {{:s :p3 true.
1 log:equalTo 1} => {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p3 true.
1 log:equalTo 1}}}].
r:rule [ a r:Fact; r:gives {
{
:s :p3 true.
1 log:equalTo 1.
} => {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p3 true.
1 log:equalTo 1.
}.
}.
}].

skolem:lemma5 a r:Inference;
r:gives {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p4 true.
1 log:equalTo 1}.
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p4 true.
1 log:equalTo 1.
}.
};
r:evidence (
skolem:lemma9
[ a r:Fact; r:gives {1 log:equalTo 1}]
);
r:rule [ a r:Fact; r:gives {{:s :p4 true.
1 log:equalTo 1} => {((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {:s :p4 true.
1 log:equalTo 1}}}].
r:rule [ a r:Fact; r:gives {
{
:s :p4 true.
1 log:equalTo 1.
} => {
((<http://eyereasoner.github.io/eye/reasoning/3outof5/sample.n3>) 1) e:optional {
:s :p4 true.
1 log:equalTo 1.
}.
}.
}].

skolem:lemma6 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_0 e:optional {:s :p1 true.
var:x_1 log:equalTo 1}.
var:x_0 e:optional {var:x_1 log:equalTo 0}.
var:x_0 e:optional {:s :p2 true.
var:x_2 log:equalTo 1}.
var:x_0 e:optional {var:x_2 log:equalTo 0}.
var:x_0 e:optional {:s :p3 true.
var:x_3 log:equalTo 1}.
var:x_0 e:optional {var:x_3 log:equalTo 0}.
var:x_0 e:optional {:s :p4 true.
var:x_4 log:equalTo 1}.
var:x_0 e:optional {var:x_4 log:equalTo 0}.
var:x_0 e:optional {:s :p5 true.
var:x_5 log:equalTo 1}.
var:x_0 e:optional {var:x_5 log:equalTo 0}.
(var:x_1 var:x_2 var:x_3 var:x_4 var:x_5) math:sum var:x_6.
var:x_6 math:notLessThan 3} => {:s a :3outof5}.
@forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
var:x_0 e:optional {
:s :p1 true.
var:x_1 log:equalTo 1.
}.
var:x_0 e:optional {
var:x_1 log:equalTo 0.
}.
var:x_0 e:optional {
:s :p2 true.
var:x_2 log:equalTo 1.
}.
var:x_0 e:optional {
var:x_2 log:equalTo 0.
}.
var:x_0 e:optional {
:s :p3 true.
var:x_3 log:equalTo 1.
}.
var:x_0 e:optional {
var:x_3 log:equalTo 0.
}.
var:x_0 e:optional {
:s :p4 true.
var:x_4 log:equalTo 1.
}.
var:x_0 e:optional {
var:x_4 log:equalTo 0.
}.
var:x_0 e:optional {
:s :p5 true.
var:x_5 log:equalTo 1.
}.
var:x_0 e:optional {
var:x_5 log:equalTo 0.
}.
(var:x_1 var:x_2 var:x_3 var:x_4 var:x_5) math:sum var:x_6.
var:x_6 math:notLessThan 3.
} => {
:s a :3outof5.
}.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/3outof5/query.n3>].

Expand Down
Loading

0 comments on commit 355ca83

Please sign in to comment.