Type-elimination-based reasoning for the description logic SHIQbs using decision diagrams and disjunctive datalog

TL;DR

This paper introduces a new reasoning method for the description logic SHIQbs that uses type elimination, decision diagrams, and disjunctive Datalog to improve reasoning efficiency and support query extensions.

Contribution

It presents a novel knowledge compilation approach converting SHIQbs knowledge bases into OBDDs and disjunctive Datalog, enabling efficient reasoning and extensions.

Findings

Method is worst-case optimal for combined and data complexity

Supports extensions with ground conjunctive queries

Provides a stepwise reduction from SHIQbs to ALCIb

Abstract

We propose a novel, type-elimination-based method for reasoning in the description logic SHIQbs including DL-safe rules. To this end, we first establish a knowledge compilation method converting the terminological part of an ALCIb knowledge base into an ordered binary decision diagram (OBDD) which represents a canonical model. This OBDD can in turn be transformed into disjunctive Datalog and merged with the assertional part of the knowledge base in order to perform combined reasoning. In order to leverage our technique for full SHIQbs, we provide a stepwise reduction from SHIQbs to ALCIb that preserves satisfiability and entailment of positive and negative ground facts. The proposed technique is shown to be worst case optimal w.r.t. combined and data complexity and easily admits extensions with ground conjunctive queries.