refreshing

reasoning/sequents/README

@@ -0,0 +1,26 @@
+--------
+Sequents
+--------
+
+See https://en.wikipedia.org/wiki/Sequent
+Aka s(urface) equ(ivalent) ent(ailment)s
+
+A sequent is a log:implies with a set of possible conclusions e.g.
+
+# all cars are green or blue
+{
+    ?A a :Car.
+} => ($
+    {
+        ?A :is :green.
+    }
+    {
+        ?A :is :blue.
+    }
+$).
+
+# negation
+{
+    ?A a :Car.
+    ?A a :Horse.
+} => ($ $).

reasoning/sequents/abc.n3

@@ -0,0 +1,22 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# i element of A
+:i a :A.
+
+# not i element of C
+{
+    :i a :C.
+} => ($ $).
+
+# all A are B or C
+{
+    ?S a :A.
+} => ($
+    {
+        ?S a :B.
+    }
+    {
+        ?S a :C.
+    }
+$).

reasoning/sequents/abc.n3.out

@@ -0,0 +1,3 @@
+@prefix : <http://example.org/ns#>.
+
+:i a :B.

reasoning/sequents/abcd.n3

@@ -0,0 +1,34 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# i element of A
+:i a :A.
+
+# not i element of C
+{
+    :i a :C.
+} => ($ $).
+
+# not not not i element of D
+{
+    {
+        {
+            :i a :D.
+        } => ($ $).
+    } => ($ $).
+} => ($ $).
+
+# all A are B or C or D
+{
+    ?S a :A.
+} => ($
+    {
+        ?S a :B.
+    }
+    {
+        ?S a :C.
+    }
+    {
+        ?S a :D.
+    }
+$).

reasoning/sequents/abcd.n3.out

@@ -0,0 +1,3 @@
+@prefix : <http://example.org/ns#>.
+
+:i a :B.

reasoning/sequents/beetle.n3

@@ -0,0 +1,36 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# beetle is a car
+:beetle a :Car.
+
+# all cars are green or blue
+{
+    ?A a :Car.
+} => ($
+    {
+        ?A :is :green.
+    }
+    {
+        ?A :is :blue.
+    }
+$).
+
+# green things are beautiful
+{
+    ?A :is :green.
+} => {
+    ?A :is :beautiful.
+}.
+
+# blue things are beautiful
+{
+    ?A :is :blue.
+} => {
+    ?A :is :beautiful.
+}.
+
+# everything is not beautiful would be inconsistent
+#{
+#    ?A :is :beautiful.
+#} => ($ $).

reasoning/sequents/beetle.n3.out

@@ -0,0 +1,3 @@
+@prefix : <http://example.org/ns#>.
+
+:beetle :is :beautiful.

reasoning/sequents/beetle12.n3

@@ -0,0 +1,156 @@
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# beetle is a car
+:beetle a :Car.
+
+# all cars are green or blue
+{
+    ?A a :Car.
+} => ($
+    {
+        ?A :is :green.
+    }
+    {
+        ?A :is :blue.
+    }
+$).
+
+# green things are nice or pretty
+{
+    ?A :is :green.
+} => ($
+    {
+        ?A :is :nice.
+    }
+    {
+        ?A :is :pretty.
+    }
+$).
+
+# pretty things are pretty 1 or pretty 2
+{
+    ?A :is :pretty.
+} => ($
+    {
+        ?A :is :pretty1.
+    }
+    {
+        ?A :is :pretty2.
+    }
+$).
+
+# nice things are nice 1 or nice 2
+{
+    ?A :is :nice.
+} => ($
+    {
+        ?A :is :nice1.
+    }
+    {
+        ?A :is :nice2.
+    }
+$).
+
+# pretty 1 things are pretty 11 or pretty 12
+{
+    ?A :is :pretty1.
+} => ($
+    {
+        ?A :is :pretty11.
+    }
+    {
+        ?A :is :pretty12.
+    }
+$).
+
+# pretty 2 things are pretty 21 or pretty 22
+{
+    ?A :is :pretty2.
+} => ($
+    {
+        ?A :is :pretty21.
+    }
+    {
+        ?A :is :pretty22.
+    }
+$).
+
+# nice 1 things are nice 11 or nice 12
+{
+    ?A :is :nice1.
+} => ($
+    {
+        ?A :is :nice11.
+    }
+    {
+        ?A :is :nice12.
+    }
+$).
+
+# nice 2 things are nice 21 or nice 22
+{
+    ?A :is :nice2.
+} => ($
+    {
+        ?A :is :nice21.
+    }
+    {
+        ?A :is :nice22.
+    }
+$).
+
+# pretty or nice or blue things are beautiful
+{
+    ?A :is :pretty11.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :pretty12.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :pretty21.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :pretty22.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice11.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice12.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice21.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :nice22.
+} => {
+    ?A :is :beautiful.
+}.
+
+{
+    ?A :is :blue.
+} => {
+    ?A :is :beautiful.
+}.

