From Interpolating Formulas to Separating Languages and Back Again
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918229459337216 |
|---|---|
| author | Kurucz, Agi Wolter, Frank Zakharyaschev, Michael |
| author_facet | Kurucz, Agi Wolter, Frank Zakharyaschev, Michael |
| contents | Traditionally, research on Craig interpolation is concerned with (a) establishing the Craig interpolation property (CIP) of a logic saying that every valid implication in the logic has a Craig interpolant and (b) designing algorithms that extract Craig interpolants from proofs. Logics that lack the CIP are regarded as `pathological' and excluded from consideration. In this chapter, we survey variations and generalisations of traditional Craig interpolation. First, we consider Craig interpolants for implications in logics without the CIP, focusing on the decidability and complexity of deciding their existence. We then generalise interpolation by looking for Craig interpolants in languages L' that can be weaker than the language L of the given implication. Thus, do not only we restrict the non-logical symbols of Craig interpolants but also the logical ones. The resulting L/L'-interpolation problem generalises L/L'-definability, the question whether an L-formula is equivalent to some L'-formula. After that, we move from logical languages to formal languages where interpolation disguises itself as separation: given two disjoint languages in a class C, does there exist a separating language in a smaller class C'? This question is particularly well-studied in the case when the input languages are regular and the separating language is first-order definable. Finally, we connect the different research strands by showing how the decidability of the separation problem for regular languages can be used to prove the decidability of Craig interpolant existence for linear temporal logic LTL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_12805 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | From Interpolating Formulas to Separating Languages and Back Again Kurucz, Agi Wolter, Frank Zakharyaschev, Michael Logic in Computer Science 03B45 (Primary) 03C40 (Secondary) Traditionally, research on Craig interpolation is concerned with (a) establishing the Craig interpolation property (CIP) of a logic saying that every valid implication in the logic has a Craig interpolant and (b) designing algorithms that extract Craig interpolants from proofs. Logics that lack the CIP are regarded as `pathological' and excluded from consideration. In this chapter, we survey variations and generalisations of traditional Craig interpolation. First, we consider Craig interpolants for implications in logics without the CIP, focusing on the decidability and complexity of deciding their existence. We then generalise interpolation by looking for Craig interpolants in languages L' that can be weaker than the language L of the given implication. Thus, do not only we restrict the non-logical symbols of Craig interpolants but also the logical ones. The resulting L/L'-interpolation problem generalises L/L'-definability, the question whether an L-formula is equivalent to some L'-formula. After that, we move from logical languages to formal languages where interpolation disguises itself as separation: given two disjoint languages in a class C, does there exist a separating language in a smaller class C'? This question is particularly well-studied in the case when the input languages are regular and the separating language is first-order definable. Finally, we connect the different research strands by showing how the decidability of the separation problem for regular languages can be used to prove the decidability of Craig interpolant existence for linear temporal logic LTL. |
| title | From Interpolating Formulas to Separating Languages and Back Again |
| topic | Logic in Computer Science 03B45 (Primary) 03C40 (Secondary) |
| url | https://arxiv.org/abs/2508.12805 |