2ATAs Make DLs easy

Proc. of the 15th Int. Workshop on Description Logics (DL 2002). Volume 53 of CEUR Workshop Proceedings, https://ceur-ws.org/. 2002.

In this paper we demonstrate that two-way alternating automata on infinite trees (2ATAs) provide a very elegant and effective formal tool for addressing reasoning in expressive DLs. Indeed, the encoding of a DL concept (to be checked for satisfiability) into an automaton (to be checked for non-emptiness) is: (i) intuitive, indeed, comparable to tableaux rules; (ii) modular, since each construct is dealt with separately; (iii) short, since the encoding is polynomial; and (iv) computationally adequate, i.e., optimally w.r.t. the complexity class of reasoning. To make these claims concrete, we illustrate the use of 2ATAs to decide satisfiability of three expressive DLs of increasing complexity, namely ALCF I reg, which corresponds to CPDL with local functionality, ALCF I breg , which extends ALCF I reg with boolean combinations of roles, and ALCQI breg , which further extends ALCF I breg with qualified number restrictions.

@inproceedings{DL-2002,
   title = "2ATAs Make DLs easy",
   year = "2002",
   author = "Diego Calvanese and De Giacomo, Giuseppe and Maurizio
Lenzerini",
   booktitle = "Proc. of the 15th Int. Workshop on Description Logics
(DL 2002)",
   pages = "107--118",
   volume = "53",
   publisher = "CEUR-WS.org",
   series = "CEUR Workshop Proceedings, https://ceur-ws.org/",
}