TY - GEN
T1 - Decision procedures for expressive description logics with intersection, composition, converse of roles and role identity
AU - Massacci, F.
PY - 2001
Y1 - 2001
N2 - 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.
AB - 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.
M3 - Conference contribution
T3 - IJCAI International Joint Conference on Artificial Intelligence
SP - 193
EP - 198
BT - 17th International Joint Conference on Artificial Intelligence, IJCAI 2001
T2 - 17th International Joint Conference on Artificial Intelligence, IJCAI 2001
Y2 - 4 August 2001 through 10 August 2001
ER -