Skip to content

Commit

Permalink
refreshing
Browse files Browse the repository at this point in the history
  • Loading branch information
@josd
josd committed Nov 13, 2024
1 parent 376a5e3 commit 1a6ad8d
Show file tree
Hide file tree
Showing 4 changed files with 72 additions and 128 deletions.
9 changes: 3 additions & 6 deletions color/deontic/workplace-answer.n3
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
@prefix : <urn:example:>.

:alice :does :log_off_at_end_of_shift.
:alice :is_fulfilling_an_obligation :log_off_at_end_of_shift.
:bob :does :work_related_task.
:bob :is_doing_a_permitted_action :work_related_task.
:carol :does :access_social_media.
:carol :is_violating_a_prohibition :access_social_media.
:alice :complies (true :is_fulfilling_an_obligation :log_off_at_end_of_shift).
:bob :complies (true :is_doing_a_permitted_action :work_related_task).
:carol :complies (false :is_violating_a_prohibition :access_social_media).
180 changes: 64 additions & 116 deletions color/deontic/workplace-proof.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,208 +8,156 @@ skolem:proof a r:Proof, r:Conjunction;
r:component skolem:lemma1;
r:component skolem:lemma2;
r:component skolem:lemma3;
r:component skolem:lemma4;
r:component skolem:lemma5;
r:component skolem:lemma6;
r:gives {
:alice :does :log_off_at_end_of_shift.
:alice :is_fulfilling_an_obligation :log_off_at_end_of_shift.
:bob :does :work_related_task.
:bob :is_doing_a_permitted_action :work_related_task.
:carol :does :access_social_media.
:carol :is_violating_a_prohibition :access_social_media.
:alice :complies (true :is_fulfilling_an_obligation :log_off_at_end_of_shift).
:bob :complies (true :is_doing_a_permitted_action :work_related_task).
:carol :complies (false :is_violating_a_prohibition :access_social_media).
}.

skolem:lemma1 a r:Inference;
r:gives {
:alice :does :log_off_at_end_of_shift.
:alice :complies (true :is_fulfilling_an_obligation :log_off_at_end_of_shift).
};
r:evidence (
skolem:lemma7
skolem:lemma7
skolem:lemma4
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:alice"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:log_off_at_end_of_shift"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:does"]];
r:rule skolem:lemma8.
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo (true :is_fulfilling_an_obligation :log_off_at_end_of_shift)];
r:rule skolem:lemma5.

