Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity
Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence. Pages 193-197.
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 u, composition ◦, union t, converse ·− of roles and role identity id(·). We show that 1. the satisfiability of ALC(u,◦, t), for which a 2-EXPTIME upper bound was given by treeautomata techniques, is PSPACE-complete; 2. the satisfiability of ALC(u,◦, t, ·−, id(·)), an open problem so far, is in NEXPTIME.
@inproceedings{ijcai2001p26,
title = {Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity},
author = {Massacci, Fabio},
booktitle = {Proceedings of the Seventeenth International Joint Conference on
Artificial Intelligence, {IJCAI-01}},
publisher = {International Joint Conferences on Artificial Intelligence},
pages = {193--197},
year = {2001},
url = {https://ijcai.org/proceedings/2001/26},
}
TY - CPAPER TI - Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity AU - Massacci, Fabio T2 - Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI-01 PB - International Joint Conferences on Artificial Intelligence PY - 2001 SP - 193 EP - 197 UR - https://ijcai.org/proceedings/2001/26 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
