Finite Model Reasoning in Horn-SHIQ.
Yazmín Angélica Ibáñez-García, Carsten Lutz, Thomas Schneider · 2013
Abstract. Finite model reasoning in expressive DLs such as ALCQI and SHIQ requires non-trivial algorithmic approaches that are substantially differerent from algorithms used for reasoning about unrestricted models. In contrast, finite model reasoning in the inexpressive fragment DL-LiteF of ALCQI and SHIQ is algorithmically rather simple: using a TBox completion procedure that reverses certain terminological cycles, one can reduce finite subsumption to unrestricted subsumption. In this paper, we show that this useful technique extends all the way to the popular and much more expressive Horn-SHIQ fragment of SHIQ. 1