# Logic in Computer Science (cs.LO)

• We define a simple dependent type theory and prove that its well-formed types correspond exactly to finite inverse categories.
• We present an ongoing implementation of a \ke\space based reasoner for a decidable fragment of stratified elementary set theory expressing the description logic $\dlssx$ (shortly $\shdlssx$). The reasoner checks the consistency of $\shdlssx$-knowledge bases (KBs) represented in set-theoretic terms. It is implemented in \textsfC++ and supports $\shdlssx$-KBs serialized in the OWL/XML format.To the best of our knowledge, this is the first attempt to implement a reasoner for the consistency checking of a description logic represented via a fragment of set theory that can also classify standard OWL ontologies.