On Axiomatic Rejection for the Description Logic ALC

摘要

Traditional proof calculi are mainly studied for formalising the notion of valid inference, i.e., they axiomatise the valid sentences of a logic. In contrast, the notion of invalid inference received less attention. Logical calculi which axiomatise invalid sentences are commonly referred to as complementary calculi or rejection systems. Such calculi provide a proof-theoretic account for deriving non-theorems from other non-theorems and are applied, in particular, for specifying proof systems for nonmonotonic logics. In this paper, we present a sound and complete sequent-type rejection system which axiomatises concept non-subsumption for the description logic ALC. Description logics are well-known knowledge-representation languages formalising ontological reasoning and provide the logical underpinning for semantic-web rear soning. We also discuss the relation of our calculus to a well-known tableau procedure for ALC. Although usually tableau calculi are syntactic variants of standard sequent-type systems, for ALC it turns out that tableaux are rather syntactic counterparts of complementary sequent-type systems. As a consequence, counter models for witnessing concept non-subsumption can easily be obtained from a rejection proof. Finally, by the well-known relationship between ALC and multi-modal logic K, we also obtain a complementary sequent-type system for the latter logic, generalising a similar calculus for standard K as introduced by Goranko.