Computation and Size of Interpolants for Hybrid Modal Logics

TL;DR

This paper investigates the computational complexity and size bounds of interpolants in hybrid modal logics, revealing exponential time bounds for Craig interpolants and undecidability of uniform interpolants.

Contribution

It introduces a new hypermosaic elimination technique to compute Craig interpolants and proves the undecidability of uniform interpolant existence in hybrid modal logics.

Findings

Craig interpolants can be computed in fourfold exponential time if they exist.

Existence of uniform interpolants is undecidable in hybrid modal logics.

Hybrid modal logics lack the Craig Interpolation Property, affecting their computational properties.

Abstract

Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig Interpolation Property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in fourfold exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.