Re: mapping FOL -> DL

On 27 Sep 2004, at 21:38, Harry Halpin wrote:
> Is there any way to map from FOL->DL while minimizing expressive power 
> lost? While I'm being informal with "minimizing expressive power 
> lost", I mean either:
>    a) Given a formula \phi, the translated formula T(\phi) should be
>       logically equivalent to \phi.
>    b) Given a formula \phi, the translated formula T(\phi) should be
>       satisfiable iff the formula \phi is satisfiable.
> Now, clearly this won't work for all of FOL, but it could for some 
> statements. And you think there would be ways of going from FOL->DL 
> that were sensible.

The problem of checking whether a FOL formula is expressible in some 
(expressive) DL is in general undecidable - by resorting to the general 
undecidability results from the Guarded Fragment modal logic community.
Given this result, you may end up in approximating a FOL formula in the 
DL while it would be correctly and completely expressible in the DL.

cheers
--e.

Enrico Franconi                  - franconi@inf.unibz.it
Free University of Bozen-Bolzano - http://www.inf.unibz.it/~franconi/
Faculty of Computer Science      - Phone: (+39) 0471-016-120
I-39100 Bozen-Bolzano BZ, Italy  - Fax:   (+39) 0471-016-129