Skip to content

Commit

Permalink
using RDF star to describe logic rules and queries
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Oct 18, 2024
1 parent 761753c commit 9d79eaa
Show file tree
Hide file tree
Showing 112 changed files with 5,135 additions and 8,675 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

v10.26.0 (2024-10-18) using RDF star to describe logic rules and queries
v10.25.2 (2024-10-17) having functional terms as reifiedtriples << functor func:args (arguments) >>
v10.25.1 (2024-10-17) having functional terms as triple terms <<( functor func:args (arguments) )>>
v10.25.0 (2024-10-17) introducing (^ functor args) functional terms
Expand Down
2 changes: 1 addition & 1 deletion VERSION
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
10.25.2
10.26.0
1 change: 1 addition & 0 deletions eye-builtins.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,7 @@ log:includes a e:Builtin.
log:includesNotBind a e:Builtin.
log:inferences a e:Builtin.
log:isBuiltin a e:Builtin.
log:isFunctorOf a e:Builtin.
log:isImpliedBy a e:Builtin.
log:isomorphic a e:Builtin.
log:langlit a e:Builtin.
Expand Down
127 changes: 42 additions & 85 deletions eye.pl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
:- catch(use_module(library(process)), _, true).
:- catch(use_module(library(http/http_open)), _, true).

version_info('EYE v10.25.2 (2024-10-17)').
version_info('EYE v10.26.0 (2024-10-18)').

