Re: ISSUE-5: n-ary datatypes - decidability on merging

On Tue, 13 Nov 2007, Jeremy Carroll wrote:
>
>> I mean this on an anstract and intuitive level. It may not be reflected
>> in the Pan-Horrocks formalization, I don't know. The point is, it *could*
>> easily be formalized. But it would look somewhat awkward. The question
>> is: is it worth it, only to get well-behaved mergers of, as you say,
>
> I find this credible - but feel that it is appropriate to indicate that (to 
> my somewhat limited knowledge) such formal work has not been done, and 
> without it we only have hunch and intuition as to quite what interactions 
> will happen.

There's more than hunch and intuition. Actually, the intuitive view
that I have been describing has a solid formal basis, namely the so-
called "fusion" of logics. In a nutshell, the fusion of two
symbol-disjoint logical systems is obtained by uniting the axiom
systems of those systems.  It is known that then, decidability
transfers from the components to the fusion. See

F. Baader, C. Lutz, H. Sturm, and F. Wolter.  Fusions of Description
Logics and Abstract Description Systems.  Journal of Artificial
Intelligence Research (JAIR), 16:1?58, 2002.

This paper may not be very accessible to a general OWL audience. What
we call datatypes in OWL is called concrete domains in that paper, and 
a result (but now quite the one we need) about concrete domains is
proved in Section 5.3.

I do not claim that you will find my intuitive statements one-to-one
in that paper. But what we would need to formalize your wishes is an
easy instance of the general approach in that paper.

greetings,
 		Carsten

--
*      Carsten Lutz, Institut f"ur Theoretische Informatik, TU Dresden       *
*     Office phone:++49 351 46339171   mailto:lutz@tcs.inf.tu-dresden.de     *

Received on Tuesday, 13 November 2007 18:20:51 UTC