Computational complexity of terminological reasoning in BACK

摘要

Terminological reasoning is a mode of reasoning all hybrid knowledge representation systems based on KL-ONE rely on. After a short introduction of what terminological reasoning amounts to, it is proven that a complete inference algorithm for the BACK system would be computationally intractable. Interestingly, this result also applies to the KANDOR system, which had been conjectured to realize complete terminological inferences with a tractable algorithm. More generally, together with an earlier paper of Brachman and Levesque it shows that terminological reasoning is intractable for any system using a nontrivial description language. Finally, consequences of this distressing result are briefly discussed.