Re: Disjoint vs. overlapping sorts

<snip/>

>> Consider OWL/full, map class extensions to unary predicates, then:
>>
>>    C^I = D^I  |=os  C^P1 = D^P1
>>
>> but
>>
>>    NOT   C^I = D^I  |=ds  C^P1 = D^P1
>>
>> Are (C^I = D^I) and (C^P1 = D^P1) not "disjoint-sort formulae"?

<snip/>

>> Or does the proposed model theory for RIF with overlapping sorts differ
>> from the OWL approach sufficiently to invalidate the first entailment?
> 
> The first entailment is perfectly valid in RIF.

I have to correct my statement here; I misread the specification.  This
entailment is in fact not valid in RIF, because RIF sees "C^I" as a
single constant symbol (i.e. the sort is part of the constant symbol).

So, c^a=d^a does not imply c^b=d^b, and also c=d does not imply c^a=d^a
(at least, according to the current specification).

However, identifiers in an OWL Full ontology would probably all be of to
sort rdfs:Resource, so the entailment question would look like:

C^rdfs:Resource = D^rdfs:Resource  |=os  C^rdfs:Resource = D^rdfs:Resource


which is obviously valid.


Best, Jos

> 
> 
> Best, Jos
> 
> 
>> Dave
> 

-- 
Please note my new email address:
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
In heaven all the interesting people are
missing.
  - Friedrich Nietzsche