From: Michael Kifer <kifer@cs.sunysb.edu>

Date: Mon, 23 Nov 2009 13:05:39 -0500

To: Jos de Bruijn <debruijn@inf.unibz.it>

Cc: RIF WG Public list <public-rif-wg@w3.org>

Message-ID: <20091123130539.48864854@kiferserv>

Date: Mon, 23 Nov 2009 13:05:39 -0500

To: Jos de Bruijn <debruijn@inf.unibz.it>

Cc: RIF WG Public list <public-rif-wg@w3.org>

Message-ID: <20091123130539.48864854@kiferserv>

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

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:57 UTC
*