Layering LX on RDF

Status

$Revision: 1.6 $ $Date: 2002/08/22 23:06:11 $

Draft presentation of some research & software development. This version is based on e-mail sent to www-rdf-logic@w3.org, so if you've followed that here, don't expect anything new.

Background

There has been considerable disagreement about how one might use RDF's extensibility to add the features of a more expressive logic language to RDF. McDermott et al proposed a layering of first-order logic on RDF, but specified that layered sentences were being described, not asserted. Various authors have suggested that constructing a sound mechanism for asserting layered first-order logic is impossible. This research attempts to demonstrate otherwise.

Approach

  1. I view RDF as a sublanguage of FOL. I use otter's FOL syntax, and a few straightforward syntactic conventions. The N-Triples line
    _:x <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://example.com/animals#Dog> .
    translates to FOL/otter as
    exists x (rdf(x, rdf_type, '<http://example.com/animals#Dog>')).   
    RDF as a sublanguage of FOL has just conjunction, existential quantification, and a ternary predicate called "rdf". I have not established a system for handling literals yet, because it seems unneccesary for this exercise.
  2. I define another sublanguage of FOL, called LX, which is a superlanguage of RDF including the other standard logical operations (disjunction, negation, conditional, biconditional, universal quantification, and existential quantification). I have not yet included arbitrary predicates and function terms, but I see no significant problem with doing so. I also write LX with otter syntax, but of course one could use any FOL syntax easily enough.
  3. I define an RDF vocabulary (ontology) for describing LX sentences. This is similar to Drew McDermott's vocabulary for describing FOL sentences [2][3], except that I include a limitted truth predicate, allowing one to describe particular LX sentences as being true. As with wtr in KIF3, this truth predicate does not allow arbitrary nesting.
  4. To explore my understanding of this layering, I have written a set of axioms for LX-described-as-true-in-RDF. I use otter with these axioms to perform inference on reified LX; I also use otter to prove the axioms are satisfiable.

Current Results

My axioms are still flawed. After considerable effort I still have not been able to use them to produce certain more-complicated proofs involving quantification. So I cannot claim that the axioms are correct while being satisfiable, but I do think producing such axioms is very probably possible. I don't want to go that last mile unless it's really necessary.

I've been experimenting with another set of axioms, in a different style, focussing on the Liar Paradox. But, in retrospect, perhaps those axioms are far more liberal than we want: do we want two layers, or arbitrary many layers? These axioms, like KIF's wtr, try to define a decent system with arbitrary many layers. But does LX really need a truth predicate? If LX is really a sublanguage of FOL, it has no truth predicate, and we just need two layers. It may be a hard to stop after the first layer; we'll need to be clear that LX is an extension to RDF but not to RDF+LX-Layering-Axioms.

Sandro Hawke
$Id: layering.html,v 1.6 2002/08/22 23:06:11 sandro Exp $