Subsumption in KL-One is Undecidable

Abstract

It is shown that in the frame-based language KL-ONE it is undecidable, whether one concept is subsumed by another concept. The concept forming operators which are sufficient for this result are: conjunction, value restriction, role restriction, the operator ‘SOME’, and role value maps using only ‘=’. In particular, number restrictions are not used. This shows that there is a basic difference between feature terms and KL-ONE, since the complexity of subsumption switches from co-NP-complete to undecidable, if the restriction is dropped that roles are functional.