Skip to content

Commit

Permalink
refreshing
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Mar 21, 2024
1 parent 52e8fe0 commit dd06733
Show file tree
Hide file tree
Showing 10 changed files with 323 additions and 0 deletions.
5 changes: 5 additions & 0 deletions reasoning/acp/README
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
---------------------
Access control policy
---------------------

Access control policy example
4 changes: 4 additions & 0 deletions reasoning/acp/acp-answer.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
@prefix : <http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#>.

:test :for :PolicyX.
:test :is true.
168 changes: 168 additions & 0 deletions reasoning/acp/acp-proof.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,168 @@
@prefix skolem: <http://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix : <http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.
@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;
r:gives {
:test :for :PolicyX.
:test :is true.
}.

skolem:lemma1 a r:Inference;
r:gives {
:test :for :PolicyX.
:test :is true.
};
r:evidence (
skolem:lemma2
skolem:lemma3
skolem:lemma4
skolem:lemma5
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#PolicyX"]];
r:rule skolem:lemma6.

skolem:lemma2 a r:Extraction;
r:gives {
:PolicyX a :Policy.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

skolem:lemma3 a r:Inference;
r:gives {
:PolicyX :pass :allOfTest.
};
r:evidence (
skolem:lemma7
skolem:lemma2
[ a r:Fact; r:gives {({
:PolicyX :allOf _:sk_0.
} {
:test1 :has _:sk_0.
}) log:forAllIn ((<http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>) 1)}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#test1"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#PolicyX"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((<http://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:lemma8.

skolem:lemma4 a r:Inference;
r:gives {
:PolicyX :pass :anyOfTest.
};
r:evidence (
skolem:lemma7
skolem:lemma2
[ a r:Fact; r:gives {(_:sk_0 {
:PolicyX :anyOf _:sk_0.
:test1 :has _:sk_0.
} (:C)) log:collectAllIn ((<http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>) 1)}]
[ a r:Fact; r:gives {(:C) list:length 1}]
[ a r:Fact; r:gives {1 log:notEqualTo 0}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#test1"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#PolicyX"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ((<http://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: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:lemma9.

skolem:lemma5 a r:Inference;
r:gives {
:PolicyX :pass :noneOfTest.
};
r:evidence (
skolem:lemma7
skolem:lemma2
[ a r:Fact; r:gives {(_:sk_0 {
:PolicyX :noneOf _:sk_0.
:test1 :has _:sk_0.
} ()) log:collectAllIn ((<http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>) 1)}]
[ a r:Fact; r:gives {() list:length 0}]
[ a r:Fact; r:gives {0 log:equalTo 0}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#test1"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://eyereasoner.github.io/eye/reasoning/acp/acp.n3#PolicyX"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ((<http://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: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:lemma10.

skolem:lemma6 a r:Extraction;
r:gives {
@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 <http://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 <http://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.
} <= {
var:x_0 :policy var:x_1.
var:x_1 a :Policy.
({
var:x_1 :allOf var:x_2.
} {
var:x_0 :has var:x_2.
}) log:forAllIn var:x_3.
}.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

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.
} <= {
var:x_0 :policy var:x_1.
var:x_1 a :Policy.
(var:x_2 {
var:x_1 :anyOf var:x_2.
var:x_0 :has var:x_2.
} var:x_3) log:collectAllIn var:x_4.
var:x_3 list:length var:x_5.
var:x_5 log:notEqualTo 0.
}.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

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.
} <= {
var:x_0 :policy var:x_1.
var:x_1 a :Policy.
(var:x_2 {
var:x_1 :noneOf var:x_2.
var:x_0 :has var:x_2.
} var:x_3) log:collectAllIn var:x_4.
var:x_3 list:length var:x_5.
var:x_5 log:equalTo 0.
}.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/acp/acp.n3>].

56 changes: 56 additions & 0 deletions reasoning/acp/acp.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
# -----------------------------
# Access control policy example
# -----------------------------

@prefix list: <http://www.w3.org/2000/10/swap/list#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <#>.

:test1 :policy :PolicyX;
:has :A, :B, :C.

:PolicyX a :Policy;
:allOf :A, :B;
:anyOf :C;
:noneOf :D.

{
?Pol :pass :allOfTest.
} <= {
?Test :policy ?Pol.
?Pol a :Policy.
({?Pol :allOf ?Field} {?Test :has ?Field}) log:forAllIn ?X.
}.

{
?Pol :pass :anyOfTest.
} <= {
?Test :policy ?Pol.
?Pol a :Policy.
(?Field {?Pol :anyOf ?Field. ?Test :has ?Field} ?List) log:collectAllIn ?X.
?List list:length ?L.
?L log:notEqualTo 0.
}.

{
?Pol :pass :noneOfTest.
} <= {
?Test :policy ?Pol.
?Pol a :Policy.
(?Field {?Pol :noneOf ?Field. ?Test :has ?Field} ?List) log:collectAllIn ?X.
?List list:length ?L.
?L log:equalTo 0.
}.

# query
_:ng11 log:query _:ng12.

{
?Pol a :Policy.
?Pol :pass :allOfTest.
?Pol :pass :anyOfTest.
?Pol :pass :noneOfTest.
} log:query {
:test :for ?Pol.
:test :is true.
}.
3 changes: 3 additions & 0 deletions reasoning/acp/test
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
#!/bin/bash -x
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache http://eyereasoner.github.io/eye/reasoning .. --nope http://eyereasoner.github.io/eye/reasoning/acp/acp.n3 --output acp-answer.n3
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache http://eyereasoner.github.io/eye/reasoning .. http://eyereasoner.github.io/eye/reasoning/acp/acp.n3 --output acp-proof.n3
5 changes: 5 additions & 0 deletions reasoning/backward/README
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
---------------------
Backward rule example
---------------------

See https://www.w3.org/2000/10/swap/doc/tutorial-1.pdf page 17
3 changes: 3 additions & 0 deletions reasoning/backward/backward-answer.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
@prefix : <http://eyereasoner.github.io/eye/reasoning/backward/backward.n3#>.

5 :moreInterestingThan 3 .
53 changes: 53 additions & 0 deletions reasoning/backward/backward-proof.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
@prefix skolem: <http://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix : <http://eyereasoner.github.io/eye/reasoning/backward/backward.n3#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@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 {
5 :moreInterestingThan 3 .
}.

skolem:lemma1 a r:Inference;
r:gives {
5 :moreInterestingThan 3 .
};
r:evidence (
skolem:lemma2
);
r:rule skolem:lemma3.

skolem:lemma2 a r:Inference;
r:gives {
5 :moreInterestingThan 3 .
};
r:evidence (
[ a r:Fact; r:gives {5 math:greaterThan 3}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo 5];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 3];
r:rule skolem:lemma4.

skolem:lemma3 a r:Extraction;
r:gives {
{
5 :moreInterestingThan 3.
} => {
5 :moreInterestingThan 3.
}.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/backward/backward.n3>].

skolem:lemma4 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {
var:x_0 :moreInterestingThan var:x_1.
} <= {
var:x_0 math:greaterThan var:x_1.
}.
};
r:because [ a r:Parsing; r:source <http://eyereasoner.github.io/eye/reasoning/backward/backward.n3>].

23 changes: 23 additions & 0 deletions reasoning/backward/backward.n3
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
# ---------------------
# Backward rule example
# ---------------------
#
# See https://www.w3.org/2000/10/swap/doc/tutorial-1.pdf page 17

@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <#>.

# something is more interesting if it is greater
{
?X :moreInterestingThan ?Y.
} <= {
?X math:greaterThan ?Y.
}.

# query
{
5 :moreInterestingThan 3.
} log:query {
5 :moreInterestingThan 3.
}.
3 changes: 3 additions & 0 deletions reasoning/backward/test
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
#!/bin/bash -x
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache http://eyereasoner.github.io/eye/reasoning .. --nope http://eyereasoner.github.io/eye/reasoning/backward/backward.n3 --output backward-answer.n3
eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache http://eyereasoner.github.io/eye/reasoning .. http://eyereasoner.github.io/eye/reasoning/backward/backward.n3 --output backward-proof.n3

0 comments on commit dd06733

Please sign in to comment.