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 PS-complete logics, it is often very hard to design optimal tableau-based algorithms for ET-complete DLs. In contrast, the automata-based approach is usually well-suited to prove ET upper-bounds, but its direct application will usually also yield an ET-algorithm for a PS-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 PS-algorithm. We illustrate the usefulness of this approach by proving a new PS upper-bound for satisfiability of concepts with respect to acyclic terminologies in the DL , which extends the basic DL with transitive and inverse roles.

Baader, F., Hladik, J., Penaloza, R. (2008). Automata can show PSpace results for description logics. INFORMATION AND COMPUTATION, 206(9-10), 1045-1056 [10.1016/j.ic.2008.03.006].

Automata can show PSpace results for description logics

Penaloza, R
2008

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 PS-complete logics, it is often very hard to design optimal tableau-based algorithms for ET-complete DLs. In contrast, the automata-based approach is usually well-suited to prove ET upper-bounds, but its direct application will usually also yield an ET-algorithm for a PS-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 PS-algorithm. We illustrate the usefulness of this approach by proving a new PS upper-bound for satisfiability of concepts with respect to acyclic terminologies in the DL , which extends the basic DL with transitive and inverse roles.
Articolo in rivista - Articolo scientifico
pspace automata, description logics, reasoning
English
1045
1056
12
Baader, F., Hladik, J., Penaloza, R. (2008). Automata can show PSpace results for description logics. INFORMATION AND COMPUTATION, 206(9-10), 1045-1056 [10.1016/j.ic.2008.03.006].
Baader, F; Hladik, J; Penaloza, R
File in questo prodotto:
File Dimensione Formato  
BaaHlaPen-IC-08.pdf

accesso aperto

Tipologia di allegato: Submitted Version (Pre-print)
Dimensione 216.73 kB
Formato Adobe PDF
216.73 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/256776
Citazioni
  • Scopus 23
  • ???jsp.display-item.citation.isi??? 11
Social impact