Re: plain rules, please

From: Sandro Hawke <sandro@w3.org>
Subject: Re: plain rules, please [was: Semantic Web Rule Language (SWRL) 0.5 released] 
Date: Wed, 26 Nov 2003 10:59:57 -0500

[...]

> > Compatible in what sense? I mean, "well, the orthogonal language needed 
> > to be entirely disjoint with OWL, and heck, it's also disjoint with OWL 
> > rules!" or "Once we figure out how to be usefully orthogonal and yet 
> > combinable with OWL, we'll find that we've subsumed OWL rules or at 
> > least fit in nicely with them"?
> 
> In the latter sense. 
> 
> > Personally, I don't yet have even a vague sense of this :(
> 
> I have a strong sense of it, but as I'm sometimes reminded, that
> doesn't mean I'm right.  I think of RDF-based logics (RDFS, OWL, SWRL,
> ...) in terms of FOL axioms on sentences like "rdf(s,p,o)".  I think
> this approach is suggested by LBase, and it's what Surnia (my quick
> hack OWL implementation) does.  From this angle, orthogonality and
> combinations of logics are fairly straightforward.

OK, let's see how easy it is to break this very strong claim!

>     -- sandro

Lets think of two extremely simple RDF-like logics, which I'll call RDF0
and RDC0, and give them ``meaning'' using the mechanism above.  Both RDF0
and RDC0 are written in triples, just like RDF and RDFS, where a triple
looks like <s,p,o> where s, p, and o are all URI references (which I will
write as QNames).  The proof theories for both RDF0 and RDC0 are given by
means the above translation (T) into plain FOL plus an axiomatization
(RDF0A/RDC0A), so that
	O1 |- O2  in RDF0
iff
	T(O1),RDF0Z |= T(O2)
and similarly for RDFC0.

RDF0 has one interpreted constant, rdf0:type, whose intended meaning is the
type relationship from RDF.  The obvious, uncontroversial axiomatization of
RDF0 is the empty set of axioms - there are just no extra axioms needed at
all for this very simple logic.

RDC0 has one interpreted constant, rdc0:subClassOf, whose intended meaning
is the subclass relationship from RDFS.  The axiomatization of RDC0 is 
	Ax rdf(x,rdc0:subClassOf,x) 
	Ax,y,z	rdf(x,rdc0:subClassOf,y) & rdf(y,rdc0:subClassOf,z) 
		-> rdf(x,rdc0:subClassOf,z)
This could be a bit controversial but note that RDC0 has no way of stating
that a URI reference denotes a class or not, so this makes the assumption
that everything is a class.  This does not really get us into trouble, and
certainly does not get us into trouble in RDC0.  

Now Sandros claim is that the combination of RDF0 and RDC0 is
straightforward.  I claim that it is not.  Certainly it is not the case
that the proof theory that results from the combination of the proof
theories of RDF0 and RDC0 gets what one wants, because
	<ex:a,rdf0:type,ex:c>,<ex:c,rdc0:subClassOf,ex:d>
does not imply
	<ex:a,rdf0:type,ex:d>
in this proof theory.

Instead a new proof theory has to be constructed for the combination of
RDF0 and RDC0.  This new proof theory may be a superset of the union of the
proof theories the two component logics, but it need not be.  To show this,
consider an extension of RDF0 (RDF1) that adds rdf1:Class, whose intended
meaning is as in RDFS, i.e., the class of all classes.  Now the combination
of RDF1 and RDC0 has the ability to state that something is a class, which
means that the first axiom for RDC0 should be replaced by
	Ax rdf(x,rdf0:type,rdf1:Class) -> rdf(x,rdc0:subClassOf,x)
	
So my claim is that axiomatizing logics, even using similar encodings for
both logics, does not provide a route to straightforward combination of
logics.

Peter F. Patel-Schneider
Bell Labs Research

PS:  Why then does the RDF/RDFS combination appear to work?  Well, it works
because RDFS is an extension of RDF, and thus all the hard work has been
already done in RDFS.

Received on Wednesday, 26 November 2003 11:51:59 UTC