Twentieth Annual IEEE Symposium on

Logic in Computer Science (LICS 2005)

Paper: Proof-Theoretic Approach to Description-Logic (at LICS 2005)

Authors: Martin Hofmann


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 polynomialtime 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.


    author = 	 {Martin Hofmann},
    title = 	 {Proof-Theoretic Approach to Description-Logic},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {229--237},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}