refreshing

eyereasoner · Dec 4, 2024 · 0a1d5a4 · 0a1d5a4
1 parent 2ab9392
commit 0a1d5a4
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 0 deletions.
diff --git a/reasoning/deontic/example1-answer.n3s b/reasoning/deontic/example1-answer.n3s
@@ -8,4 +8,7 @@
 :p :isObligatoryIn :w1.
 :p :isObligatoryIn :w2.
 :p :isObligatoryIn :w3.
+:r :isObligatoryIn :w1.
+:r :isObligatoryIn :w2.
+:r :isObligatoryIn :w3.
 :q :isForbiddenIn :w3.
diff --git a/reasoning/deontic/example1-proof.n3s b/reasoning/deontic/example1-proof.n3s
@@ -14,6 +14,9 @@ skolem:proof a r:Proof, r:Conjunction;
     r:component skolem:lemma7;
     r:component skolem:lemma8;
     r:component skolem:lemma9;
+    r:component skolem:lemma10;
+    r:component skolem:lemma11;
+    r:component skolem:lemma12;
     r:gives {
         :p :isPermittedIn :w1.
         :q :isPermittedIn :w1.
@@ -23,6 +26,9 @@ skolem:proof a r:Proof, r:Conjunction;
         :p :isObligatoryIn :w1.
         :p :isObligatoryIn :w2.
         :p :isObligatoryIn :w3.
+        :r :isObligatoryIn :w1.
+        :r :isObligatoryIn :w2.
+        :r :isObligatoryIn :w3.
         :q :isForbiddenIn :w3.
     }.
 
@@ -147,6 +153,51 @@ skolem:lemma8 a r:Inference;
     }}].
 
 skolem:lemma9 a r:Inference;
+    r:gives {
+        :r :isObligatoryIn :w1.
+    };
+    r:evidence (
+        [ a r:Fact; r:gives {:r :isObligatoryIn :w1}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:r"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:w1"]];
+    r:rule [ a r:Fact; r:gives {@forSome var:x_0, var:x_1. {
+        var:x_0 :isObligatoryIn var:x_1.
+    } => {
+        var:x_0 :isObligatoryIn var:x_1.
+    }}].
+
+skolem:lemma10 a r:Inference;
+    r:gives {
+        :r :isObligatoryIn :w2.
+    };
+    r:evidence (
+        [ a r:Fact; r:gives {:r :isObligatoryIn :w2}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:r"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:w2"]];
+    r:rule [ a r:Fact; r:gives {@forSome var:x_0, var:x_1. {
+        var:x_0 :isObligatoryIn var:x_1.
+    } => {
+        var:x_0 :isObligatoryIn var:x_1.
+    }}].
+
+skolem:lemma11 a r:Inference;
+    r:gives {
+        :r :isObligatoryIn :w3.
+    };
+    r:evidence (
+        [ a r:Fact; r:gives {:r :isObligatoryIn :w3}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "urn:example:r"]];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "urn:example:w3"]];
+    r:rule [ a r:Fact; r:gives {@forSome var:x_0, var:x_1. {
+        var:x_0 :isObligatoryIn var:x_1.
+    } => {
+        var:x_0 :isObligatoryIn var:x_1.
+    }}].
+
+skolem:lemma12 a r:Inference;
     r:gives {
         :q :isForbiddenIn :w3.
     };

diff --git a/reasoning/deontic/example1.n3s b/reasoning/deontic/example1.n3s
@@ -21,6 +21,9 @@
 :q :isTrueIn :w2.
 :p :isTrueIn :w3.
 
+# proposition implications
+:p :implies :r.
+
 # declare components
 :isObligatoryIn a log:Component.
 :isPermittedIn a log:Component.
@@ -96,6 +99,15 @@
     ) log:collectAllIn _:Scope.
 }.
 
+# K axiom
+(_:Proposition1 _:Proposition2 _:World) log:onNegativeSurface {
+    () log:onNegativeSurface {
+        _:Proposition2 :isObligatoryIn _:World.
+    }.
+    _:Proposition1 :implies _:Proposition2.
+    _:Proposition1 :isObligatoryIn _:World.
+}.
+
 # query
 (_:Proposition _:World) log:onNegativeSurface {
     _:Proposition :isObligatoryIn _:World.