- From: Jos de Bruijn <debruijn@inf.unibz.it>
- Date: Tue, 24 Nov 2009 13:59:08 +0100
- To: kifer@cs.sunysb.edu
- CC: RIF WG Public list <public-rif-wg@w3.org>
- Message-ID: <4B0BD89C.1010104@inf.unibz.it>

Michael Kifer wrote: > oh well. I see it is indeed tricky. > I think then it is very desirable to explain which problems arise without the > restriction on ##. Otherwise, this restriction looks weird. And saying that > this introduces universal quantification in rule bodies is not accurate. Agreed. I will come up with a text (also explaining the restriction on quantification) that I hope will be satisfactory. Best, Jos > > michael > > > On Mon, 23 Nov 2009 17:30:36 +0100 > Jos de Bruijn <debruijn@inf.unibz.it> wrote: > >> I think I found a counterexample for using the proposed embedding into >> DL-safe SWRL-like languages: >> >> Say, you have an OWL DL ontology: >> >> forall x (x=a) (in OWL syntax: SubClass(owl:Thing OneOf(a)) >> >> and the RIF rule: >> >> a##b >> >> their combination entails >> SubClass(a b) >> but does not entail >> SubClass(b a) >> >> >> if we embed this combination as follows: >> >> forall ?x (?x=a) >> a'##b' >> Forall ?x (b_class(?x) :- ##(a',b') and a_class(?x)) >> Forall ?x (a_class(?x) :- ##(b',a') and b_class(?x)) >> >> the obtained theory DOES entail (the translation of) SubClass(b a), >> since a' and b' are necessarily mapped to the same individual in the >> domain (a'=b' is entailed). >> (what is crucial to the counter-example here is that SWRL-like languages >> have a strict separation between the abstract and concrete domains, >> i.e., an IRI cannot be mapped to a data value; it is always mapped to >> the individual domain) >> >> >> Best, Jos >> >> >> >> Jos de Bruijn wrote: >>> Michael Kifer wrote: >>>> 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. >>> You are absolutely right. >>> The translation in the appendix only works if ##-atoms are not allowed >>> in rule bodies. I actually don't know at the moment how ##-atoms in rule >>> bodies could be translated. >>> >>>> 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 what happens in the embedding in section 9.2.1: tr(b) and tr'(b) >>> are distinct constants. >>> >>>> 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) >>> Is this meant to be the result of the embedding of DL-document formula >>> containing >>> >>> a=b >>> a##c >>> >>> into RIF BLD? >>> >>> One problem here is that >>> Forall ?x (c_class(?x) :- b_class##c_class and b_class) >>> is not well-formed RIF because the same constant (b_class, c_class) >>> appears both as individual and as predicate here. >>> >>> However, this is easy to remedy by using an embedding that yields >>> >>> a=b >>> a'##c' >>> Forall ?x (c_class(?x) :- b'##c' and b_class) >>> >>> For this example the embedding works. However, I am not convinced that >>> it works in general, since OWL does have non-ground equality and I_C(b') >>> and I_C(c') are in D_ind. I do not have a counter-example at the moment, >>> but I also cannot think of an argument for correctness of this embedding >>> right now. >>> >>> >>> Cheers, Jos >>> >>> >>> <snip/> >>> -- Jos de Bruijn debruijn@inf.unibz.it +390471016224 http://www.debruijn.net/

Received on Tuesday, 24 November 2009 12:59:17 UTC