Re: ISSUE: OWL-DL compatibility

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/