On the Relation of Resolution and Tableaux Proof Systems for Description Logics
Abstract
This paper investigates the relationship between resolution and\ntableaux proof system for the satisfiability of general\nknowledge bases in the description logic $\\mathcal{ALC}$. We show\nthat resolution proof systems can polynomially simulate their\ntableaux counterpart. Our resolution proof system is based \non a selection refinement and utilises standard redundancy elimination \ncriteria to ensure termination.
Cite
Text
Hustadt and Schmidt. "On the Relation of Resolution and Tableaux Proof Systems for Description Logics." International Joint Conference on Artificial Intelligence, 1999.Markdown
[Hustadt and Schmidt. "On the Relation of Resolution and Tableaux Proof Systems for Description Logics." International Joint Conference on Artificial Intelligence, 1999.](https://mlanthology.org/ijcai/1999/hustadt1999ijcai-relation/)BibTeX
@inproceedings{hustadt1999ijcai-relation,
title = {{On the Relation of Resolution and Tableaux Proof Systems for Description Logics}},
author = {Hustadt, Ullrich and Schmidt, Renate A.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1999},
pages = {110-117},
url = {https://mlanthology.org/ijcai/1999/hustadt1999ijcai-relation/}
}