Finite model reasoning in horn description logics

Ibanez Garcia, Yazmin ORCID: https://orcid.org/0000-0002-1276-904X, Lutz, Carsten and Schneider, Thomas 2014. Finite model reasoning in horn description logics. Presented at: Fourteenth International Conference on Principles of Knowledge Representation and Reasoning, Vienna, Austria, 20-24 July 2014. Published in: Baral, Chitta, De Giacomo, Giuseppe and Eiter, Thomas eds. KR'14: Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning. AAAI Press, pp. 288-297.

Full text not available from this repository.

Abstract

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.

Item Type:	Conference or Workshop Item (Paper)
Date Type:	Publication
Status:	Published
Schools:	Computer Science & Informatics
Publisher:	AAAI Press
ISBN:	9781577356578
Date of First Compliant Deposit:	1 April 2020
Date of Acceptance:	12 January 2014
Last Modified:	07 Nov 2022 09:56
URI:	https://orca.cardiff.ac.uk/id/eprint/130693

Citation Data

Cited 14 times in Scopus. View in Scopus. Powered By Scopus® Data

Actions (repository staff only)

Edit Item