In Dean, T. (ed),
Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99).
PostScript (Copyright © 1999
Morgan Kaufmann, IJCAI).
This paper investigates the relationship between resolution and
tableaux proof system for the satisfiability of general
knowledge bases in the description logic 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.
Renate A. Schmidt
FM Group |
Last modified: 27 Apr 2001
Copyright © 1999
Renate A. Schmidt,
School of Computer Science, Man Univ, email@example.com