Model comparison games for horn description logics



Jung, JC, Papacchini, F ORCID: 0000-0002-0310-7378, Wolter, F ORCID: 0000-0002-4470-606X and Zakharyaschev, M
(2019) Model comparison games for horn description logics. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2019-6-24 - 2019-6-27, Vancouver.

This is the latest version of this item.

[img] Text
lics19.pdf - Author Accepted Manuscript
Available under License : See the attached licence file.

Download (369kB) | Preview

Abstract

© 2019 IEEE. Horn description logics are syntactically defined fragments of standard description logics that fall within the Horn fragment of first-order logic and for which ontology-mediated query answering is in PTIME for data complexity. They were independently introduced in modal logic to capture the intersection of Horn first-order logic with modal logic. In this paper, we introduce model comparison games for the basic Horn description logic horn ALC (corresponding to the basic Horn modal logic) and use them to obtain an Ehrenfeucht-Frafsse type definability result and a van Benthem style expressive completeness result for horn ALC. We also establish a finite model theory version of the latter. The Ehrenfeucht-Frafsse type definability result is used to show that checking horn ALC indistinguishability of models is ExpTIME-complete, which is in sharp contrast to ALC indistinguishability (i.e., bisimulation equivalence) checkable in PTIME. In addition, we explore the behavior of Horn fragments of more expressive description and modal logics by defining a Horn guarded fragment of first-order logic and introducing model comparison games for it.

Item Type: Conference or Workshop Item (Unspecified)
Additional Information: Full version of LICS'19 paper
Uncontrolled Keywords: cs.LO, cs.LO, F.4.1
Depositing User: Symplectic Admin
Date Deposited: 16 Jan 2020 09:57
Last Modified: 15 Mar 2024 10:06
DOI: 10.1109/LICS.2019.8785658
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3052785

Available Versions of this Item