RDF ⇌ BiRel: Coherent Logic and Skolem Machines
The web site skolemmachines.org describes how to build a Turing Machine equivalent called a Skolem Machine that functions on Coherent Logic, the Logic that the article Knowledge Representation in Bicategories of Relations states is the internal language of distributive bicategories of relations. The web site comes with a Java Applet, and an 2009 article Skolem Machines by John Fischer and Marc Bezem.
This article is cited in the 2015 paper Geometrisation of first-order logic by Roy Dyckhoff and Sara Negri, an article that goes over a very long list of more or less formal proofs from Skolem onward that Coherent logic is equivalent in power to first order logic.
So this raises a number of basic questions:
- which parts of RDF/OWL are in the coherent logic space (ie. requiring disjunction and negation)?
- Euler Sharp, an implementation of an N3 reasoner used a coherent inference engine at one point. This required the Agfa team to implement disjunctions in a slightly inelegant way, as explained by Jos de Roo in a mail to the Semantic Web mailing List on January 18 2020. How close is N3 to coherent logic?
- Skolem Machines rules are formed of sequents A1, A2, A3, ... ⊢ C1 | C2 | C3 | ... where An's are conjunctions of atomic statements and the consequent are disjunctions of conjunctions of atomic statements. Can one recognise that structure in the bicategories of relations?
- The W3C had a project on RDF rules interchange format (RIF). Did they have something to say on this?
It seems that Sara Negri and Roy Dickhoff got interested in Geometric Logic for its application to modal logic as it allowed them "to capture logics with arbitrary first-order conditions on their Kripke frames. (see Non-normal modal logics:a challenge to proof theory). Coherent logic is plays an import role in a recent 2019 PhD thesis Bunched logics: a uniform approach in relation to modal logic and tableau calculi.
A far-out question: in a 2016 article Wittgenstein’s Struggles with the Quantifiers Jan Van Plato (who has coauthored articles with Sara Negri) has argued that Wittgenstein had trouble with universal quantification, which is exactly the quantifier missing in Coherent Logic. Was Wittgentstein a Coherent Logician?
Of Note: Thierry Coquand (of Coq fame) wrote an article in 2006 Automating Coherent Logic arguing that it "is well-suited for providing automated reasoning support to logical framework".