[DL] satisfiability vs. unsatisfiability

[Franz Baader]

Since ExpTime is a deterministic complexity class, it is actually
irrelevant whether you consider satisfiability or unsatisfiability.
Thus, Theorem 3.27 also holds for satisfiability, and the hardness
trivially transfers to the larger language ALC.

Note, however, that ExpTime-hardness for ALC with GCI was known before
(see the IJCAI'912 paper by Schild). The result for AL is a
strengthening of this. The most recent result in this direction is
that, even for FL_0, subsumption w.r.t. GCIs is ExpTime hard (see my
ECAI'05 paper with Sebastian Brandt and Carsten Lutz).

Best regards,

-Franz

On Wed, Apr 14, 2010 at 5:41 PM,  <longo at dmi.unict.it> wrote:
> Theorem 3.27 of the Description Logics Handbook says that in the dl AL the
> UN-satisfiability of a concept w.r.t. a finite set of inclusions is ExpTime
> hard. Do this result extends to the satisfiability (of a concept ...) in
> ALC?
>
> Thank you in advance,
> Cristiano Longo
>
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
>
> ---
> **  You received this mail via the description logic mailing list; for more
>  **
> **  information, visit the description logic homepage at http://dl.kr.org/.
>  **
>