Re: ISSUE: OWL-DL compatibility

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.

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

Received on Monday, 23 November 2009 18:06:15 UTC