Re: ISSUE: OWL-DL compatibility

Michael Kifer wrote:
> 
> On Thu, 19 Nov 2009 12:15:53 +0100
> Jos de Bruijn <debruijn@inf.unibz.it> wrote:
> 
>> 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
> .....
>>>> 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.
> 
> Hold on! a,b, and c are predicates. How can you write a=b in BLD?

No, but you can in OWL

> If you meant a=b in OWL-DL, then it means a subclass b and b subclass a, isn't
> it?  So, b subclass c is entailed.

No. OWL 2 has punning, which means you can use the same identifier as
both a class and an instance, but they are interpreted contextually.

> If you mean a=b in RDF then this cannot be
> even mapped to BLD.
> 
> In any case, I don't see how any of your arguments support your assertion that
> ## in the rule body somehow bring universal quantification into the rule bodies
> of BLD.

I showed that your proposed embedding (the one with the axiom schemas)
is not faithful. I believe my embedding, where statements b##c are
mapped to formulas
(a) Forall ?x (tr'(c)(?x) :- tr'(b)(?x)
is.

> To me this all looks like a non-sequitur. If you can provide a formal argument,
> please do.

I do not have a formal argument. I simply have not been able to come up
with a faithful embedding that avoids universal formulas (a) in rule bodies.
I think it is unwise to introduce features in the language that nobody
knows how to deal with.


Best, Jos

> 
> regards
> michael
> 
>  
>> 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
>>>>>>>>>>>
>>>>>>>>>>>                   
>>
> 

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

Received on Friday, 20 November 2009 14:18:32 UTC