A Tableau Decision Procedure for SHOIQ

Abstract. OWL DL, a new W3C ontology language recommendation, is based on the expressive description logic SHOIN. Although the ontology consistency problem for SHOIN is known to be decidable, up to now there has been no known “practical” decision procedure, i.e., a goal directed procedure that is likely to perform well with realistic ontology derived problems. We present such a decision procedure for SHOIQ, a slightly more expressive logic than SHOIN, extending the well known algorithm for SHIQ, which is the basis for several highly successful implementations.

• Type: Journal
• Year: 2007
• Where: JAR
• Authors: Ian Horrocks, Ulrike Sattler
• Keywords: Description Logic Shoin, JAR 2007, Ontology Language Recommendation, SHOIN