Re: ISSUE: OWL-DL compatibility

Let's backtrack a little and try to summarize. The thread is now hard to
follow, I am afraid.

1. The issue of a##b in the body of the rules.

   This is the main question that sparked the whole discussion.
   You have stated that this somehow introduces universal quantification in the
   body of the rules and gave as an argument the fact that a##b implies
   is mapped to Forall ?x (tr'(b)(?x) :- tr'(a)(?x).
   But how does this demonstrate that this introduces universal quantification
   in rule bodies?
   After all,  H implies P  and  H implies Q does not mean Q implies P or vice
   versa.
   Your translation in Sec 9.2.1, which says 
      tr(b##c) = Forall ?x (tr'(c)(?x) :- tr'(b)(?x))
   does not seem to be the same as what the semantic says. The semantics says
   only that b##c implies the implication.

2. The argument against the axiom 
   Forall ?x (tr'(c)(?x) :- tr(b)##tr(c) and tr'(b)(?x))
   This seems to be an issue with the embedding that you present in the
   appendix, not with the semantics.
   The example that you brought up is interesting.
   OWL2:
     a=b
     a subclass c
   I think that when you have punning in the source language then the two
   occurrences of "a" should be mapped differently. Say, the individual "a" is
   mapped to "a" and the class occurrences of "a" should be mapped into
   something like class_a. That is, the class occurrences of symbols and their
   individual occurrences should be mapped using different tr-mappings.
   On the RIF side we'll have

     a=b
     a_class##c_class
     Forall ?x (c_class(?x) :- b_class##c_class and b_class)



regards
michael


On Fri, 27 Nov 2009 15:17:41 +0100
Jos de Bruijn <debruijn@inf.unibz.it> wrote:

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

Received on Saturday, 21 November 2009 03:42:36 UTC