Tableau Systems for SHIO and SHIQ.

Abstract

this paper tableau systems for two expressive DLs, the new DLSHIO and the wellknown [5]. Our main results are the following: firstly, we obtain that satisfiability is ExpTime-complete and can be decided by a tableau algorithm. Secondly, we will see that although these two logics share most of their constructs, they lead to quite di#erent TSs, which demonstrates how the capabilities of our framework can be used to capture di#erent language properties. Thirdly, the succinctness of the proofs demonstrates how our framework simplifies the design of TAs