[DL] Decision problems of DL vs. FOL

[Thomas Schneider]

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                                            |
> |  Oxford Road                                             _/// 
> _       |
> |  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                                            |
|  Oxford Road                                             _///_       |
|  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: <http://mailman.zih.tu-dresden.de/pipermail/dl/attachments/20100602/a430f5c6/attachment.sig>