Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics

TL;DR

This paper investigates uniform interpolation and forgetting in the expressive description logic ALC, providing theoretical characterizations, complexity bounds, and methods for computing and analyzing uniform interpolants and conservative extensions.

Contribution

It offers model-theoretic and automata-theoretic characterizations, complexity bounds, and computational approaches for uniform interpolation and conservative extensions in ALC.

Findings

Model-theoretic characterizations of uniform interpolants

Complexity bounds for deciding existence of interpolants

Methods for computing and bounding size of interpolants

Abstract

We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform inter- polants and their existence in terms of bisimula- tions, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model- theoretic and automata-theoretic methods that, as a by-product, also provides characterizations of and decision procedures for conservative extensions.