Re: plain rules, please

   [Peter Patel-Schneider]
   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.

Just a technical point: One can can always arrange for the new proof
theory to be a superset of the union of the component proof theories,
by using namespaces to "hide" stuff that doesn't belong in the merged
proof theory.

In the example, the combined proof theory would have its own notion of
comb:subClassOf distinct from rdc0:subClassOf.  We'd have an axiom

    Axy (rdf(x, comb:subClassOf, y)
         <--> rdf(x, rdf0:type, rdf1:Class) & rdf(y, rdf0:type, rdf1:Class)
              & rdf(x, rdc0:subClassOf, y)

Semantics-wise, the interpretation of <x rdc0:subClassOf y> would be
different in the merged theory than in RDC0 itself.  It would mean
"either deno(x) is not a class or deno(y) is not a class or deno(x) is
a subset of denotation(y)."  (deno(term) is the denotation of term)
Otherwise, the axiom Ax (rdf(x, rdc0:subClassOf, x)) would be false,
and it has to stay true.

This has nothing to do with your main point, which I agree with.

                                             -- Drew


-- 
                                   -- Drew McDermott
                                      Yale Computer Science Department

Received on Wednesday, 26 November 2003 13:20:29 UTC