Re: ISSUE: OWL-DL compatibility

>>> Unless anyone else has an opinion, Jos are you willing to make that change?
>> I updated the syntax and semantics of RIF-OWL DL combinations, as well
>> as the embedding of RIF-OWL 2 RL combinations accordingly:
> 
> Thanks Jos.
> Please see questions within.
> 
>> - in class membership formulas a#b, b must be a constant symbol
>> - in subclass formulas b##c, c,b must be constant symbols
>> - subclass formulas may only occur as facts
>>
>> I imposed the last restriction, because I believe that in BLD-OWL 2 RL
>> combinations, using subclass statements in rule bodies necessarily
>> amounts to have been to introduce universal quantification in the body,
>> making such combinations outside horn, which I think is undesirable.
> 
> Can you elaborate? How does this introduce universal quantification? 

The semantic correspondence between subclasses in OWL and ## in RIF is
defined as follows [1]:

C(c) is a subset of C(d) whenever Itruth(Isub(IC(<c>),IC(<d>))) = t, for
any two IRIs c and d

Now, since there is a strict separation between the interpretation of
individuals and classes in the OWL direct semantics, we cannot objects
in Dind to represent classes. Thus, like we did for frame formulas, we
need to change the interpretation of subclass formulas [2]:

Isub is a mapping D × D → D


If we now want to embed this modified RIF into standard RIF [3] the only
embedding I can come up with for b##c is
(a)  Forall ?x (tr'(c)(?x) :- tr'(b)(?x))


[1]
http://www.w3.org/2005/rules/wiki/SWC#Semantics_of_RIF-OWL_DL_Combinations
[2]
http://www.w3.org/2005/rules/wiki/SWC#Modified_Semantics_for_RIF_Subclass.2C_Membership.2C_and_Frame_Formulas
[3]
http://www.w3.org/2005/rules/wiki/SWC#Embedding_RIF_DL-document_formulas_into_RIF_BLD

> And why
> does it matter anyway?
> We already have universal quantification on the OWL side, so any OWL
> predicate that occurs in a rule body potentially brings in universal
> quantification. A combination of OWL+Horn is not Horn, so I don't understand
> your concerns.

A combination of OWL 2 RL (which is Horn) with Horn should be Horn as
well, IMHO.
Besides, full OWL 2 DL does not introduce arbitrary universal
quantification. In particular, formulas of the form (a) cannot appear
inside axioms. If formulas of the form (a) would be allowed to appear in
the bodies of rules, known techniques for reasoning with DL-safe
OWL+Horn cannot be used for RIF-OWL DL combinations.

> 
>> Besides, having subclass statements in rules without allowing variables
>> does not seem all that useful.
> 
> We don't really know that. If there is a legitimate concern -- then yes. But I
> don't understand your concern, so please elaborate.

To summarize: my main concerns are that if a##b is allowed in rule bodies:

- it is not possible to use rules reasoning with RIF-OWL2RL combinations
- it is not possible to use know techniques for reasoning with DL-safe
OWL+Horn for DL-safe RIF-OWL DL combinations



Cheers, Jos

