Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees

Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI 1999). 1999.

In the last years, the investigation on Description Logics (DLs) has been driven by the goal of applying them in several areas, such as, software engineering, information systems, databases, information integration, and intelligent access to the web. The modeling requirements arising in the above areas have stimulated the need for very rich languages, including fixpoint constructs on concepts to represent recursive structures. We study a DL comprising the most general form of fixpoint constructs, all classical concept forming constructs, plus inverse roles, n-ary relations, qualified number restrictions, and inclusion assertions. We establish the EXPTIME decidability of such logic by presenting a decision procedure based on a reduction to nonemptiness of alternating automata on infinite trees. We observe that this is the first decidability result for a logic combining inverse roles, number restrictions, and general fixpoints.

@inproceedings{IJCAI-1999,
   title = "Reasoning in Expressive Description Logics with Fixpoints based on
Automata on Infinite Trees",
   year = "1999",
   author = "Diego Calvanese and De Giacomo, Giuseppe and Maurizio
Lenzerini",
   booktitle = "Proc. of the 16th Int. Joint Conf. on Artificial Intelligence
(IJCAI 1999)",
   pages = "84--89",
}