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

Calvanese, Diego; De Giacomo, Giuseppe; Lenzerini, Maurizio

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

Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini

Download BibTeX Cite

Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 84-88.

Abstract

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 to represent recursive structures. We study a DL comprising the most general form of fixpoint constructs on concepts, 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 role s, number restriction s, and general fixpoints .

Diego Calvanese, Giuseppe De Giacomo, and Maurizio Lenzerini. 1999. Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees. In Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI-99. IJCAI, 84–88. https://ijcai.org/proceedings/1999/13

@inproceedings{ijcai1999p13,
  title     = {Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees},
  author    = {Calvanese, Diego and De Giacomo, Giuseppe and Lenzerini, Maurizio},
  booktitle = {Proceedings of the Sixteenth International Joint Conference on
               Artificial Intelligence, {IJCAI-99}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Thomas Dean},
  pages     = {84--88},
  year      = {1999},
  note      = {Automated Reasoning},
  url       = {https://ijcai.org/proceedings/1999/13},
}

TY  - CPAPER
TI  - Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees
AU  - Calvanese, Diego
AU  - De Giacomo, Giuseppe
AU  - Lenzerini, Maurizio
T2  - Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI-99
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1999
SP  - 84
EP  - 88
UR  - https://ijcai.org/proceedings/1999/13
ER  -