Re: ISSUE: OWL-DL compatibility

Michael Kifer wrote:
> On Wed, 18 Nov 2009 16:06:06 +0100
> Jos de Bruijn <debruijn@inf.unibz.it> wrote:
>
>   
>>>>> 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
>>     
>
> Just to be clear: "whenever" means "if" here, right?
>   

Yes.
>   
>> 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))
>>     
>
> So, where is the universal quantifier in the body?
> What you have here is an axiom schema in RIF of the form:
>
> Forall ?x (tr'(c)(?x) :- tr(b)##tr(c) and tr'(b)(?x))
>   

I was also originally thinking about such an axiom schema, but that will
not work, since class identifiers are not in Dind.
This axiom schema would create unwanted connections between individuals
in Dind and classes.

Consider for example an OWL ontology with the statements:
a=b
a subclass c

This ontology does not entail b subclass c. When adding the mentioned
axiom and a##c to the ontology, b subclass c is entailed.


Cheers, Jos

> It does not mean that this axion is substituted in the body of a rule whenever
> c##b appears there. Otherwise, you would be claiming that Horn F-logic is not
> Horn, for example.
>
> michael
>
>
>  
>
>   
>> [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
>>>>>>>>>
>>>>>>>>>

Received on Thursday, 19 November 2009 11:18:24 UTC