A Gentzen system for the description logic

The Gentzen systems for a sequent Γ⇒Δ have been proposed in the propositional logic, the predicate calculus and other logics. In this paper, based on the Gentzen system for the predicate calculus, we propose the Gentzen system for a sequent Γ⇒Δ in the description logic, where Γ and Δ are two sets of assertions in ALC: Assertions with universal qualification and inclusion assertions are decomposed as those of universal quantification formulas in the Gentzen system for the predicate calculus. It is proved that the Gentzen system for description logic is sound and complete; but it is not decidable.