skolem:lemma2 a r:Inference;
r:gives {
:alice :is_fulfilling_an_obligation :log_off_at_end_of_shift.
};
r:evidence (
skolem:lemma7
skolem:lemma9
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:alice"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:log_off_at_end_of_shift"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:is_fulfilling_an_obligation"]];
r:rule skolem:lemma8.

skolem:lemma3 a r:Inference;
r:gives {
:bob :does :work_related_task.
};
r:evidence (
skolem:lemma10
skolem:lemma10
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:bob"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:work_related_task"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:does"]];
r:rule skolem:lemma8.

skolem:lemma4 a r:Inference;
r:gives {
:bob :is_doing_a_permitted_action :work_related_task.
:bob :complies (true :is_doing_a_permitted_action :work_related_task).
};
r:evidence (
skolem:lemma10
skolem:lemma11
skolem:lemma6
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:bob"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:work_related_task"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:is_doing_a_permitted_action"]];
r:rule skolem:lemma8.
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo (true :is_doing_a_permitted_action :work_related_task)];
r:rule skolem:lemma5.

skolem:lemma5 a r:Inference;
skolem:lemma3 a r:Inference;
r:gives {
:carol :does :access_social_media.
:carol :complies (false :is_violating_a_prohibition :access_social_media).
};
r:evidence (
skolem:lemma12
skolem:lemma12
skolem:lemma7
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:carol"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:access_social_media"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:does"]];
r:rule skolem:lemma8.
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo (false :is_violating_a_prohibition :access_social_media)];
r:rule skolem:lemma5.

skolem:lemma6 a r:Inference;
skolem:lemma4 a r:Inference;
r:gives {
:carol :is_violating_a_prohibition :access_social_media.
:alice :complies (true :is_fulfilling_an_obligation :log_off_at_end_of_shift).
};
r:evidence (
skolem:lemma12
skolem:lemma13
skolem:lemma8
skolem:lemma9
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:carol"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:access_social_media"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:is_violating_a_prohibition"]];
r:rule skolem:lemma8.

skolem:lemma7 a r:Extraction;
r:gives {
:alice :does :log_off_at_end_of_shift.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:alice"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:log_off_at_end_of_shift"]];
r:rule skolem:lemma10.

skolem:lemma8 a r:Extraction;
skolem:lemma5 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1, var:x_2. {
var:x_0 :does var:x_1.
var:x_0 var:x_2 var:x_1.
@forAll var:x_0, var:x_1. {
var:x_0 :complies var:x_1.
} => {
var:x_0 var:x_2 var:x_1.
var:x_0 :complies var:x_1.
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace-query.n3>].

skolem:lemma9 a r:Inference;
r:gives {
:alice :is_fulfilling_an_obligation :log_off_at_end_of_shift.
};
r:evidence (
skolem:lemma7
skolem:lemma14
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:alice"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:log_off_at_end_of_shift"]];
r:rule skolem:lemma15.

skolem:lemma10 a r:Extraction;
r:gives {
:bob :does :work_related_task.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma11 a r:Inference;
skolem:lemma6 a r:Inference;
r:gives {
:bob :is_doing_a_permitted_action :work_related_task.
:bob :complies (true :is_doing_a_permitted_action :work_related_task).
};
r:evidence (
skolem:lemma10
skolem:lemma16
skolem:lemma11
skolem:lemma12
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:bob"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:work_related_task"]];
r:rule skolem:lemma17.

skolem:lemma12 a r:Extraction;
r:gives {
:carol :does :access_social_media.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].
r:rule skolem:lemma13.

skolem:lemma13 a r:Inference;
skolem:lemma7 a r:Inference;
r:gives {
:carol :is_violating_a_prohibition :access_social_media.
:carol :complies (false :is_violating_a_prohibition :access_social_media).
};
r:evidence (
skolem:lemma12
skolem:lemma18
skolem:lemma14
skolem:lemma15
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:carol"]];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:access_social_media"]];
r:rule skolem:lemma19.
r:rule skolem:lemma16.

skolem:lemma14 a r:Extraction;
skolem:lemma8 a r:Extraction;
r:gives {
:alice :does :log_off_at_end_of_shift.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma9 a r:Extraction;
r:gives {
:workplace_policy :obliged :log_off_at_end_of_shift.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma15 a r:Extraction;
skolem:lemma10 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {
var:x_0 :does var:x_1.
:workplace_policy :obliged var:x_1.
} => {
var:x_0 :is_fulfilling_an_obligation var:x_1.
var:x_0 :complies (true :is_fulfilling_an_obligation var:x_1).
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma16 a r:Extraction;
skolem:lemma11 a r:Extraction;
r:gives {
:bob :does :work_related_task.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma12 a r:Extraction;
r:gives {
:workplace_policy :permitted :work_related_task.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma17 a r:Extraction;
skolem:lemma13 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {
var:x_0 :does var:x_1.
:workplace_policy :permitted var:x_1.
} => {
var:x_0 :is_doing_a_permitted_action var:x_1.
var:x_0 :complies (true :is_doing_a_permitted_action var:x_1).
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma18 a r:Extraction;
skolem:lemma14 a r:Extraction;
r:gives {
:carol :does :access_social_media.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma15 a r:Extraction;
r:gives {
:workplace_policy :forbidden :access_social_media.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].

skolem:lemma19 a r:Extraction;
skolem:lemma16 a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {
var:x_0 :does var:x_1.
:workplace_policy :forbidden var:x_1.
} => {
var:x_0 :is_violating_a_prohibition var:x_1.
var:x_0 :complies (false :is_violating_a_prohibition var:x_1).
}.
};
r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/deontic/workplace.n3>].
Expand Down
5 changes: 2 additions & 3 deletions color/deontic/workplace-query.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@

# Query to test if everyone complies with deontic logic
{
?Person :does ?Action.
?Person ?P ?Action.
?Person :complies ?Check.
} => {
?Person ?P ?Action.
?Person :complies ?Check.
}.
6 changes: 3 additions & 3 deletions color/deontic/workplace.n3
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,19 +15,19 @@
?Person :does ?Action.
:workplace_policy :obliged ?Action
} => {
?Person :is_fulfilling_an_obligation ?Action.
?Person :complies (true :is_fulfilling_an_obligation ?Action).
}.

{
?Person :does ?Action.
:workplace_policy :permitted ?Action
} => {
?Person :is_doing_a_permitted_action ?Action.
?Person :complies (true :is_doing_a_permitted_action ?Action).
}.

{
?Person :does ?Action.
:workplace_policy :forbidden ?Action
} => {
?Person :is_violating_a_prohibition ?Action.
?Person :complies (false :is_violating_a_prohibition ?Action).
}.

0 comments on commit 1a6ad8d

Please sign in to comment.