Re: ISSUE: OWL-DL compatibility

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?

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

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 Wednesday, 18 November 2009 19:12:39 UTC