- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Wed, 18 Nov 2009 14:11:56 -0500
- To: Jos de Bruijn <debruijn@inf.unibz.it>
- Cc: Chris Welty <cawelty@gmail.com>, RIF WG Public list <public-rif-wg@w3.org>

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