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

Date: Mon, 23 Nov 2009 16:58:59 +0100

Message-ID: <4B0AB143.80000@inf.unibz.it>

To: kifer@cs.sunysb.edu

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

Date: Mon, 23 Nov 2009 16:58:59 +0100

Message-ID: <4B0AB143.80000@inf.unibz.it>

To: kifer@cs.sunysb.edu

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

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 15:59:15 UTC

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