A Proof Theory for Preferential Default Description Logics
Sven Suska · 1994
An extension of Description Logics by weighted default rules is presented, using the semantics of preferential models. Such Preferential Default Description Logics adhere to the principle of exception minimization and are therefore suited for certain tasks in Natural Language Processing. A sound and complete proof theory is given, based on establishing a correspondence between models and sets of default applications (`default spaces'). A Prolog algorithm computing maximal default spaces is described and formally veri ed. As a consequence, the default extension is decidable if the underlying Description Logic is. However, its complexity is exponential, some ideas are proposed to cope with this problem. A tractable subclass is characterized, for which a polynomial algorithm is sketched.