Bridging the Gap between Tableau and Consequence-Based Reasoning

ABSTRACT. We present a non-deterministic consequence-based procedure for the description logic ALCHI. Just like the similar style (deterministic) procedures for EL and Horn-SHIQ, our procedure explicitly derives subsumptions between concepts, but due to non-deterministic rules, not all of these subsumptions are consequences of the ontology. Instead, the consequences are only those subsumptions that can be derived regardless of the choices made in the application of the rules. This is similar to tableau-based procedures, for which an ontology is inconsistent if every expansion of the tableau eventually results in a clash. We report on a preliminary experimental evaluation of the procedure using a version of SNOMED~CT with disjunctions, which demonstrates some promising potential.