@INPROCEEDINGS{HustadtSchmidt99b,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
MONTH = {August},
YEAR = {1999},
TITLE = {On the Relation of Resolution and Tableaux Proof Systems for Description Logics},
EDITOR = {Dean, T.},
BOOKTITLE = {Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99)},
VOLUME = {1},
PUBLISHER = {Morgan Kaufmann},
PAGES = {110--115},
ISBN = {1-55860-613-0},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/HustadtSchmidt99b.html},
ABSTRACT = {This paper investigates the relationship between resolution and
tableaux proof system for the satisfiability of general
knowledge bases in the description logic $\mathcal{ALC}$. We show
that resolution proof systems can polynomially simulate their
tableaux counterpart. Our resolution proof system is based 
on a selection refinement and utilises standard redundancy elimination 
criteria to ensure termination.},
}