# [DL] DL Reasoner

Fernando Naufel do Amaral fnaufel at gmail.com
Wed Feb 9 18:06:08 CET 2011

On Sat, Jan 29, 2011 at 1:48 PM, Cássio Santos <cassio.comp at gmail.com> wrote:
> There are DL reasoners that supports ALCQI+ID?
> Where the ID means that we can represent the unitary cardinality of a
> concept, like a concept can have just one individual.

A few remarks. Please correct me if I'm mistaken.

1. I have run into the constructor Id(C) as denoting the identity
relation on a concept C. In other words, it is a role constructor
such that

interpr( Id(C) )  =  { (a, a) |  a \in interpr( C ) }

2. With this meaning, Id(C) can be defined in ALC as

\exists Id(C) . D  =  C \dland D

3. But you say that Id(C) is an assertion to the effect that the
interpretation of C is a singleton. As Luciano Serafini and
Markus Krötzsch have pointed out, you can use nominals (in OWL 1

C = {c}

4. But, to preserve correctness of inferences, nothing else can be
essentially as a Skolem constant in this context).

And I think there's a catch here: if you're using the unique name
assumption, this unique instance c of C cannot be referred to by
any other name.

So this definition only works if we drop the unique name
assumption.

5. Does the "+" in ALCQI+ID denote the transitive closure operator?
If it does, it cannot be expressed in OWL 2 DL.

Regards,

Fernando

--
Fernando Náufel, D.Sc.
fnaufel at ic.uff.br
http://fnaufel.wordpress.com
http://www.uff.br/llarc

(~Professor Doctor -- see http://en.wikipedia.org/wiki/Professor#Brazil)
LLaRC - Laboratório de Lógica e Representação do Conhecimento
DCT - Depto. de Ciência e Tecnologia
PURO - Pólo Universitário de Rio das Ostras
Brazil
--

> --
> Cássio Fernando,
> λSE - Language-oriented Software Engineering research group
>
> ---
> **  You received this mail via the description logic mailing list; for more
>  **
> **  information, visit the description logic homepage at http://dl.kr.org/.
>  **
>
>