W3C home > Mailing lists > Public > www-rdf-interest@w3.org > October 2004

Re: mapping FOL -> DL

From: Enrico Franconi <franconi@inf.unibz.it>
Date: Sun, 10 Oct 2004 15:49:30 +0200
Message-Id: <358BCE04-1AC3-11D9-A9E5-000A9575BDDE@inf.unibz.it>
Cc: Peter <meancity@gmail.com>, www-rdf-interest@w3.org, <www-rdf-logic@w3.org>
To: Harry Halpin <hhalpin@ibiblio.org>
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



Received on Sunday, 10 October 2004 13:50:07 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:10 GMT