Computation and Size of Interpolants for Hybrid Modal Logics
2026-02-17 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors studied hybrid modal logics, a type of logic that doesn't have a property called the Craig Interpolation Property (CIP). They developed a new method to actually find something called interpolants in these logics within a specific time limit, which was not known before. However, they also found that deciding if uniform interpolants exist is impossible, which differs from other related logics where these always exist. Their work helps understand how complex these logic problems are and provides practical ways to handle them.
Hybrid modal logicsCraig Interpolation Property (CIP)InterpolantsUniform interpolantsDecidabilityHypermodal logicDescription logicComplexity theoryNon-constructive proofs
Authors
Jean Christoph Jung, Jędrzej Kołodziejski, Frank Wolter
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.