[DL] Decision problems of DL vs. FOL

[Enrico Franconi]

On 30 May 2010, at 03:38, Steve W wrote:

> 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?

The problems are equivalent, but the languages are different - typically DLs are fragments of FOL.

> For example, isn't subsumption checking equivalent to checking implication?

Indeed, but it is equivalent to checking logical implication between very special fragments of FOL:

\phi \models \psi

where \phi is a set of TBox and ABox axioms and \psi is a TBox (subsumption) axiom; so, if you are in a decidable DL, then \phi and \psi can not be full fledged FOL formulas.

> Is instance checking not equivalent to evaluating the truth value of a predicate given a constant?

Like above, where \psi is a set of ground atoms (ABox).

> 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?

All problems which make sense in FOL make sense in DLs: sat, validity, entailment, falsifiablity, etc. Moreover, in DLs some problems make more sense than in FOL, like classification, and all the non-standard DL reasoning problems (like least-common-subsumer, etc).

cheers
--e.