From: Michael Kifer <kifer@cs.sunysb.edu>

Date: Thu, 19 Nov 2009 15:24:23 -0500

To: Jos de Bruijn <debruijn@inf.unibz.it>

Cc: Chris Welty <cawelty@gmail.com>, RIF WG Public list <public-rif-wg@w3.org>

Message-ID: <20091119152423.19565b20@kiferdesk>

Date: Thu, 19 Nov 2009 15:24:23 -0500

To: Jos de Bruijn <debruijn@inf.unibz.it>

Cc: Chris Welty <cawelty@gmail.com>, RIF WG Public list <public-rif-wg@w3.org>

Message-ID: <20091119152423.19565b20@kiferdesk>

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? 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. 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. To me this all looks like a non-sequitur. If you can provide a formal argument, please do. 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 Thursday, 19 November 2009 20:25:00 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Thursday, 19 November 2009 20:25:01 GMT
*