Conservative Extensions in Horn Description Logics with Inverse Roles
  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_\bot. The same results
hold for inseparability and entailment.
