- From: Patrick J Hayes <phayes@ihmc.us>
- Date: Mon, 20 Jan 2020 14:14:47 -0600
- To: Antoine Zimmermann <antoine.zimmermann@emse.fr>
- CC: Henry Story <henry.story@bblfish.net>, Jos De Roo <jos.deroo@agfa.com>, semantic-web <semantic-web@w3.org>
- Message-ID: <B989AADF-34FB-4D1A-BDB1-D6877FACAEE8@ihmc.us>
> On Jan 20, 2020, at 5:26 AM, Antoine Zimmermann <antoine.zimmermann@emse.fr> wrote: > > RDF is only first order logic insofar as it can be translated into FOL while preserving entailments. That is, there exists a translation T from RDF graphs to FOL formulas such that: > > G1 RDF-entails G2 if and only if T(G1) FOL-entails T(G2) Correct, although (with qualification, see below) the actual model theory of RDF can be seen as a simplification of FOL model theory, giving a more directly semantic relationship. > > But this is a rather strong simplication, because RDF is not *a* logic, but *a family* of logics. RDF 1.1 Semantics defines simple entailment, D-entailment, RDF-entailment (recognising D), RDFS-entailment (recognising D), where D can be any set of datatype IRIs. True. I was referring to the basic RDF which supports simple entailment. RDFS entailment without datatypes is a (similarly restricted) FOL axiomatic theory. But as you say, datatype reasoning is whole other matter. > > Simple entailment can be translated to FOL using either: relations of arity 2 (where the predicate IRI is used as a binary FOL predicate); or using a single relation of arity 3 (where <s> <p> <o> becomes Triple(s,p,o)). > > If you assume the set D to be empty, then RDF-entailment and RDFS-entailment can be translated to FOL as well. But as soon as you add datatypes and literals to the picture, it's a whole different story. RDF 1.1 Semantics imposes that RDF(S)-entailment MUST recognise xsd:string and rdf:langString. This totally cripples the RDF-to-FOL translation. Well, as with RDFS, it maps into a FO axiomatic theory (in this case, countably infinite) but the actual reasoning is still simple FO reasoning. It does not require a different /logic/. Pat > > For instance, in RDFS-entailment recognising {xsd:string,rdf:langString}, is the following graph consistent (written in Turtle, assuming the obvious prefixes)? > > rdfs:Resource rdfs:subClassOf xsd:string . > > (left as an exercise to the reader :) :-) I am not sure myself. If a language-tagged string a kind of string? > > Datatype semantics in RDF is horribly complicated to properly handle and I doubt there is (and even will be) any reasoner that correctly and completely implements datatype entailment as defined in the standard. Notably, in his excellent paper from 2005, Herman J. ter Horst provides a sound and complete algorithm for RDFS with datatype entailment, but he dismisses the official D-entailment semantics to propose a more computable one, that he calls D*-entailment [1]. D*-entailment is what practical reasoners usually implement, if they support datatypes at all. > > However, De Bruijn and Heymans show that, if we are cautious in selecting supported datatypes, it is still theoretically possible to reason efficiently with standard D-entailment [2]. But first, they do not provide an effective algorithm,* and second, it forbids quite a lot of datatype combinations. > > > * Only indirectly via translation to F-Logic, and it may not be efficient at all. > > > --AZ > > > > [1] Herman J. ter Horst. Completeness, decidability and complexity of entailment for RDF Schema and a semantic extension involving the OWL vocabulary. In Journal of Web Semantics, Volume 3, Issues 2–3, October 2005, pages 79-115. > [2] Jos De Bruijn and Stijn Heymans. Logical Foundations of RDF(S) with Datatypes. In Journal of Artificial Intelligence Research, Volume 38, August 2010, pages 535-568. > > Le 19/01/2020 à 06:06, Patrick J Hayes a écrit : > > [skip] > >>> >>> 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.) 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 >>> >>> > > -- > Antoine Zimmermann > Institut Henri Fayol > École des Mines de Saint-Étienne > 158 cours Fauriel > CS 62362 > 42023 Saint-Étienne Cedex 2 > France > Tél:+33(0)4 77 42 66 03 > Fax:+33(0)4 77 42 66 66 > http://www.emse.fr/~zimmermann/ <http://www.emse.fr/~zimmermann/> > Member of team Connected Intelligence, Laboratoire Hubert Curien
Received on Monday, 20 January 2020 20:15:03 UTC