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

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 intersectionSquare cap, composition○, unionSquare cup, converse· - of roles and role identity id(·). We show that 1. the satisfiability of ALC(Square cap,○, Square cup), for which a 2-EXPTIME upper bound was given by tree-automata techniques, is PSPACE-complete; 2. the satisfiability of ALC(Square cap,○, Square cup·-, id(·)), an open problem so far, is in NEXPTIME.