> 
> cheers
> michael
> 
>> Best, Jos
>>
>>>
>>> Michael Kifer wrote:
>>>> Yes, I agree that 3a is a reasonable fix. 3b is too big of a change,
>>>> and I was
>>>> not suggesting it for this round.
>>>>
>>>> michael
>>>>
>>>>
>>>> On Tue, 10 Nov 2009 10:53:32 -0500
>>>> Chris Welty <cawelty@gmail.com> wrote:
>>>>
>>>>> I read this a little more carefully.
>>>>>
>>>>> Basically, the issue is whether to add some correspondence between
>>>>> rif:subclass and rdf:subclass and between rif:type and rdf:type *in
>>>>> the OWL compatibility section* of SWC.  Such a correspondence is
>>>>> already there for RDF compatibility, but Michael noted that it is not
>>>>> "inherited" by the "OWL-DL" (now know as OWL Direct Semantics)
>>>>> section.  So, currently in SWC, the OWL-DL compatibility has no
>>>>> correspondence between the rather obvious type/subclass relations in
>>>>> the two languages.
>>>>>
>>>>> I agree this is a problem and should be fixed, and option #1 in
>>>>> Michael's analysis, copied below (to leave it as is) is unacceptable.
>>>>>
>>>>> Option #2 is to just add a sentence to the text saying there is no
>>>>> correspondence between owl and rif type/subclass.  This is less than
>>>>> satisfactory.
>>>>>
>>>>> Option #3 is to "fix" it somehow, and there are two variations there,
>>>>> I'll call them 3a (just repeat the correspondences from RDFS in
>>>>> OWL-DL) and 3b (do the best possible job mapping between owl and rif
>>>>> subclass).
>>>>>
>>>>> </chair>I prefer option 3a.  I agree with Jos' analysis of option 3b
>>>>> and think it is too big a change.<chair>
>>>>>
>>>>> As chair, I am also willing to accept 2 or 3a as an oversight and bug
>>>>> fix (I personally thought the correspondence between type and
>>>>> subclass were "inherited" from the RDF correspondence, so 3a would
>>>>> just make it the way I thought it was), however 3b seems to me,
>>>>> procedurally, to be much more significant and requires a new last
>>>>> call for SWC.
>>>>>
>>>>> -Chris
>>>>>
>>>>> Jos de Bruijn wrote:
>>>>>>> In today's telecon I was asked to reanimate the issue of OWL
>>>>>>> compatibility,
>>>>>>> which was discussed 1 month ago.
>>>>>>>
>>>>>>> Here is the relevant message:
>>>>>>>
>>>>>>> http://lists.w3.org/Archives/Public/public-rif-wg/2009Sep/0017.html
>>>>>>>
>>>>>>> The current situation is a bug, IMO. If it isn't a bug then at
>>>>>>> least that part
>>>>>>> of the document is very unsatisfactory and obscure. Jos proposed 3
>>>>>>> solutions:
>>>>>>>
>>>>>>> 1- leave things as they are, assuming that # and ## are not of
>>>>>>> interest
>>>>>>>    to users of RIF-OWL DL combinations
>>>>>>> 2- explain the use of # and ## in the document (this would
>>>>>>> certainly not
>>>>>>>    be a substantive change, so we should not run into procedural
>>>>>>> problems)
>>>>>>> 3- define the semantics of # and ## in RIF-OWL DL combinations in a
>>>>>>>    similar fashion as in RIF-RDF combinations: a one-to-one
>>>>>>> correspondence
>>>>>>>    between # and OWL class membership statements and implication
>>>>>>> between ##
>>>>>>>    and OWL subclassing.
>>>>>>>
>>>>>>> The easiest for him would be to do nothing (1), thus leaving things
>>>>>>> unsatisfactory and obscure. His next choice is (3), which is also
>>>>>>> my choice and
>>>>>>> the "right thing to do."  (3) stretches things a little, but it can
>>>>>>> be argued
>>>>>>> that it is a simple fix.
>>>>>> In my earlier e-mail to Michael referred to I did not say what my
>>>>>> preference is among the mentioned options.  I guess arguments can be
>>>>>> made for all three options, so in fact I do not have a strong
>>>>>> preference, but I do have a concern about option (3): implementation
>>>>>> might be harder.  If, for example, implementation is done through
>>>>>> embedding in other rules system, like the embedding of RIF-OWL2RL
>>>>>> combination in the appendix of the document, quite a few rules need to
>>>>>> be added for the ## construct.
>>>>>> In particular, for every pair of distinct class names (A,B), we need to
>>>>>> add the rule:
>>>>>>
>>>>>> Forall ?x (?x[rdf:type -> B] :- And(?x[rdf:type -> A] A##B))
>>>>>>
>>>>>> This means adding a quadratic number of rules.
>>>>>>
>>>>>> Dealing with # is easy: in the mapping of RIF DL-document formulas to
>>>>>> RIF documents [1] we simply map a#b to tr'(b)(a). Clearly, we would
>>>>>> restrict b in formulas a#b to constant symbols.
>>>>>>
>>>>>>
>>>>>> [1]
>>>>>> http://www.w3.org/TR/rif-rdf-owl/#Embedding_RIF_DL-document_formulas_into_RIF_BLD
>>>>>>
>>>>>>
>>>>>>
>>>>>>> Solution (2) is more work. It fixes the obscurity aspect, not the
>>>>>>> unsatisfactory aspect of the definitions. So, (3) seems like the
>>>>>>> best way to
>>>>>>> proceed.
>>>>>>>
>>>>>>> Solution (3) still leaves some problems, which are unrelated to the
>>>>>>> above
>>>>>>> issues. In the current semantics, subclassing in RIF implies
>>>>>>> subclassing in
>>>>>>> OWL/RDF, but not vice versa.
>>>>>>>
>>>>>>> In this regard, I would like to point to my follow-up message
>>>>>>> http://lists.w3.org/Archives/Public/public-rif-wg/2009Sep/0019.html
>>>>>>> Here I proposed a stronger semantics, which fixes this
>>>>>>> non-entailment problem.
>>>>>> Michael proposed the following semantics:
>>>>>>
>>>>>> {(A,B) | A rdfs:subclassOf B and A != B on the RDF side}
>>>>>>                 = {(A,B) | A##B on the RIF side}
>>>>>>
>>>>>> I feel that this would take us out of Horn, even when considering
>>>>>> Simple
>>>>>> entailment, because implementation would require (classical) negation.
>>>>>> At least, that is the only way I current see how this could be
>>>>>> implemented. As we know, classical negation in the body amounts to
>>>>>> disjunction in the head, so we would end up adding the following
>>>>>> rule to
>>>>>> the embedding of RDF-RDF combinations:
>>>>>>
>>>>>> Forall ?x, ?y (Or(?x##?y ?x=?y) :- ?x[rdfs:subClassOf -> ?y])
>>>>>>
>>>>>> For RIF-OWL DL combinations such a semantics is even more problematic,
>>>>>> because subclass in OWL DL means subset relation between class
>>>>>> extensions, so the condition would look something like (X^C is the
>>>>>> class
>>>>>> extension of X):
>>>>>>
>>>>>> {(A,B) | A^C subset B^C and A^C != B^C on the RDF side}
>>>>>>                 = {(A,B) | A##B on the RIF side}
>>>>>>
>>>>>> (Actually, we will need to apply some tricks here, since A and B are
>>>>>> not
>>>>>> constants on the OWL side, but I guess we can come up with a definition
>>>>>> that kind-of achieves this semantics)
>>>>>>
>>>>>> A formula implementing the => direction of the condition for a pair of
>>>>>> class names A,B would look something like (again, negation in the body
>>>>>> becomes disjunction in the head):
>>>>>>
>>>>>> Forall ?x (
>>>>>>   Or(A##B
>>>>>>      And(Forall ?x(?x[rdf:type -> B] :- ?x[rdf:type -> A])
>>>>>>          Forall ?x(?x[rdf:type -> A] :- ?x[rdf:type -> B])))
>>>>>>   :-
>>>>>>   Forall ?x(?x[rdf:type -> B] :- ?x[rdf:type -> A]))
>>>>>>
>>>>>>
>>>>>> So, I would not be in favor of extending either the semantics of RDF or
>>>>>> the semantics of OWL DL combinations with such a condition.
>>>>>>
>>>>>>
>>>>>> Best, Jos
>>>>>>> This would certainly be a substantive change semantically (although
>>>>>>> not
>>>>>>> significant textually). If we don't have the energy to do it this
>>>>>>> time,
>>>>>>> maybe for RIF 1.1.
>>>>>>>
>>>>>>> michael
>>>>>>>

-- 
                         debruijn@inf.unibz.it
Jos de Bruijn,        http://www.debruijn.net/

Received on Wednesday, 18 November 2009 15:06:48 UTC