A tableaux decision procedure for SHOIQ
Ian Horrocks, Ulrike Sattler · Research Explorer (The University of Manchester) · 2005
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,