[DL] satisfiability vs. unsatisfiability

Franz Baader baader at tcs.inf.tu-dresden.de
Fri Apr 16 08:58:24 CEST 2010

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,


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/.
>  **

More information about the dl mailing list