From: Drew McDermott <drew.mcdermott@yale.edu>
Date: Wed, 26 Nov 2003 13:20:23 -0500 (EST)
Message-Id: <200311261820.hAQIKNL07456@pantheon-po02.its.yale.edu>

```

[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

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:46:16 UTC