Abstract | ||
---|---|---|
In Description Logics (DLs), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as concept satisfl- ability. Whereas tableau-based algorithms usually yield worst-case opti- mal algorithms in the case of PSpace-complete logics, it is often very hard to design optimal tableau-based algorithms for ExpTime-complete DLs. In contrast, the automata-based approach is usually well-suited to prove ExpTime upper-bounds, but its direct application will usually also yield an ExpTime-algorithm for a PSpace-complete logic since the (tree) automaton constructed for a given concept is usually exponen- tially large. In the present paper, we formulate conditions under which an on-the-∞y construction of such an exponentially large automaton can be used to obtain a PSpace-algorithm. We illustrate the usefulness of this approach by proving a new PSpace upper-bound for satisflability of concepts w.r.t. acyclic terminologies in the DL SI. |
Year | Venue | Keywords |
---|---|---|
2007 | Description Logics | description logic,design optimization,upper bound |
Field | DocType | Citations |
Discrete mathematics,Computer science,Automaton,Algorithm,PSPACE | Conference | 0 |
PageRank | References | Authors |
0.34 | 16 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Franz Baader | 1 | 8123 | 646.64 |
Jan Hladik | 2 | 84 | 8.89 |
Rafael Peñaloza | 3 | 459 | 62.80 |