---
title: "Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity"
authors:
  - "Fabio Massacci"
doi: ""
url: "https://ijcai.org/proceedings/2001/26"
pdf: "https://ijcai.org/proceedings/2001/0026.pdf"
venue: "Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence"
year: 2001
pages: "193-197"
track: ""
keywords:
---

# Decision Procedures for Expressive Description Logics with Intersection, Composition, Converse of Roles and Role Identity

Fabio Massacci

*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.