In Dean, T. (ed),
Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99).
Vol. 1,
Morgan Kaufmann,
110-115.
BiBTeX,
PDF (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
Home |
Publications |
Tools |
FM Group |
School |
Man Univ
Last modified: 29 Dec 17
Copyright © 1999
Renate A. Schmidt,
School of Computer Science, Man Univ, schmidt@cs.man.ac.uk