# Logic Layering (with RDF)

### Status

$Revision: 1.1 $ $Date: 2002/08/19 21:08:18 $

Draft presentation of some research & software development

## 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 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.

## Approach and Current Results

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 $