Re: Disjoint vs. overlapping sorts

Jos de Bruijn wrote:
> Regarding my action:
> 
> "talk to Michael Kifer and have one of your post the results to the
> list" about the resolution of
> issue 31 (the question was about translating from OS to DS) (action 287).
> 
> 
> My original concern was that, when translating from the situation of
> disjoint sorts to a situation of overlapping sorts, and entailment would
> not be preserved, e.g.:
> 
> forall x,y (x=y)
> p(a)
> q(b)
> 
> entails q(a) in the case of overlapping sorts (since p and q are
> interpreted as the same object), but not in the case of disjoint sorts
> (because the variables x and y are interpreted in the individual domain,
> and p, q are interpreted in the unary predicate domain).
> 
> When talking to Michael, we came to the conclusion that the above
> formulas are actually not proper RIF formulas for the case of disjoint
> sorts, since the symbols do not have an associated sort.
> The formulas would be represented in the following way:
> 
> forall x^I,y^I (x^I=y^I)
> p^P1(a^I)
> q^P1(b^I)
> 
> where I is the sort of individuals, and P1 is the sort of unary predicates.
> 
> In the case of disjoint sorts, the following formulas are theorems:
> 
> forall x^I,y^P1 (x^I != y^P1)
> forall x^I,y^P2 (x^I != y^P2)
> forall x^P1,y^P2 (x^P1 != y^P2)
> ......
> 
> We can thus axiomatize disjoint sorts in the overlapping sorts example.
>  This is, however, not necessary if we restrict ourselves to formulas
> which are allowed to be written in the disjoint sorts case (i.e. no
> equality statements involving different sorts).
> 
> The following can be easily shown (and would need be to be part of some
> RIF document which describes how languages with disjoint sorts
> interoperate with RIF):
> 
> Let phi and psi be two disjoint-sort formulas, then
> 
> phi |=ds psi    iff     phi |=os psi
> 
> where |=ds is entailment in the case of disjoint sorts, and |=os is
> entailment in the case of overlapping sorts.

I'm not quite sort how this addresses the issue you raised but if you 
are convinced then fine.

However, I'm also not instantly convinced it is correct for all 
plausible interpretations of "overlapping sorts".

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"?

Or does the proposed model theory for RIF with overlapping sorts differ 
from the OWL approach sufficiently to invalidate the first entailment?

Dave
-- 
Hewlett-Packard Limited
Registered Office: Cain Road, Bracknell, Berks RG12 1HN
Registered No: 690597 England

Received on Tuesday, 22 May 2007 14:35:46 UTC