Conservative Extensions in Horn Description Logics with Inverse Roles

DOI10.1613/JAIR.1.12182zbMATH Open1445.68205arXiv2011.09858OpenAlexW3029037574MaRDI QIDQ5114785FDOQ5114785

Authors:

Publication date: 26 June 2020

Published in: Journal of Artificial Intelligence Research (Search for Journal in Brave)

Abstract: We investigate the decidability and computational complexity of conservative extensions and the related notions of inseparability and entailment in Horn description logics (DLs) with inverse roles. We consider both query conservative extensions, defined by requiring that the answers to all conjunctive queries are left unchanged, and deductive conservative extensions, which require that the entailed concept inclusions, role inclusions, and functionality assertions do not change. Upper bounds for query conservative extensions are particularly challenging because characterizations in terms of unbounded homomorphisms between universal models, which are the foundation of the standard approach to establishing decidability, fail in the presence of inverse roles. We resort to a characterization that carefully mixes unbounded and bounded homomorphisms and enables a decision procedure that combines tree automata and a mosaic technique. Our main results are that query conservative extensions are 2ExpTime-complete in all DLs between ELI and Horn-ALCHIF and between Horn-ALC and Horn-ALCHIF, and that deductive conservative extensions are 2ExpTime-complete in all DLs between ELI and ELHIF_�ot. The same results hold for inseparability and entailment.

Full work available at URL: https://arxiv.org/abs/2011.09858

Recommendations

• Deciding inseparability and conservative extensions in the description logic
• Conservative Extensions in the Lightweight Description Logic $\mathcal{EL}$
• Conservative extensions in modal logic
• scientific article; zbMATH DE number 1761427
• Inseparability and conservative extensions of description logic ontologies: a survey
• On conservative extensions in logics with infinitary predicates
• Extensions of non-standard inferences to description logics with transitive roles
• scientific article; zbMATH DE number 1354137
• A description logic with transitive and inverse roles and role hierarchies
• Role Conjunctions in Expressive Description Logics

Mathematics Subject Classification ID

Knowledge representation (68T30) Logic in artificial intelligence (68T27)

Cited In (2)

• Conservative Extensions in the Lightweight Description Logic $\mathcal{EL}$
• Deciding inseparability and conservative extensions in the description logic

This page was built for publication: Conservative Extensions in Horn Description Logics with Inverse Roles

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5114785)