Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity
Abstract
In the quest for expressive description logics for real-world applications, a powerful combination of constructs has so far eluded practical decision procedures: intersection and composition of roles. We propose tableau-based decision procedures for the satisfiability of logics extending ALC with the intersection⊓, composition◦, union⊔, converse · − of roles and role identity id(·). We show that 1. the satisfiability of ALC(⊓,◦, ⊔), for which a 2-EXPTIME upper bound was given by treeautomata techniques, is PSPACE-complete; 2. the satisfiability of ALC(⊓,◦, ⊔, · − , id(·)), an open problem so far, is in NEXPTIME. 1
Cite
Text
Massacci. "Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity." International Joint Conference on Artificial Intelligence, 2001.Markdown
[Massacci. "Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity." International Joint Conference on Artificial Intelligence, 2001.](https://mlanthology.org/ijcai/2001/massacci2001ijcai-decision/)BibTeX
@inproceedings{massacci2001ijcai-decision,
title = {{Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity}},
author = {Massacci, Fabio},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2001},
pages = {193-198},
url = {https://mlanthology.org/ijcai/2001/massacci2001ijcai-decision/}
}