reasoning/sequents/beetle12.n3.out

@@ -0,0 +1,3 @@
+@prefix : <http://example.org/ns#>.
+
+:beetle :is :beautiful.

reasoning/sequents/good-cobbler.n3

@@ -0,0 +1,42 @@
+# ------------
+# Good Cobbler
+# ------------
+#
+# Example from https://shs.hal.science/halshs-04148373/document
+# Using functional logic http://intrologic.stanford.edu/chapters/chapter_11.html
+#
+
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
+@prefix : <urn:example:>.
+
+# Some x is a good cobbler
+# (:good :Cobbler) stands for the functional term good(Cobbler)
+_:x a (:good :Cobbler).
+
+(:good :Cobbler) rdfs:subClassOf :Cobbler.
+
+# rdfs:subClassOf entailment
+{?C rdfs:subClassOf ?D. ?X a ?C} => {?X a ?D}.
+
+# invalid inference "x is good. x is a cobbler. therefore, x is a good cobbler".
+# uncommenting the following 2 triples will blow a inference fuse
+#_:x a :good.
+#_:x a :Cobbler.
+
+# maybe this is too strong in general
+{
+    ?X a ?Y.
+    ?X a ?Z.
+} => {
+    {
+        ?X a (?Y ?Z).
+    } => ($ $).
+}.
+
+# some more thinking
+# donald is a decoy duck, but it is not a duck
+
+:donald a (:decoy :duck).
+
+(:decoy :duck) rdfs:subClassOf :decoy.

reasoning/sequents/good-cobbler.n3.out

@@ -0,0 +1,3 @@
+
+_:e_x_1 a <urn:example:Cobbler>.
+<urn:example:donald> a <urn:example:decoy>.

reasoning/sequents/slide33.n3

@@ -0,0 +1,42 @@
+@prefix owl: <http://www.w3.org/2002/07/owl#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <http://example.org/ns#>.
+
+# slide 33 example from https://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk
+
+# owl restriction
+:aaa owl:onProperty :bbb.
+:aaa owl:allValuesFrom :ccc.
+
+# the following 2 triples should entail :yyy a :ccc.
+#:xxx a :aaa.
+#:xxx :bbb :yyy.
+
+# the following codex should entail :xxx a :aaa.
+{
+    :xxx :bbb ?y.
+} => {
+    ?y a :ccc.
+}.
+
+# owl:allValuseFrom description logic
+{
+    ?a owl:onProperty ?b.
+    ?a owl:allValuesFrom ?c.
+} => {
+    {
+        ?x a ?a.
+        ?x ?b ?y.
+    } => {
+        ?y a ?c.
+    }.
+    {
+        {
+            ?x ?b ?y.
+        } => {
+            ?y a ?c.
+        }.
+    } => {
+        ?x a ?a.
+    }.
+}.