Re: is rdf a regular logic? RIF? was: Coherent Logic (a.k.a Geometric Logic) and RDF?

> 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.) For details, see https://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk <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
> 
>