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

Date: Fri, 27 Nov 2009 15:17:41 +0100

Message-ID: <4B0FDF85.5050306@inf.unibz.it>

To: kifer@cs.sunysb.edu

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

Date: Fri, 27 Nov 2009 15:17:41 +0100

Message-ID: <4B0FDF85.5050306@inf.unibz.it>

To: kifer@cs.sunysb.edu

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

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

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:57 UTC
*