Consequence-based reasoning for description logics with disjunction, inverse roles, and nominals - Cucala, D; Cuenca Grau, B; Horrocks, I (CEUR Workshop Proceedings, 2017)
We present a consequence-based calculus for the SHOI description logic. Known consequence-based reasoning procedures are either restricted to logics without nominals (e.g. SRIQ), or to Horn logics (e.g. Horn-SROIQ). In line with existing approaches, our algorithm uses context structures to assist in the derivation of clauses, which are generated by inference rules such as (hyper)resolution. These rules are applied only locally|that is, between clauses in either the same context or in neighbouring contexts. In order to deal with interactions between nominals, inverse roles, and disjunction, we allow for a restricted form of non-local inference. Our calculus displays worst-case optimal behaviour, and it is amenable to implementation.