LATPub405: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| Zeile 18: | Zeile 18: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract= | |Abstract= In the area of Description Logic (DL), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case optimal 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 exponentially large. In the present paper, we formulate conditions under which an on-the-fly 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 satisfiability of concepts with respect to acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles. | ||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 52: | Zeile 36: | ||
year = {2008}, | year = {2008}, | ||
} | } | ||
}} | }} | ||
Version vom 23. März 2015, 13:24 Uhr
Automata Can Show PSPACE Results for Description Logics
Franz BaaderFranz Baader, Jan HladikJan Hladik, Rafael PeñalozaRafael Peñaloza
Franz Baader, Jan Hladik, Rafael Peñaloza
Automata Can Show PSPACE Results for Description Logics
Information and Computation, Special Issue: First International Conference on Language and Automata Theory and Applications (LATA'07), 206(9--10):1045-1056, 2008
Automata Can Show PSPACE Results for Description Logics
Information and Computation, Special Issue: First International Conference on Language and Automata Theory and Applications (LATA'07), 206(9--10):1045-1056, 2008
- KurzfassungAbstract
In the area of Description Logic (DL), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case optimal 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 exponentially large. In the present paper, we formulate conditions under which an on-the-fly 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 satisfiability of concepts with respect to acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@article{ BaaHlaPen-IC-08,
author = {Franz {Baader} and Jan {Hladik} and Rafael {Pe{\~n}aloza}},
journal = {Information and Computation, Special Issue: First International Conference on Language and Automata Theory and Applications ({LATA'07})},
number = {9--10},
pages = {1045--1056},
title = {Automata Can Show {PSPACE} Results for Description Logics},
volume = {206},
year = {2008},
}
