A Tableaux 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,
Cite
Text
Horrocks and Sattler. "A Tableaux Decision Procedure for SHOIQ." International Joint Conference on Artificial Intelligence, 2005.Markdown
[Horrocks and Sattler. "A Tableaux Decision Procedure for SHOIQ." International Joint Conference on Artificial Intelligence, 2005.](https://mlanthology.org/ijcai/2005/horrocks2005ijcai-tableaux/)BibTeX
@inproceedings{horrocks2005ijcai-tableaux,
title = {{A Tableaux Decision Procedure for SHOIQ}},
author = {Horrocks, Ian and Sattler, Ulrike},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2005},
pages = {448-453},
url = {https://mlanthology.org/ijcai/2005/horrocks2005ijcai-tableaux/}
}