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

-- https://josd.github.io/ <http://josd.github.io/>


On Sun, Jan 19, 2020 at 6:15 AM 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
>
> Thanks for the pointer.

>
>
> 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?
>
> The challenging use cases were:

- assisting building architects in the creative process of making
  design choices
- assisting healthcare givers in making choices for clinical
  treatment paths
- assisting clinical trial designers in making choices for
  eligibility criteria

To implement those use cases we used MONADIC [1] and RESTdesc [2]:

Discovery --> Specification --> Execution --> Evaluation --> Report
    ^            ^    ^                         |    |         |
    |            |    |                         |    |         |
    |            |    '-------------------------'    |         |
    |            |                                   |         v
instructions  knowledge <----------------------------'       answer

Discovery + Specification = Abduction
Execution + Inference = Deduction
Evaluation + Report = Induction

[1] https://lists.w3.org/Archives/Public/www-archive/2010Nov/0004.html
[2] https://ruben.verborgh.org/publications/verborgh_phd_2014/


>
> 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 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.
>
> Nobody could have said it better :-)


> Pat
>
>
> PS. Hi Jos!
>

 Hi Pat!
 I really miss the exciting discussions at the W3C face to face meetings
 but they rewired my brain and so I still benefit from them ;-)
>
>
>
>
> 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
>
>
>
>
>