Re: ISSUE: OWL-DL compatibility

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/