[DL] Decision problems of DL vs. FOL

Thomas Schneider schneidt at cs.man.ac.uk
Wed Jun 2 23:51:26 CEST 2010

```On 2 Jun 2010, at 13:46, Steve W wrote:

> If I understand correctly, DL handles only unary and binary
> predicates -- is that supposed to be a limitation?

It is; together with other restrictions, see below ...

> Any n-ary predicates can be encoded as binary ones, e.g.,
> F(a,G(b,c)), right?

This is true, but binary predicates can't be used in DLs arbitrarily.
The only way to use them in the basic DL ALC is in guards of
quantifiers such as \exists y (R(x,y) \land C(y)) and nested versions
of this kind of expression. You have more ways of using roles (which
represent binary predicates) in more expressive DLs, but if you allow
their full use, you'd have to allow arbitrarily many variables to be
quantified over, and already the 3-variable fragment of FOL is
undecidable.

(Disclaimer: I admit that some features in more expressive yet still
decidable DLs require more than three variables in the standard
translation, but those are used in such a controlled way that the
target fragment is again restricted enough and more or less well-
behaved.)

> But, can any FOL formula be translated to DL?

No. The fragment obtained by translating any of the commonly used DLs
into FOL is strictly smaller than FOL; for ALC it's the guarded
fragment restricted to 2 variables.

Section 4.2 has some of this information and more ...

Cheers

Thomas

>
> Thanks for the pointer.
> Steve
>
>
> On 30 May 2010, at 02:38, Steve W wrote:
>
> Hi all,
>
> According to the Wikipedia article on DL, it says that the decision
> problems are more efficient than those of FOL. Are DL decision
> problems not equivalent to those in FOL? For example, isn't
> subsumption checking equivalent to checking implication? Is instance
> checking not equivalent to evaluating the truth value of a predicate
> given a constant? Assuming what I said is correct, then do all
> decision problems of DL have an equivalent form in FOL? Which
> problems of FOL are not supported by DL?
>
> Thanks for any input.
>
> Cheers,
> Steve
> ---
> **  You received this mail via the description logic mailing list;
> for more  **
> **  information, visit the description logic homepage at http://dl.kr.org/
> .  **
>
> +
> ----------------------------------------------------------------------+
> |  Dr Thomas Schneider                    schneider (at)
> cs.man.ac.uk  |
> |  School of Computer Science       http://www.cs.man.ac.uk/
> ~schneidt  |
> |  Kilburn Building, Room 2.114                 phone +44 161
> 2756136  |
> |  University of
> Manchester                                            |
> _       |
> |  Manchester M13 9PL
> (o~o)       |
> +-----------------------------------------------------oOOO--(_)--
> OOOo--+
>
> Prague (vb.)
>  To declaim loudly and pompously upon any subject about which the
>  speaker has less knowledge than at least one other person at the
>  table.
>
>                  Douglas Adams, John Lloyd: The Deeper Meaning of Liff
>
>
>
>
>
>
>
>
> ---
> **  You received this mail via the description logic mailing list;
> for more  **
> **  information, visit the description logic homepage at http://dl.kr.org/
> .  **
>
>

+----------------------------------------------------------------------+
|  Dr Thomas Schneider                    schneider (at) cs.man.ac.uk  |
|  School of Computer Science       http://www.cs.man.ac.uk/~schneidt  |
|  Kilburn Building, Room 2.114                 phone +44 161 2756136  |
|  University of Manchester                                            |
|  Manchester M13 9PL                                      (o~o)       |
+-----------------------------------------------------oOOO--(_)--OOOo--+

Prague (vb.)
To declaim loudly and pompously upon any subject about which the
speaker has less knowledge than at least one other person at the
table.

Douglas Adams, John Lloyd: The Deeper Meaning of Liff

-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 203 bytes
Desc: This is a digitally signed message part
URL: <https://mailman.informatik.uni-bremen.de/pipermail/dl/attachments/20100602/a430f5c6/attachment.sig>
```