AAAI Publications, Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
Finite Model Reasoning in Horn Description Logics
Yazmín Ibáñez García, Carsten Lutz, Thomas Schneider

Last modified: 2014-05-04


We study finite model reasoning in expressive Horn description logics (DLs), starting with a reduction of finite ABox consistency to unrestricted ABox consistency. The reduction relies on reversing certain cycles in the TBox, an approach that originated in database theory, was later adapted to the inexpressive DL DL-Lite_F , and is shown here to extend to the expressive Horn DL Horn-ALCFI . The model construction used to establish correctness makes the structure of finite models more explicit than existing approaches to finite model reasoning in expressive DLs that rely on solving systems of inequations over the integers. Since the reduction incurs an exponential blow-up, we then develop a dedicated consequence-based algorithm for finite ABox consistency in Horn-ALCFI that implements the reduction on-the-fly rather than executing it up-front. The algorithm has optimal worst-case complexity and provides a promising foundation for implementations. We next show that our approach can be adapted to finite (positive existential) query answering relative to Horn-ALCFI TBoxes, proving that this problem is EXPTIME-complete in combined complexity and PTIME-complete in data complexity. For finite satisfiability and subsumption, we also show that our techniques extend to Horn-SHIQ.


description logic; finite satisfiability; query answering

Full Text: PDF