Consequence-based reasoning for description logics with disjunction, inverse roles, and nominals

Conference item

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.

Authors: Cucala, D; Cuenca Grau, B; Horrocks, I

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: CEUR Workshop Proceedings
• Host title: 30th International Workshop on Description Logics (DL 2017)
• Journal: 30th International Workshop on Description Logics (DL 2017)
• Publication date: 2017-07-01
• Acceptance date: 2017-06-12
• ISSN: 1613-0073