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

Date: Mon, 23 Nov 2009 17:30:36 +0100

Message-ID: <4B0AB8AC.6070301@inf.unibz.it>

To: kifer@cs.sunysb.edu

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

Date: Mon, 23 Nov 2009 17:30:36 +0100

Message-ID: <4B0AB8AC.6070301@inf.unibz.it>

To: kifer@cs.sunysb.edu

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

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/Received on Monday, 23 November 2009 16:30:48 UTC

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