On the proof theory of ALC

Abstract

Description Logics is a family of formalisms used to represent knowledge of a domain. In contrast with others knowledge representation systems, Description Logics are equipped with a formal, logic-based semantics. Knowledge representation systems based on description logics provide various inference capabilities that deduce implicit knowledge from the explicitly represented knowledge. In [9] we present a sequent calculus for ALC, a basic Description Logic, called S ALC. The first motivation for developing such system is the extraction of computational content of ALC proofs. The present calculus is an intermediate step towards a Natural Deduction System for ALC. In this paper we present the proof of cut elimination for S ALC.