Expressive ABox Reasoning with Number Restrictions, Role Hierarchies, and Transitively Closed Roles

We present a new tableaux calculus deciding the ABox consistency problem for the expressive description logic ALCNHR+ . Prominent language features of ALCNHR+ are number restrictions, role hierarchies, transitively closed roles, and generalized concept inclusions. The ABox description logic system RACE is based on the calculus for ALCNHR+ .

• Type: Conference
• Year: 2000
• Where: KR
• Authors: Volker Haarslev, Ralf Möller
• Keywords: ABox Consistency Problem, Automated Reasoning, Description Logic, Expressive Description Logic, KR 2000