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>

To: www-rdf-rules@w3.org

Date: Wed, 26 Nov 2003 13:20:23 -0500 (EST)

Message-Id: <200311261820.hAQIKNL07456@pantheon-po02.its.yale.edu>

To: www-rdf-rules@w3.org

[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 DepartmentReceived on Wednesday, 26 November 2003 13:20:29 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:15 UTC
*