$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 email@example.com, so if you've followed that here, don't expect anything new.
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.
_: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.
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.
$Id: layering.html,v 1.6 2002/08/22 23:06:11 sandro Exp $