Proof-theoretic approach to description-logic

In recent work Baader has shown that a certain description logic with conjunction, existential quantification and with circular definitions has a polynomial time subsumption problem both under an interpretation of circular definitions as greatest fixpoints and under an interpretation as arbitrary fixpoints (introduced by Nebel). This was shown by translating definitions in the description logic ("TBoxes") into a labelled transition system and by reducing subsumption to a question of the existence of certain simulations. In the case of subsumption under the descriptive semantics a new kind of simulation, called synchronised simulation, had to be introduced. In this paper, we also give polynomial-time decision procedures for these logics; this time by devising sound and complete proof systems for them and demonstrating that proof search is polynomial for these systems. We then use the proof-theoretic method to study the hitherto unknown complexity of description logic with universal quantification, conjunction, and GCI axioms. Finally, we extend the proof-theoretic method to negation and thus obtain a decision procedure for the description logic ALC with fixpoints. This last section is only sketched.