- From: Henry Story <henry.story@bblfish.net>
- Date: Wed, 22 Jan 2020 15:22:21 +0100
- To: Patrick Hayes <phayes@ihmc.us>
- Cc: Jos De Roo <jos.deroo@agfa.com>, semantic-web <semantic-web@w3.org>
> On 19 Jan 2020, at 06:06, Patrick J Hayes <phayes@ihmc.us> wrote: > > > >> On Jan 18, 2020, at 3:02 PM, Henry Story <henry.story@bblfish.net> wrote: >> >> Thanks for your very helpful answer Jos, >> >> Thinking about these I developed some further questions below, >> which perhaps the larger community here may have thoughts on. >> >>> On 18 Jan 2020, at 13:11, Jos De Roo <jos.deroo@agfa.com> wrote: >>> >>> Hi Henri, >>> >>> Here's my feedback in a nutshell. >>> >>> Coherent logic formulae were expressed in N3 and used an ugly way to >>> express disjunction in the conclusion of log:implies. It would have >>> been nice to use use a '|' to separate the conclusions but that would >>> have required an extension of N3 which was not feasable. For an example >>> see the Pappus Desargues Hessenberg [1] test case at [2], [3], [4] and [5]. >> >> So that fits well Patterson’s thesis that one gets coherent logic by adding >> the structures for disjunction and false (aka coproducts and bottom) to regular logic - the internal logic of bicategories of relations. >> Adding disjunction and bottom giving us distributive relational ologs. >> >> It seems you found coherent logic important just at the point at which >> you needed disjunction. >> >>> In EYE we impemented a so called "branch engine" on top of the original >>> "trunk engine". The former engine is like a Skolem Machine [6] whereas >>> the latter is a forward backward chainer (backward chaining for rules >>> using <= in N3 and forward chaining for rules using => in N3). >> >> Thanks for the link to the Skolem machines web site. The paper with the >> same name published there which explains Skolem machines as a variation >> of Turing machines, is easy to read, and also fits very nicely with the >> picture from the bicategories of relations. >> >> Btw. I found an article from 2015 that gives a very complete overview >> of coherent logic and all the different proofs of its equivalence to >> first order logic from Skolem’s work in the 1920s onwards that is >> a great follow up on the Skolem machines article which is also covered. >> >> Roy Dyckhoff and Sara Negri "Geometrisation Of First-Order Logic" >> https://twitter.com/bblfish/status/1218559825476562945 >> >> The researchers interestingly write this yo because of an interest >> in modal logic. >> >> ( The importance of its relation to modal logic seems >> to be taken up by a 2019 PhD thesis >> ”Bunched Logics: A Uniform Approach” >> https://twitter.com/bblfish/status/1215024256985247745 >> ) >> >>> >>> Althoug we came up with challenging use cases in the building construction >>> domain and in the healtcare and life science domain we were not seeing >>> that is was used. It is not good to maintain an engine that is not used >>> hence we removed the branch engine some years ago. >> >> Do you have descriptions of the challenges you were able to address by >> having regular logic? >> >> If Patterson gives a good model of RDF it would follow that RDF is a regular logic, since it does not have disjunction. Is that correct? >> >> If so are there advantages for RDF, as a linked data format to be >> a regular logic rather than a coherent one? Disadvantages? >> >> Henry >> >> PS. I think I remember Pat Hayes claiming RDF was a first order logic >> on this list a year or so ago… (that would I presume not fit it being >> a regular logic,… But I am not an expert in this (yet). > > RDF is a (very minimal) fragment of FOL. Technically it is binary (relations of arity 1 or 2) FOL restricted to conjunction and the existential quantifier. No negation, disjunction or universal quantifier. It also lacks any scoping mechanism, but this does not matter when there is no negation, disjunction or universal quantification. One would get full FOL by adding negation and a scoping mechanism (such as an explicit existential quantifier, although other syntaxes could be used.) yes, so that is why it looks so close to regular logic as far as I understand. Patterson writes: > Regular logic is the fragment of first order logic generated by =, ⊤, ∧, and ∃. Paterson in Appendix A gives a definition of Regular Logic and one can also find on p11 of "Regular Categories and Regular Logic” from 1998 https://www.brics.dk/LS/98/2/BRICS-LS-98-2.pdf a simple and detailed definition in 8 lines. The last states: > Regular logic is roughly speaking the ∃–∧–fragment of many-sorted first- order logic. The main obvious difference is that it is many sorted. Perhaps one would then think of RDF or OWL as a one or two sorted regular logic (resources and literals)? (I think one also needs ⊤, a type with one element). The logic can then be mapped one 1-1 to a bicategory of relations - a category with arrows between arrows, which allows one to draw diagrams and equate relations. Functorial Semantics works by representing a schema as a small category. One then maps that into a category of instances, which for our purposes is the category of sets and relations. (I’ll ignore this difference to RDF here). Taking the Grothendieck construction of that Functor gives one a new Category that is equivalent a flattened structure (actually a category) just like an RDF graph, and that can be mapped back to the original schema. Relations pick out subsets of RxR (in our single sorted version). Because it is a bicategory there are relations between relations, these arrows map to relations that are subsets of other relations, which gives us entailment ⊢. It could also explains how relations can be in subject position in RDF. There is a generalized notion of truth ⊤, which is the full relation between two types, which makes sense for entailment. If we have the one element type I, then ⊤ between IxI is the top relation of the booleans, (false would then be the empty relation). ∧: conjunction I think in RDF is related to joining triples into a graph. In the bicategory space it is represented by parallel arrows, so independent relations (individually independent, but potentially part of a larger connected graph). Connected concepts allow one to form equations between relations such that a grandparent is the same as the parent of a parent. = I think equality comes out of category theory, as every type needs to have its own identity relation. So it looks like regular logic comes with owl:sameAs . ∃ Introducing an existential quantifier moves a relation R: A → B to a relation R’: A → I where I is the one element set. Relations to the one element set are equivalent to the definition of a concept in DL. And I guess it is actually what is happening here: https://www.w3.org/TR/owl2-syntax/#Existential_Quantification Adding the dual ⋁ (or) and ⊥ (false) requires a distributive bicategory of relations, which gives one coherent logic which is equivalent in expressiveness to first order logic. Those are needed for some OWL concepts I was told. Henry > For details, see https://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk starting on slide 20. > > Now, it should also be said that RDF is a slightly nonstandard FOL since it allows the same name to occur in both individual and relation position, which feels ‘higher order’. However, the semantics of RDF is strictly first order. This issue has been explored to death in the literature on, among other things, ISO Common Logic. > > Pat > > > PS. Hi Jos! > >> >>> >>> Kind regards, >>> Jos >>> >>> [1] https://en.wikipedia.org/wiki/Desargues%27s_theorem#Relation_to_Pappus's_theorem >>> [2] https://github.com/w3c/N3/blob/master/grammar/tests/N3Tests/07test/pd_hes_theory.n3 >>> [3] https://github.com/w3c/N3/blob/master/grammar/tests/N3Tests/07test/pd_hes_tactic.n3 >>> [4] https://github.com/w3c/N3/blob/master/grammar/tests/N3Tests/07test/pd_hes_query.n3 >>> [5] https://github.com/w3c/N3/blob/master/grammar/tests/N3Tests/07test/pd_hes_result.n3 >>> [6] https://skolemmachines.org/ >>> >>> >>> Jos De Roo | Agfa HealthCare >>> Data Scientist | HE/Clinical Analytics >>> http://josd.github.io/ >>> >>> Agfa HealthCare NV, Moutstraat 100, B-9000 Gent, Belgium >>> http://www.agfa.com/healthcare >>> From: Henry Story <henry.story@bblfish.net> >>> Sent: 18 January 2020 00:51 >>> To: semantic-web <semantic-web@w3.org> >>> Subject: Coherent Logic (a.k.a Geometric Logic) and RDF? >>> >>> Hi, >>> >>> I came across Coherent Logic recently. Apparently it is >>> as expressive as First Order Logic. And I found that it was used >>> by Jos De Roo’s EYE implementation of an N3 reasoner. [1] >>> I was wondering what the feedback of its use was in the field, and >>> return on experience on how it fit into the Semantic Web stack. >>> >>> I came across it by reading an excellent 2017 paper by >>> Evan Patterson [2] >>> "Knowledge Representation in Bicategories of Relations” >>> >>> Where David Spivak (MIT) has put together some very elegant >>> work showing how Category Theory could be applied to Databases, >>> and in a number of articles tying these to RDF and SPARQL, the >>> problem has been that his Database instances are functors from >>> a small Category playing the role of a Schema into the Category Set, >>> where objects are Sets and morphisms are functions. This does >>> not fit well with RDF as many relations such as foaf:knows >>> are not functional. >>> >>> By adapting this functorial semantics and instead of using >>> normal Categories for Schemas, Patterson uses Bicategories of relations >>> which can have morphisms between morphisms (giving us >>> inference). Then when representing DB instances as functors >>> into the Category Rel, where objects are Sets and morphisms >>> are relations, we get much closer to RDF. >>> Indeed Patterson starts off his discussion with Description Logics. >>> >>> (Note by the way that both Spivak and Patterson, point to a >>> fundamental concept in Category Theory known as the Grothendieck >>> construction that takes a tabular database and turns it into >>> the flattened structure of RDF, this itself being essential in >>> analyses of SQL or SPARQL Queries) >>> >>> Now the first part of the paper shows that ”regular logic is the >>> internal language of bicategories of relations”. The final >>> section shows that ”distributive relational ontology logics (ologs)” >>> correspond to Coherent Logic. >>> >>> This way of putting things gives a special place to ”regular >>> logic” and ”coherent logic”. So I searched around and found >>> the latter used by Jos de Roo’s N3 reasoner EYE, which seems >>> to somewhat confirm Patterson’s modeling of RDF. >>> >>> >>> Henry Story >>> >>> [1] See Twitter thread https://twitter.com/bblfish/status/1215024256985247745 >>> [2] https://www.epatters.org/assets/papers/2017-relational-ologs.pdf >> >> >
Received on Wednesday, 22 January 2020 14:22:29 UTC