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

• Type: Conference
• Year: 2005
• Where: LICS
• Authors: Martin Hofmann
• Keywords: Certain Description Logic, Computer Science, Description Logic, LICS 2005, Polynomial Time Subsumption