$Revision: 1.1 $ $Date: 2002/08/19 21:08:18 $
Draft presentation of some research & software development
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 qualified that layered sentences were being described, not asserted. Various authors have suggested that constructing a sound a mechanism for asserting layered first-order logic is impossible. This research attempts to prove otherwise.
We take RDF to be a small sublanguage of FOL with a rather non-traditional syntax. We imagine another language, LX, which is a larger subject of FOL, perhaps including negation, disjunction, and universal quantification. LX sentences can be described and asserted (described as true) in RDF sentences (aka graphs or documents) using our logic layering vocabulary. RDF sentences can be examined to see which LX sentences they describe as true, and LX inference can be performed.
The basic mechanism of describing (encoding) and recognizing (decoding) LX sentences in RDF sentences is neither novel nor difficult, although we have not explored its computational complexity. (We implement decoding with an NP algorithm, but there may well be ones which are linear in the size of the extracted sentence.)
Our main contribution is axioms which tie LX sentences to RDF sentences which describe them as true. The entailment of an LX sentence is the same as the entailment of the conjunction of our axioms and an RDF sentence describing the LX sentence as true. Although we do not prove this for all LX sentences, we do demonstrate it for for many specific ones. There are also some complex sentences for which we have not been able to generate a proof, suggesting a possible flaw in the axioms.
We also believe the axioms are internally consistent (satisfiable). Our best evidence right now is that (1) the refutational proofs which otter finds for encodings of LX sentences matching themselves appear reasonable, and (2) an attempt to prove a contradiction in the axioms using hyper-resolution with a set-of-support strategy (which is complete) terminates finding no contradictions. Unfortunately, our attempts to find a finite model have not yet succeeded.
@@@@ pointers to work, in cvs tree in dev.
Sandro Hawke
First: 2002-03-29; This: $Id: Overview.html,v 1.1 2002/08/19 21:08:18 sandro Exp $