license_info('MIT License

Expand Down Expand Up @@ -382,7 +382,6 @@
nb_setval(current_scope, '<>'),
nb_setval(doc_nr, 0),
nb_setval(wn, 0),
nb_setval(prepare, false),
opts(Argus, Args),
( Args = []
-> opts(['--help'], _)
Expand Down Expand Up @@ -1545,7 +1544,6 @@
write(query(\+Y, true)),
writeln('.').
tr_n3p(['\'<http://www.w3.org/2000/10/swap/log#implies>\''(X, Y)|Z], Src, query) :-
\+ (atomic(X), atomic(Y)),
!,
( Y = '\'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#csvTuple>\''(L, T)
-> ( is_list(T)
Expand Down Expand Up @@ -1580,7 +1578,6 @@
),
tr_n3p(Z, Src, query).
tr_n3p([':-'(Y, X)|Z], Src, query) :-
\+ (atomic(X), atomic(Y)),
!,
( Y = '\'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#csvTuple>\''(L, T)
-> ( is_list(T)
Expand Down Expand Up @@ -1626,7 +1623,6 @@
),
tr_n3p(Z, Src, Mode).
tr_n3p(['\'<http://www.w3.org/2000/10/swap/log#implies>\''(X, Y)|Z], Src, Mode) :-
\+ (atomic(X), atomic(Y)),
!,
( flag(tactic, 'linear-select')
-> write(implies(X, '\'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#transaction>\''(X, Y), Src)),
Expand All @@ -1640,21 +1636,19 @@
tr_n3p([':-'(Y, X)|Z], Src, Mode) :-
!,
tr_tr(Y, U),
( atomic(X),
atomic(Y)
-> write('\'<http://www.w3.org/2000/10/swap/log#isImpliedBy>\''(U, X))
; write(':-'(U, X))
),
write(':-'(U, X)),
writeln('.'),
tr_n3p(Z, Src, Mode).
tr_n3p(['\'<http://www.w3.org/2000/10/swap/log#query>\''(X, Y)|Z], Src, Mode) :-
\+ (atomic(X), atomic(Y)),
!,
write('\'<http://www.w3.org/2000/10/swap/log#query>\''(X, Y)),
writeln('.'),
djiti_answer(answer(Y), A),
write(implies(X, A, Src)),
writeln('.'),
( X \= reifiedtriple(_, _, _, _),
Y \= reifiedtriple(_, _, _, _)
-> djiti_answer(answer(Y), A),
write(implies(X, A, Src)),
writeln('.')
; write('\'<http://www.w3.org/2000/10/swap/log#query>\''(X, Y)),
writeln('.')
),
tr_n3p(Z, Src, Mode).
tr_n3p(['\'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#tactic>\''(X, Y)|Z], Src, Mode) :-
!,
Expand Down Expand Up @@ -2151,7 +2145,10 @@
subject(S, []),
verb(P, []),
object(O, []),
[rp_gt_gt].
[rp_gt_gt],
{ retractall(flag(rdfstar)),
assertz(flag(rdfstar))
}.
pathitem(reifiedtriple(S, P, O, N), T) -->
[lt_lt],
!,
Expand All @@ -2164,7 +2161,10 @@
; append([Ts, Tp, To], T)
)
},
[gt_gt].
[gt_gt],
{ retractall(flag(rdfstar)),
assertz(flag(rdfstar))
}.
pathitem(Node, []) -->
['{'],
{ nb_getval(fdepth, I),
Expand Down Expand Up @@ -5287,8 +5287,8 @@
)
).
djiti_fact('<http://www.w3.org/2000/10/swap/log#query>'(A, B), C) :-
\+atomic(A),
\+atomic(B),
A \= reifiedtriple(_, _, _, _),
B \= reifiedtriple(_, _, _, _),
djiti_answer(answer(B), D),
makevars(implies(A, D, '<>'), C, zeta),
\+C,
Expand Down Expand Up @@ -5344,17 +5344,17 @@
%

prepare_builtins :-
nb_setval(prepare, true),

% rdflists
( clause('<http://www.w3.org/1999/02/22-rdf-syntax-ns#first>'(_, _), true)
-> retractall(flag(rdflists)),
assertz(flag(rdflists))
; true
),

% quads
( quad(triple(_, _, _), _)
% rdfstar
( ( quad(triple(_, _, _), _)
; flag(rdfstar)
)
-> % create trig graphs
( graphid(G),
findall(C,
Expand All @@ -5373,52 +5373,31 @@
; true
),

% create terms
( pred(P),
P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#first>',
P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#reifies>',
P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#rest>',
P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>',
P \= '<http://www.w3.org/1999/02/22-rdf-syntax-ns#value>',
P \= quad,
X =.. [P, _, _],
call(X),
ground(X),
getterm(X, Y),
( Y = X
-> true
; retract(X),
assertz(Y)
),
fail
; true
),

% create forward rules
assertz(implies((
'<http://www.w3.org/2000/10/swap/log#implies>'(A, B),
'<http://www.w3.org/2000/10/swap/graph#statement>'(A, C),
'<http://www.w3.org/2000/10/swap/graph#statement>'(B, D)
getterm(A, C),
getterm(B, D)
), '<http://www.w3.org/2000/10/swap/log#implies>'(C, D), '<>')),

% create backward rules
assertz(implies((
'<http://www.w3.org/2000/10/swap/log#isImpliedBy>'(A, B),
'<http://www.w3.org/2000/10/swap/graph#statement>'(A, C),
'<http://www.w3.org/2000/10/swap/graph#statement>'(B, D)
getterm(A, C),
getterm(B, D)
), ':-'(C, D), '<>')),

% create queries
assertz(implies((
'<http://www.w3.org/2000/10/swap/log#query>'(A, B),
'<http://www.w3.org/2000/10/swap/graph#statement>'(A, C),
'<http://www.w3.org/2000/10/swap/graph#statement>'(B, D)
getterm(A, C),
getterm(B, D)
), '<http://www.w3.org/2000/10/swap/log#query>'(C, D), '<>')),

% create rdfsurfaces
assertz(implies((
'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(A, B),
'<http://www.w3.org/2000/10/swap/graph#statement>'(B, C)
getterm(B, C)
), '<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(A, C), '<>'))
; forall(
retract('<http://www.w3.org/2000/10/swap/log#isImpliedBy>'(A, B)),
Expand Down Expand Up @@ -5731,8 +5710,7 @@
'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(_, I)
), false, '<>'))
; true
),
nb_setval(prepare, false).
).

'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#avg>'(A, B) :-
\+flag(restricted),
Expand Down Expand Up @@ -12761,43 +12739,22 @@
-> true
; throw(malformed_list_invalid_rest(E))
).
getterm(graph(A, B), graph(A, C)) :-
nb_getval(prepare, false),
graph(A, B),
!,
getterm(B, D),
conjify(D, C).
getterm(graph(A, B), '<http://www.w3.org/2000/10/swap/log#equalTo>'(B, C)) :-
nb_getval(prepare, false),
getconj(A, D),
D \= A,
getterm(reifiedtriple('<http://www.w3.org/2000/10/swap/log#conjunction>', '<http://www.w3.org/2000/10/swap/log#isFunctorOf>', A, _), B) :-
!,
getterm(D, E),
conjify(E, C).
getterm(A, B) :-
nb_getval(prepare, false),
graph(A, _),
!,
getconj(A, C),
getterm(C, D),
conjify(D, B).
findall(C,
( member(reifiedtriple(S, P, O, _), A),
D =.. [P, S, O],
getterm(D, C)
),
E
),
conj_list(F, E),
conjify(F, B).
getterm(A, B) :-
A =.. [C|D],
getterm(D, E),
B =.. [C|E].

getconj(A, B) :-
nonvar(A),
findall(C,
( graph(A, C)
),
D
),
D \= [],
!,
conjoin(D, B).
getconj(A, A).

getstring(A, B) :-
'<http://www.w3.org/2000/10/swap/log#uri>'(A, B),
!.
Expand Down
Binary file modified eye.zip
View file
Binary file not shown.
44 changes: 25 additions & 19 deletions reasoning/acp/acp-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix : <http://example.org/#>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix list: <http://www.w3.org/2000/10/swap/list#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.

skolem:proof a r:Proof, r:Conjunction;
r:component skolem:lemma1;
Expand All @@ -25,15 +25,7 @@ skolem:lemma1 a r:Inference;
skolem:lemma5
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://example.org/#PolicyX"]];
r:rule [ a r:Fact; r:gives {@forSome var:x_0. {
var:x_0 a :Policy.
var:x_0 :pass :allOfTest.
var:x_0 :pass :anyOfTest.
var:x_0 :pass :noneOfTest.
} => {
:test :for var:x_0.
:test :is true.
}}].
r:rule skolem:lemma6.

skolem:lemma2 a r:Extraction;
r:gives {
Expand All @@ -46,7 +38,7 @@ skolem:lemma3 a r:Inference;
:PolicyX :pass :allOfTest.
};
r:evidence (
skolem:lemma6
skolem:lemma7
skolem:lemma2
[ a r:Fact; r:gives {({
:PolicyX :allOf _:sk_0.
Expand All @@ -58,14 +50,14 @@ skolem:lemma3 a r:Inference;
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://example.org/#PolicyX"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/acp/acp.n3>) 1)];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
r:rule skolem:lemma7.
r:rule skolem:lemma8.

skolem:lemma4 a r:Inference;
r:gives {
:PolicyX :pass :anyOfTest.
};
r:evidence (
skolem:lemma6
skolem:lemma7
skolem:lemma2
[ a r:Fact; r:gives {(_:sk_0 {
:PolicyX :anyOf _:sk_0.
Expand All @@ -80,14 +72,14 @@ skolem:lemma4 a r:Inference;
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo (:C)];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo 1];
r:rule skolem:lemma8.
r:rule skolem:lemma9.

skolem:lemma5 a r:Inference;
r:gives {
:PolicyX :pass :noneOfTest.
};
r:evidence (
skolem:lemma6
skolem:lemma7
skolem:lemma2
[ a r:Fact; r:gives {(_:sk_0 {
:PolicyX :noneOf _:sk_0.
Expand All @@ -102,15 +94,29 @@ skolem:lemma5 a r:Inference;
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
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_5"]; r:boundTo 0];
r:rule skolem:lemma9.
r:rule skolem:lemma10.

skolem:lemma6 a r:Extraction;
r:gives {
:test1 :policy :PolicyX.
@forAll var:x_0. {
var:x_0 a :Policy.
var:x_0 :pass :allOfTest.
var:x_0 :pass :anyOfTest.
var:x_0 :pass :noneOfTest.
} => {
:test :for var:x_0.
:test :is true.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

skolem:lemma7 a r:Extraction;
r:gives {
:test1 :policy :PolicyX.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

skolem:lemma8 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1, var:x_2, var:x_3. {
var:x_1 :pass :allOfTest.
Expand All @@ -126,7 +132,7 @@ skolem:lemma7 a r:Extraction;
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

skolem:lemma8 a r:Extraction;
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_1 :pass :anyOfTest.
Expand All @@ -143,7 +149,7 @@ skolem:lemma8 a r:Extraction;
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

skolem:lemma9 a r:Extraction;
skolem:lemma10 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_1 :pass :noneOfTest.
Expand Down
Loading

0 comments on commit 9d79eaa

Please sign in to comment.