Re: ISSUE: OWL-DL compatibility

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/>