Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computation and Size of Interpolants for Hybrid Modal Logics

Jean Christoph Jung, Jędrzej Kołodziejski, Frank Wolter

TL;DR

It is shown, 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 and that the existence of uniform interpolants is undecidable.

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.

Computation and Size of Interpolants for Hybrid Modal Logics

TL;DR

It is shown, 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 and that the existence of uniform interpolants is undecidable.

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.
Paper Structure (23 sections, 38 theorems, 91 equations)

This paper contains 23 sections, 38 theorems, 91 equations.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Warm-Up: First-Order Separators
  5. Separators in Hybrid Logics
  6. Hypermosaic Elimination
  7. Separator Construction
  8. Separators in Graded Hybrid Logics
  9. Hypermosaic Elimination
  10. Separator Construction with Grades
  11. Separator Size: Lower Bound
  12. Uniform Interpolants
  13. Discussion
  14. Extending the Input Language
  15. Modifying the Notion of Interpolant
  16. ...and 8 more sections

Key Result

Theorem 1

Let $\mathcal{L}\xspace\in \mathsf{HL}\xspace\cup \mathsf{GHL}\xspace$. Given $\varphi,\psi$ in $\mathcal{L}\xspace$ such that a Craig interpolant for $\varphi \rightarrow\psi$ exists, one can construct such an interpolant in fourfold exponential time (and of fourfold exponential size) in the size o

Theorems & Definitions (89)

  • Theorem 1
  • Example 2
  • Theorem 3
  • Theorem 4: DBLP:journals/jsyml/ArecesBM01
  • Theorem 5: DBLP:journals/logcom/BezhanishviliC06DBLP:journals/jsyml/ArecesBM01
  • Definition 6
  • Lemma 7
  • Theorem 8
  • Lemma 8
  • Theorem 9
  • ...and 79 more