From aed0f645b481e9145d15efe84d5748b508194040 Mon Sep 17 00:00:00 2001 From: josd Date: Mon, 6 Jan 2025 22:34:11 +0100 Subject: [PATCH] adding multi-agent example --- reasoning/multi-agent/README | 5 + reasoning/multi-agent/multi-agent-answer.n3 | 13 + .../multi-agent/multi-agent-explanation.n3 | 121 +++++++ reasoning/multi-agent/multi-agent-proof.n3 | 316 ++++++++++++++++++ reasoning/multi-agent/multi-agent-query.n3 | 7 + reasoning/multi-agent/multi-agent.n3 | 109 ++++++ reasoning/multi-agent/test | 4 + 7 files changed, 575 insertions(+) create mode 100644 reasoning/multi-agent/README create mode 100644 reasoning/multi-agent/multi-agent-answer.n3 create mode 100644 reasoning/multi-agent/multi-agent-explanation.n3 create mode 100644 reasoning/multi-agent/multi-agent-proof.n3 create mode 100644 reasoning/multi-agent/multi-agent-query.n3 create mode 100644 reasoning/multi-agent/multi-agent.n3 create mode 100755 reasoning/multi-agent/test diff --git a/reasoning/multi-agent/README b/reasoning/multi-agent/README new file mode 100644 index 000000000..93bbde2e0 --- /dev/null +++ b/reasoning/multi-agent/README @@ -0,0 +1,5 @@ +------------------- +Multi-agent example +------------------- + +Obligations, permissions and prohibitions depend on the roles, goals and interactions between agents. diff --git a/reasoning/multi-agent/multi-agent-answer.n3 b/reasoning/multi-agent/multi-agent-answer.n3 new file mode 100644 index 000000000..e9eb64e69 --- /dev/null +++ b/reasoning/multi-agent/multi-agent-answer.n3 @@ -0,0 +1,13 @@ +@prefix : . + +true :obligation { + :agent2 :complete_task :task1. +}. +true :permission { + :agent2 :execute_task :task1. +}. +true :obligation { + :agent1 :escalate_task :task1. +}. +true :violation :task1. +true :sanction :agent2. diff --git a/reasoning/multi-agent/multi-agent-explanation.n3 b/reasoning/multi-agent/multi-agent-explanation.n3 new file mode 100644 index 000000000..6d23fc0c3 --- /dev/null +++ b/reasoning/multi-agent/multi-agent-explanation.n3 @@ -0,0 +1,121 @@ +@prefix : . +@prefix var: . +@prefix log: . +@prefix math: . + +true :obligation { + :agent2 :complete_task :task1. +}. +true :permission { + :agent2 :execute_task :task1. +}. +true :obligation { + :agent1 :escalate_task :task1. +}. +true :violation :task1. +true :sanction :agent2. + +# +# Explain the reasoning +# + +{ + { + var:x_0 :assigned var:x_1. + } => { + true :obligation { + var:x_1 :complete_task var:x_0. + }. + }. + :task1 :assigned :agent2. +} log:explains { + true :obligation { + :agent2 :complete_task :task1. + }. +}. + +{ + { + var:x_0 :role :employee. + var:x_1 :assigned var:x_0. + } => { + true :permission { + var:x_0 :execute_task var:x_1. + }. + }. + :agent2 :role :employee. + :task1 :assigned :agent2. +} log:explains { + true :permission { + :agent2 :execute_task :task1. + }. +}. + +{ + { + var:x_0 :role :manager. + var:x_1 :assigned var:x_2. + var:x_1 :deadline var:x_3. + true :current_time var:x_4. + var:x_4 math:greaterThan var:x_3. + ({ + true :completed var:x_1. + } false true) log:ifThenElseIn var:x_5. + } => { + true :obligation { + var:x_0 :escalate_task var:x_1. + }. + }. + :agent1 :role :manager. + :task1 :assigned :agent2. + :task1 :deadline 10 . + true :current_time 15 . + 15 math:greaterThan 10 . + ({ + true :completed :task1. + } false true) log:ifThenElseIn (() 1). +} log:explains { + true :obligation { + :agent1 :escalate_task :task1. + }. +}. + +{ + { + true :obligation { + var:x_0 :complete_task var:x_1. + }. + var:x_1 :deadline var:x_2. + true :current_time var:x_3. + var:x_3 math:greaterThan var:x_2. + ({ + true :completed var:x_1. + } false true) log:ifThenElseIn var:x_4. + } => { + true :violation var:x_1. + }. + true :obligation { + :agent2 :complete_task :task1. + }. + :task1 :deadline 10 . + true :current_time 15 . + 15 math:greaterThan 10 . + ({ + true :completed :task1. + } false true) log:ifThenElseIn (() 1). +} log:explains { + true :violation :task1. +}. + +{ + { + true :violation var:x_0. + var:x_0 :assigned var:x_1. + } => { + true :sanction var:x_1. + }. + true :violation :task1. + :task1 :assigned :agent2. +} log:explains { + true :sanction :agent2. +}. diff --git a/reasoning/multi-agent/multi-agent-proof.n3 b/reasoning/multi-agent/multi-agent-proof.n3 new file mode 100644 index 000000000..08da11547 --- /dev/null +++ b/reasoning/multi-agent/multi-agent-proof.n3 @@ -0,0 +1,316 @@ +@prefix skolem: . +@prefix r: . +@prefix : . +@prefix n3: . +@prefix var: . +@prefix math: . +@prefix log: . + +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:gives { + true :obligation { + :agent2 :complete_task :task1. + }. + true :permission { + :agent2 :execute_task :task1. + }. + true :obligation { + :agent1 :escalate_task :task1. + }. + true :violation :task1. + true :sanction :agent2. + }. + +skolem:lemma1 a r:Inference; + r:gives { + true :obligation { + :agent2 :complete_task :task1. + }. + }; + r:evidence ( + skolem:lemma6 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { + :agent2 :complete_task :task1. + }]; + r:rule skolem:lemma7. + +skolem:lemma2 a r:Inference; + r:gives { + true :permission { + :agent2 :execute_task :task1. + }. + }; + r:evidence ( + skolem:lemma8 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { + :agent2 :execute_task :task1. + }]; + r:rule skolem:lemma9. + +skolem:lemma3 a r:Inference; + r:gives { + true :obligation { + :agent1 :escalate_task :task1. + }. + }; + r:evidence ( + skolem:lemma10 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo { + :agent1 :escalate_task :task1. + }]; + r:rule skolem:lemma7. + +skolem:lemma4 a r:Inference; + r:gives { + true :violation :task1. + }; + r:evidence ( + skolem:lemma11 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:task1"]]; + r:rule skolem:lemma12. + +skolem:lemma5 a r:Inference; + r:gives { + true :sanction :agent2. + }; + r:evidence ( + skolem:lemma13 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:agent2"]]; + r:rule skolem:lemma14. + +skolem:lemma6 a r:Inference; + r:gives { + true :obligation { + :agent2 :complete_task :task1. + }. + }; + r:evidence ( + skolem:lemma15 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:task1"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:agent2"]]; + r:rule skolem:lemma16. + +skolem:lemma7 a r:Extraction; + r:gives { + @forAll var:x_0. { + true :obligation var:x_0. + } => { + true :obligation var:x_0. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma8 a r:Inference; + r:gives { + true :permission { + :agent2 :execute_task :task1. + }. + }; + r:evidence ( + skolem:lemma17 + skolem:lemma15 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:agent2"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:task1"]]; + r:rule skolem:lemma18. + +skolem:lemma9 a r:Extraction; + r:gives { + @forAll var:x_0. { + true :permission var:x_0. + } => { + true :permission var:x_0. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma10 a r:Inference; + r:gives { + true :obligation { + :agent1 :escalate_task :task1. + }. + }; + r:evidence ( + skolem:lemma19 + skolem:lemma15 + skolem:lemma20 + skolem:lemma21 + [ a r:Fact; r:gives {15 math:greaterThan 10}] + [ a r:Fact; r:gives {({ + true :completed :task1. + } false true) log:ifThenElseIn (() 1)}] + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:agent1"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:task1"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "urn:example:agent2"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 10]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo 15]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo (() 1)]; + r:rule skolem:lemma22. + +skolem:lemma11 a r:Inference; + r:gives { + true :violation :task1. + }; + r:evidence ( + skolem:lemma6 + skolem:lemma20 + skolem:lemma21 + [ a r:Fact; r:gives {15 math:greaterThan 10}] + [ a r:Fact; r:gives {({ + true :completed :task1. + } false true) log:ifThenElseIn (() 1)}] + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:agent2"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:task1"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo 10]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 15]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (() 1)]; + r:rule skolem:lemma23. + +skolem:lemma12 a r:Extraction; + r:gives { + @forAll var:x_0. { + true :violation var:x_0. + } => { + true :violation var:x_0. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma13 a r:Inference; + r:gives { + true :sanction :agent2. + }; + r:evidence ( + skolem:lemma11 + skolem:lemma15 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:task1"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:agent2"]]; + r:rule skolem:lemma24. + +skolem:lemma14 a r:Extraction; + r:gives { + @forAll var:x_0. { + true :sanction var:x_0. + } => { + true :sanction var:x_0. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma15 a r:Extraction; + r:gives { + :task1 :assigned :agent2. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma16 a r:Extraction; + r:gives { + @forAll var:x_0, var:x_1. { + var:x_0 :assigned var:x_1. + } => { + true :obligation { + var:x_1 :complete_task var:x_0. + }. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma17 a r:Extraction; + r:gives { + :agent2 :role :employee. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma18 a r:Extraction; + r:gives { + @forAll var:x_0, var:x_1. { + var:x_0 :role :employee. + var:x_1 :assigned var:x_0. + } => { + true :permission { + var:x_0 :execute_task var:x_1. + }. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma19 a r:Extraction; + r:gives { + :agent1 :role :manager. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma20 a r:Extraction; + r:gives { + :task1 :deadline 10 . + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma21 a r:Extraction; + r:gives { + true :current_time 15 . + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma22 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_0 :role :manager. + var:x_1 :assigned var:x_2. + var:x_1 :deadline var:x_3. + true :current_time var:x_4. + var:x_4 math:greaterThan var:x_3. + ({ + true :completed var:x_1. + } false true) log:ifThenElseIn var:x_5. + } => { + true :obligation { + var:x_0 :escalate_task var:x_1. + }. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma23 a r:Extraction; + r:gives { + @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { + true :obligation { + var:x_0 :complete_task var:x_1. + }. + var:x_1 :deadline var:x_2. + true :current_time var:x_3. + var:x_3 math:greaterThan var:x_2. + ({ + true :completed var:x_1. + } false true) log:ifThenElseIn var:x_4. + } => { + true :violation var:x_1. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma24 a r:Extraction; + r:gives { + @forAll var:x_0, var:x_1. { + true :violation var:x_0. + var:x_0 :assigned var:x_1. + } => { + true :sanction var:x_1. + }. + }; + r:because [ a r:Parsing; r:source ]. + diff --git a/reasoning/multi-agent/multi-agent-query.n3 b/reasoning/multi-agent/multi-agent-query.n3 new file mode 100644 index 000000000..7f7471489 --- /dev/null +++ b/reasoning/multi-agent/multi-agent-query.n3 @@ -0,0 +1,7 @@ +@prefix : . + +{ true :obligation ?A } => { true :obligation ?A }. +{ true :permission ?A } => { true :permission ?A }. +{ true :prohibition ?A } => { true :prohibition ?A }. +{ true :violation ?A } => { true :violation ?A }. +{ true :sanction ?A } => { true :sanction ?A }. diff --git a/reasoning/multi-agent/multi-agent.n3 b/reasoning/multi-agent/multi-agent.n3 new file mode 100644 index 000000000..0f0a7f255 --- /dev/null +++ b/reasoning/multi-agent/multi-agent.n3 @@ -0,0 +1,109 @@ +@prefix math: . +@prefix log: . +@prefix : . + +# define agents +:agent1 a :Agent. +:agent2 a :Agent. + +# define roles +:agent1 :role :manager. +:agent2 :role :employee. + +# define tasks and deadlines +:task1 a :Task. +:task1 :deadline 10. + +# current time +true :current_time 15. + +# task assignment +:task1 :assigned :agent2. + +# task reporting +:task1 :reported :agent2. + +# obligations +{ + ?Manager :role :manager. + ?Employee :role :employee. + ?Task a ?Task. + ({ ?Task :assigned ?Employee } false true ) log:ifThenElseIn ?SCOPE. +} => { + true :obligation { ?Manager :assign_task (?Employee ?Task) }. +}. + +{ + ?Task :assigned ?Employee. + ({ ?Task :reported ?Employee } false true ) log:ifThenElseIn ?SCOPE. +} => { + true :obligation { ?Employee :report_progress ?Task }. +}. + +{ + ?Task :assigned ?Employee. +} => { + true :obligation { ?Employee :complete_task ?Task }. +}. + +{ + ?Manager :role :manager. + ?Task :assigned ?Employee. + ?Task :deadline ?Time. + true :current_time ?T. + ?T math:greaterThan ?Time. + ({ true :completed ?Task } false true ) log:ifThenElseIn ?SCOPE. +} => { + true :obligation { ?Manager :escalate_task ?Task }. +}. + +# permissions +{ + ?Employee :role :employee. + ?Task :assigned ?Employee. +} => { + true :permission { ?Employee :execute_task ?Task }. +}. + +# prohibitions +{ + ({ ?Task :assigned ?Agent } false true ) log:ifThenElseIn ?SCOPE. +} => { + true :prohibition { ?Agent :modify_task ?Task }. +}. + +# conflict detection +{ + true :obligation ?Action. + true :prohibition ?Action. +} => { + true :conflict ?Action. +}. + +# resolve conflicts with priority +{ + ?Agent :role :manager. + true :conflict ?Action. + true :obligation ?Action. +} => { + true :resolve_conflict ?Action. +}. + +# violations +{ + true :obligation { ?Employee :complete_task ?Task }. + ?Task :deadline ?Time. + true :current_time ?T. + ?T math:greaterThan ?Time. + ({ true :completed ?Task } false true ) log:ifThenElseIn ?SCOPE. +} => { + true :violation ?Task. +}. + +# sanctions +{ + true :violation ?Task. + ?Task :assigned ?Employee. +} => { + true :sanction ?Employee. +}. diff --git a/reasoning/multi-agent/test b/reasoning/multi-agent/test new file mode 100755 index 000000000..182ef16f5 --- /dev/null +++ b/reasoning/multi-agent/test @@ -0,0 +1,4 @@ +#!/bin/bash +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/multi-agent/multi-agent.n3 --query https://eyereasoner.github.io/eye/reasoning/multi-agent/multi-agent-query.n3 --output multi-agent-answer.n3 +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --explain https://eyereasoner.github.io/eye/reasoning/multi-agent/multi-agent.n3 --query https://eyereasoner.github.io/eye/reasoning/multi-agent/multi-agent-query.n3 --output multi-agent-explanation.n3 +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/multi-agent/multi-agent.n3 --query https://eyereasoner.github.io/eye/reasoning/multi-agent/multi-agent-query.n3 --output multi-agent-proof.n3