Computation and Size of Interpolants for Hybrid Modal Logics

Frank Wolter; Jean Christoph Jung; J\k{e}drzej Ko{\l}odziejski

arxiv: 2602.15821 · v2 · pith:3MLYHHBSnew · submitted 2026-02-17 · 💻 cs.LO

Computation and Size of Interpolants for Hybrid Modal Logics

Jean Christoph Jung , J\k{e}drzej Ko{\l}odziejski , Frank Wolter This is my paper

Pith reviewed 2026-05-21 12:10 UTC · model grok-4.3

classification 💻 cs.LO

keywords Craig interpolationhybrid modal logichypermosaic eliminationinterpolant computationuniform interpolantsundecidabilitymodal logicdescription logic

0 comments

The pith

Craig interpolants for many hybrid modal logics can be computed in fourfold exponential time when they exist via hypermosaic elimination.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Hybrid modal logics include nominals that allow naming worlds, yet they fail the Craig Interpolation Property. This paper develops a hypermosaic elimination technique that constructs interpolants by successively removing inconsistent mosaic combinations while preserving satisfiability in the hybrid language. The resulting procedure runs in fourfold exponential time for standard variants such as those with nominals and the down-arrow operator. The same analysis shows that deciding whether a uniform interpolant exists is undecidable, in contrast to ordinary modal and intuitionistic logics. These results matter because interpolants can act as explicit descriptions or as separators between positive and negative examples inside description-logic knowledge bases.

Core claim

Using a hypermosaic elimination technique, Craig interpolants in many standard hybrid modal logics can be computed in fourfold exponential time if they exist. The existence of uniform interpolants is undecidable.

What carries the argument

hypermosaic elimination technique that removes inconsistent mosaics while tracking nominal constraints and hybrid accessibility relations to produce an interpolant of controlled size.

If this is right

Interpolants become algorithmically obtainable in 4EXPTIME for all hybrid logics covered by the technique.
Uniform interpolants cannot be decided for existence, unlike the situation in modal or intuitionistic logic.
Interpolants serve directly as definite descriptions or data separators in description-logic applications.
The method supplies an explicit size bound on the interpolants that are produced.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same elimination idea might be adapted to other logics that lack the Craig Interpolation Property once suitable mosaic representations are identified.
Undecidability of uniform interpolants suggests a fundamental trade-off between expressive power and the ability to compute uniform interpolants in hybrid settings.
Restricted fragments, for example those with bounded modal depth, could restore decidability of uniform interpolants while retaining most hybrid features.

Load-bearing premise

The hypermosaic elimination procedure works without further restrictions on the hybrid modal logics beyond the presence of nominals and standard modal operators.

What would settle it

An explicit hybrid modal formula pair that possesses an interpolant yet requires more than fourfold exponential time under any correct hypermosaic procedure, or a hybrid logic in which uniform interpolant existence is decidable.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a constructive 4-EXPTIME procedure for Craig interpolants in hybrid modal logics via a new hypermosaic elimination technique, plus an undecidability result for uniform interpolants.

read the letter

The main news is a constructive 4-EXPTIME bound for computing Craig interpolants in many standard hybrid modal logics when they exist, using a new hypermosaic elimination method, together with a proof that uniform interpolant existence is undecidable. This stands in contrast to earlier non-constructive results on logics without the Craig property and to the situation in plain modal or intuitionistic logic where uniform interpolants always exist. The approach also ties into practical uses for data separation in description logic knowledge bases, where interpolants can serve as definite descriptions or separators between examples. That part of the motivation is laid out clearly and directly. The hypermosaic technique is presented as the key new ingredient that turns a non-constructive existence result into an explicit algorithm with a size bound. This is the sort of step that can matter for people who need to actually produce the interpolants rather than just know they are there. The paper handles the basic setup for hybrid logics with nominals in a standard way and avoids any obvious circularity or self-referential fitting. The soft spot is the novel elimination procedure itself. Hybrid logics require nominals to designate unique worlds rigidly, and the mosaics have to track that across merges and reductions while respecting accessibility. If the rules for propagating those constraints are incomplete, the output formulas could satisfy local conditions but fail to interpolate globally. The technique is fresh and the abstract gives no small-model checks or independent verification, so this is the part that needs the closest look in review. The concern about nominal handling is real but not obviously fatal on the information available. This is a paper for specialists in modal and hybrid logic or in the complexity of interpolation. A reader who works on description logic applications or on constructive proof methods for logical properties would get direct value from the bounds and the contrast with uniform interpolation. It has enough technical substance and engagement with the literature to deserve a serious referee rather than a desk reject, even if the proofs require careful checking.

Referee Report

2 major / 2 minor

Summary. The paper introduces a hypermosaic elimination technique to compute Craig interpolants for many standard hybrid modal logics (with nominals) in fourfold exponential time when they exist. It also proves that the existence of uniform interpolants is undecidable in these logics, contrasting with modal and intuitionistic logics.

Significance. If the hypermosaic construction is correct, the result supplies the first explicit complexity bound and constructive method for interpolant computation in a class of logics without the Craig interpolation property. This is relevant for applications in description logics where interpolants serve as definite descriptions or data separators. The undecidability result for uniform interpolants is a clear negative result that sharpens the boundary between hybrid and non-hybrid modal logics.

major comments (2)

[§4] §4 (Hypermosaic elimination procedure): The rules for propagating and eliminating nominal constraints across mosaics must be shown to preserve global uniqueness and consistency of nominal interpretations. The skeptic concern is valid here: if a nominal can be assigned to different worlds in merged mosaics without an explicit global consistency check, the output formula may satisfy local modal conditions yet fail to be a valid interpolant for formulas containing nominals. This is load-bearing for the central 4-EXPTIME claim.
[Theorem 5.1] Theorem 5.1 (or the main complexity theorem): The fourfold exponential bound is derived from the size of the hypermosaic space; the proof sketch must explicitly count the number of possible nominal assignments and confirm that the elimination phase does not introduce an extra exponential factor when enforcing rigidity of nominals.

minor comments (2)

[Abstract] The abstract and introduction should list the precise hybrid modal logics covered (e.g., whether the result holds for all extensions with the universal modality or only for the basic hybrid logic K with nominals).
[§3] Notation for mosaics and hypermosaics should be introduced with a small illustrative example early in §3 to clarify how nominals differ from ordinary propositional variables in the construction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. The points raised concern the exposition of correctness and complexity details in the hypermosaic technique. We respond to each major comment below and will incorporate clarifications in the revised manuscript.

read point-by-point responses

Referee: [§4] §4 (Hypermosaic elimination procedure): The rules for propagating and eliminating nominal constraints across mosaics must be shown to preserve global uniqueness and consistency of nominal interpretations. The skeptic concern is valid here: if a nominal can be assigned to different worlds in merged mosaics without an explicit global consistency check, the output formula may satisfy local modal conditions yet fail to be a valid interpolant for formulas containing nominals. This is load-bearing for the central 4-EXPTIME claim.

Authors: We agree that explicit preservation of global uniqueness and consistency for nominals is essential. The hypermosaic construction maintains a single global nominal-to-world map that is updated during each merge and elimination step; local constraints are only applied if they are compatible with this map. To address the concern directly, we will insert a new lemma (Lemma 4.7) in §4 that proves, by induction on the elimination sequence, that every intermediate hypermosaic preserves a rigid, globally unique interpretation for all nominals appearing in the input formulas. The proof will also show that any interpolant extracted from a final consistent hypermosaic satisfies the original formulas under this global assignment. revision: yes
Referee: [Theorem 5.1] Theorem 5.1 (or the main complexity theorem): The fourfold exponential bound is derived from the size of the hypermosaic space; the proof sketch must explicitly count the number of possible nominal assignments and confirm that the elimination phase does not introduce an extra exponential factor when enforcing rigidity of nominals.

Authors: The size of the hypermosaic space is bounded by the product of the number of possible modal types (already 3-EXPTIME) and the number of functions assigning the k nominals (k linear in the input size) to the at most exponentially many worlds per mosaic. This yields an additional single-exponential factor, keeping the overall bound at 4-EXPTIME. The elimination phase itself performs only local consistency checks and map updates that are polynomial in the representation size of each hypermosaic; no re-enumeration of assignments occurs. We will expand the proof of Theorem 5.1 with an explicit counting paragraph and a separate lemma bounding the time for rigidity enforcement. revision: yes

Circularity Check

0 steps flagged

No circularity: novel elimination technique yields independent complexity bound

full rationale

The paper establishes a 4-EXPTIME procedure for Craig interpolants via a new hypermosaic elimination technique applied to standard hybrid modal semantics with nominals. No quoted definitions, equations, or self-citations reduce the claimed existence, size, or complexity result to fitted inputs or prior results by construction. The derivation is self-contained against external modal logic benchmarks, with the undecidability of uniform interpolants likewise resting on a separate reduction that does not loop back to the interpolant computation claim.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the correctness of the new hypermosaic elimination procedure and on standard background properties of hybrid modal logics with nominals.

axioms (1)

domain assumption Hybrid modal logics are defined with nominals and standard modal semantics
Invoked throughout as the setting for which the technique and undecidability hold.

pith-pipeline@v0.9.0 · 5699 in / 1095 out tokens · 64975 ms · 2026-05-21T12:10:13.157567+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We extend the elimination method further by eliminating unrealizable sets of mosaics, called hypermosaics... Theorem 12. For a hypermosaic H, the following are equivalent: H is realizable by an H(σ)-bisimulation; H ∈ Z∗.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The construction of separators proceeds by induction on the number of rounds of the elimination procedure... sep_i(c, t) defined via Sepc-star-types and case distinctions on nominal types.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

50 extracted references · 50 canonical work pages

[1]

Interpolation and model checking,

K. L. McMillan, “Interpolation and model checking,” inHandbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds. Springer, 2018, pp. 421–446. [Online]. Available: https://doi.org/10.1007/978-3-319-10575-8_14

work page doi:10.1007/978-3-319-10575-8_14 2018
[2]

Benedikt, J

M. Benedikt, J. Leblay, B. ten Cate, and E. Tsamoura,Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation, ser. Synthesis Lectures on Data Management. Morgan & Claypool Pub- lishers, 2016

work page 2016
[3]

Projective beth definability and craig interpolation for relational query optimization (material to accompany invited talk),

D. Toman and G. E. Wedell, “Projective beth definability and craig interpolation for relational query optimization (material to accompany invited talk),” inProceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021) associated with the 18th International Conference on Principles of Knowledge Representation and ...

work page 2021
[4]

Logical separability of labeled data examples under ontologies,

J. C. Jung, C. Lutz, H. Pulcini, and F. Wolter, “Logical separability of labeled data examples under ontologies,”Artif. Intell., vol. 313, p. 103785,

work page
[5]

Available: https://doi.org/10.1016/j.artint.2022.103785

[Online]. Available: https://doi.org/10.1016/j.artint.2022.103785

work page doi:10.1016/j.artint.2022.103785 2022
[6]

Universal proof theory: Semi-analytic rules and craig interpolation,

A. A. Tabatabai and R. Jalali, “Universal proof theory: Semi-analytic rules and craig interpolation,”Ann. Pure Appl. Log., vol. 176, no. 1, p. 103509,

work page
[7]

Available: https://doi.org/10.1016/j.apal.2024.103509

[Online]. Available: https://doi.org/10.1016/j.apal.2024.103509

work page doi:10.1016/j.apal.2024.103509 2024
[8]

Modal interpolation via nested sequents,

M. Fitting and R. Kuznets, “Modal interpolation via nested sequents,” Ann. Pure Appl. Log., vol. 166, no. 3, pp. 274–305, 2015. [Online]. Available: https://doi.org/10.1016/j.apal.2014.11.002

work page doi:10.1016/j.apal.2014.11.002 2015
[9]

Beth definability in expressive description logics,

B. ten Cate, E. Franconi, and I. Seylan, “Beth definability in expressive description logics,”J. Artif. Intell. Res., vol. 48, pp. 347–414, 2013

work page 2013
[10]

Interpolation for extended modal languages,

B. ten Cate, “Interpolation for extended modal languages,”J. Symb. Log., vol. 70, no. 1, pp. 223–234, 2005

work page 2005
[11]

Interpolation in knowledge rep- resentation,

J. C. Jung, P. Koopmann, and M. Knorr, “Interpolation in knowledge rep- resentation,”arXiv preprint arXiv:2512.08833, 2025

work page arXiv 2025
[12]

Formal properties of modularisation,

B. Konev, C. Lutz, D. Walther, and F. Wolter, “Formal properties of modularisation,” inModular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization, ser. Lecture Notes in Computer Science, H. Stuckenschmidt, C. Parent, and S. Spaccapietra, 30 Eds. Springer, 2009, vol. 5445, pp. 25–66. [Online]. Available: https://doi.org/10.1007/978-...

work page doi:10.1007/978-3-642-01907-4_3 2009
[13]

Decomposing de- scription logic ontologies,

B. Konev, C. Lutz, D. K. Ponomaryov, and F. Wolter, “Decomposing de- scription logic ontologies,” inProceedings of the 12th International Confer- ence on Principles of Knowledge Representation and Reasoning, KR 2010. AAAI Press, 2010

work page 2010
[14]

Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions,

A. Artale, J. C. Jung, A. Mazzullo, A. Ozaki, and F. Wolter, “Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions,”ACM Trans. Comput. Log., vol. 24, no. 4, pp. 34:1–34:51, 2023. [Online]. Available: https://doi.org/10.1145/3597301

work page doi:10.1145/3597301 2023
[15]

An investigation of definability in ontology alignment,

D. Geleta, T. R. Payne, and V. Tamma, “An investigation of definability in ontology alignment,” inKnowledge Engineering and Knowledge Management - 20th International Conference, EKAW 2016, Bologna, Italy, November 19-23, 2016, Proceedings, ser. Lecture Notes in Computer Science, E. Blomqvist, P. Ciancarini, F. Poggi, and F. Vitali, Eds., vol. 10024, 2016,...

work page doi:10.1007/978-3-319-49004-5_17 2016
[16]

On free description logics with definite descriptions,

A. Artale, A. Mazzullo, A. Ozaki, and F. Wolter, “On free description logics with definite descriptions,” inProceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, 2021, pp. 63–73. [Online]. Available: https://doi.org/10.24963/kr.2021/7

work page doi:10.24963/kr.2021/7 2021
[17]

Graded modal logic and counting bisimulation

M. Otto, “Graded modal logic and counting bisimula- tion,”CoRR, vol. abs/1910.00039, 2019. [Online]. Available: http://arxiv.org/abs/1910.00039

work page arXiv 1910
[18]

A note on graded modal logic,

M. de Rijke, “A note on graded modal logic,”Stud Log- ica, vol. 64, no. 2, pp. 271–283, 2000. [Online]. Available: https://doi.org/10.1023/A:1005245900406

work page doi:10.1023/a:1005245900406 2000
[19]

A road-map on complexity for hybrid logics,

C. Areces, P. Blackburn, and M. Marx, “A road-map on complexity for hybrid logics,” inProceedings of the 8th Annual Conference of the European Association for Computer Science Logic, CSL 1999. Springer, 1999, pp. 307–321. [Online]. Available: https://doi.org/10.1007/3-540-48168-0_22

work page doi:10.1007/3-540-48168-0_22 1999
[20]

The complexity of reasoning with cardinality restrictions and nominals in expressive description logics,

S. Tobies, “The complexity of reasoning with cardinality restrictions and nominals in expressive description logics,”J. Artif. Intell. Res., vol. 12, pp. 199–217, 2000. [Online]. Available: https://doi.org/10.1613/jair.705

work page doi:10.1613/jair.705 2000
[21]

Integrating description logics and action formalisms for reasoning about web services,

F. Baader, M. Milicic, C. Lutz, U. Sattler, and F. Wolter, “Integrating description logics and action formalisms for reasoning about web services,” Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, LTCS-Report LTCS-05-02, 2005, see http://lat.inf.tu-dresden.de/research/reports.html. 31

work page 2005
[22]

Interpolation in modal logic,

M. Marx, “Interpolation in modal logic,” inProceedings of the 7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998. Springer, 1998, pp. 154–163. [Online]. Available: https://doi.org/10.1007/3-540-49253-4_13

work page doi:10.1007/3-540-49253-4_13 1998
[23]

From interpolating formulas to separating languages and back again,

A. Kurucz, F. Wolter, and M. Zakharyaschev, “From interpolating formulas to separating languages and back again,”CoRR, vol. abs/2508.12805,

work page arXiv
[24]

From interpolating formulas to separating languages and back again,

[Online]. Available: https://doi.org/10.48550/arXiv.2508.12805

work page doi:10.48550/arxiv.2508.12805
[25]

Effective interpolation and preservation in guarded logics,

M. Benedikt, B. ten Cate, and M. Vanden Boom, “Effective interpolation and preservation in guarded logics,”ACM Trans. Comput. Log., vol. 17, no. 2, pp. 8:1–8:46, 2016

work page 2016
[26]

Six proofs of interpolation for the modal logic k,

N. Bezhanishvili, B. t. Cate, and R. Iemhoff, “Six proofs of interpolation for the modal logic k,”arXiv preprint arXiv:2510.16398, 2025

work page arXiv 2025
[27]

In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

J. C. Jung and F. Wolter, “Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments,” in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. IEEE, 2021, pp. 1–14. [Online]. Available: https://doi.org/10.1109/LICS52264.2021.9470585

work page doi:10.1109/lics52264.2021.9470585 2021
[28]

Deciding the existence of interpolants and definitions in first-order modal logic,

A. Kurucz, F. Wolter, and M. Zakharyaschev, “Deciding the existence of interpolants and definitions in first-order modal logic,”Log. Methods Comput. Sci., vol. 21, no. 4, 2025. [Online]. Available: https://doi.org/10.46298/lmcs-21(4:6)2025

work page doi:10.46298/lmcs-21(4:6)2025 2025
[29]

Computation of interpolants for description logic concepts in hard cases,

J. C. Jung, J. Kołodziejski, and F. Wolter, “Computation of interpolants for description logic concepts in hard cases,” inProc. of DL 2025, 2025

work page 2025
[30]

FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions,

Y. Zhao and R. A. Schmidt, “FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions,” inAutomated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, ser. Lecture Notes in Computer Science, vol. 11716. Springer, 2019, pp. 568–579. [Online]. A...

work page doi:10.1007/978-3-030-29436-6_34 2019
[31]

LETHE:forgettinganduniforminterpolationforexpressive description logics,

P.Koopmann, “LETHE:forgettinganduniforminterpolationforexpressive description logics,”Künstliche Intell., vol. 34, no. 3, pp. 381–387, 2020. [Online]. Available: https://doi.org/10.1007/s13218-020-00655-w

work page doi:10.1007/s13218-020-00655-w 2020
[32]

On an interpretation of second order quantification in first order intuitionistic propositional logic,

A. M. Pitts, “On an interpretation of second order quantification in first order intuitionistic propositional logic,”J. Symb. Log., vol. 57, no. 1, pp. 33–52, 1992. [Online]. Available: https://doi.org/10.2307/2275175

work page doi:10.2307/2275175 1992
[33]

Uniform interpolation and layered bisimulation,

A. Visseret al., “Uniform interpolation and layered bisimulation,” in Gödel’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy. Association for Symbolic Logic, 1996, pp. 139–164. 32

work page 1996
[34]

Definitorially complete description logics,

B. ten Cate, W. Conradie, M. Marx, and Y. Venema, “Definitorially complete description logics,” inProceedings of the 10th International Conference on Principles of Knowledge Representation and Reason- ing, KR 2006. AAAI Press, 2006, pp. 79–89. [Online]. Available: http://www.aaai.org/Library/KR/2006/kr06-011.php

work page 2006
[35]

Constructive interpolation in hybrid logic,

P. Blackburn and M. Marx, “Constructive interpolation in hybrid logic,” J. Symb. Log., vol. 68, no. 2, pp. 463–480, 2003. [Online]. Available: https://doi.org/10.2178/jsl/1052669059

work page doi:10.2178/jsl/1052669059 2003
[36]

Transfer results for hybrid logic. part I: the case without satisfaction operators,

N. Bezhanishvili and B. ten Cate, “Transfer results for hybrid logic. part I: the case without satisfaction operators,”J. Log. Comput., vol. 16, no. 2, pp. 177–197, 2006. [Online]. Available: https://doi.org/10.1093/logcom/exi056

work page doi:10.1093/logcom/exi056 2006
[37]

Hybrid logics: Characterization, interpolation and complexity,

C. Areces, P. Blackburn, and M. Marx, “Hybrid logics: Characterization, interpolation and complexity,”J. Symb. Log., vol. 66, no. 3, pp. 977–1010,

work page
[38]

Available: https://doi.org/10.2307/2695090

[Online]. Available: https://doi.org/10.2307/2695090

work page doi:10.2307/2695090
[39]

Hybrid logics,

C. Areces and B. ten Cate, “Hybrid logics,” inHandbook of Modal Logic. Elsevier, 2007, vol. 3, pp. 821–868

work page 2007
[40]

Goldman: The symplectic nature of fundamental groups of surfaces, Advances in Math

H. Friedman, “The complexity of explicit definitions,”Advances in Mathematics, vol. 20, no. 1, pp. 18–29, 1976. [Online]. Available: https://www.sciencedirect.com/science/article/pii/0001870876901675

work page arXiv 1976
[41]

Baader, I

F. Baader, I. Horrocks, C. Lutz, and U. Sattler,An Introduction to De- scription Logic. Cambridge University Press, 2017

work page 2017
[42]

Uniform interpolation, automata and the modalµ-calculus,

G. D’Agostino and M. Hollenberg, “Uniform interpolation, automata and the modalµ-calculus,” inProceedings of the 1st Workshop on Advances in Modal Logic, AiML-1. CSLI Publications, 1996, pp. 73–84

work page 1996
[43]

Ebbinghaus and J

H. Ebbinghaus and J. Flum,Finite model theory, ser. Perspectives in Math- ematical Logic. Springer, 1995

work page 1995
[44]

Baader, Diego

Franz. Baader, Diego. Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F.. Patel-Schneider, Eds.,The Description Logic Handbook: The- ory, Implementation, and Applications. Cambridge University Press, 2003

work page 2003
[45]

The interpolant existence problem for weak K4 and difference logic,

A. Kurucz, F. Wolter, and M. Zakharyaschev, “The interpolant existence problem for weak K4 and difference logic,” inAdvances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024, A. Ciabattoni, D. Gabelaia, and I. Sedlár, Eds. College Publications, 2024, pp. 465–484

work page 2024
[46]

Separation and definability in fragments of two-variable first-order logic with counting,

L. Kuijer, T. Tan, F. Wolter, and M. Zakharyaschev, “Separation and definability in fragments of two-variable first-order logic with counting,” in 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025. IEEE, 2025, pp. 329–343. [Online]. Available: https://doi.org/10.1109/LICS65433.2025.00032 33

work page doi:10.1109/lics65433.2025.00032 2025
[47]

The convenience of tilings,

P. van Emde Boas, “The convenience of tilings,” inComplexity, Logic, and Recursion Theory, 1997, pp. 331–363. 34 A Proofs for Section 3 Lemma 9.The following conditions are equivalent for allm: •m 1 ∧case(c 1),m 2 ∧case(c 2)are jointlyH(σ)-consistent; •m∈ Y ∗. Proof.Assumem= (m 1,m 2)andM 1, w1 ∼H,σ M2, w2 withM i, wi |=m i ∧ case(ci), fori= 1,2. We show ...

work page 1997
[48]

, λ×|Type|}and a weakR-counting function with codomain{0,

Moreover, if either condition holds forH ′,m, then they admit anR- counting function with codomain{0, . . . , λ×|Type|}and a weakR-counting function with codomain{0, . . . , λ}. Proof.We show (1). Only the right-to-left implication is nontrivial. Assume Ris a weakR-counting function form, H ′. We first obtain a weakR-counting functionR ′ bounded byλform, ...

work page
[49]

there is a uniform FO(σ)-interpolant forφS inH

work page
[50]

there is a uniformH(σ)-interpolant forφS in FO. (Observe that (2)⇒(3) always holds.) To constructφS, regard the tilest∈ T as propositional variables and letσcontainT, the symbolsS, E,minintroduced in the paper, propositional variablesleft,right,top,bottom, and binary relations F, Rx, Ry. Ewill again allow us to access the nodes in a finite linear order.Fw...

work page

[1] [1]

Interpolation and model checking,

K. L. McMillan, “Interpolation and model checking,” inHandbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds. Springer, 2018, pp. 421–446. [Online]. Available: https://doi.org/10.1007/978-3-319-10575-8_14

work page doi:10.1007/978-3-319-10575-8_14 2018

[2] [2]

Benedikt, J

M. Benedikt, J. Leblay, B. ten Cate, and E. Tsamoura,Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation, ser. Synthesis Lectures on Data Management. Morgan & Claypool Pub- lishers, 2016

work page 2016

[3] [3]

Projective beth definability and craig interpolation for relational query optimization (material to accompany invited talk),

D. Toman and G. E. Wedell, “Projective beth definability and craig interpolation for relational query optimization (material to accompany invited talk),” inProceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021) associated with the 18th International Conference on Principles of Knowledge Representation and ...

work page 2021

[4] [4]

Logical separability of labeled data examples under ontologies,

J. C. Jung, C. Lutz, H. Pulcini, and F. Wolter, “Logical separability of labeled data examples under ontologies,”Artif. Intell., vol. 313, p. 103785,

work page

[5] [5]

Available: https://doi.org/10.1016/j.artint.2022.103785

[Online]. Available: https://doi.org/10.1016/j.artint.2022.103785

work page doi:10.1016/j.artint.2022.103785 2022

[6] [6]

Universal proof theory: Semi-analytic rules and craig interpolation,

A. A. Tabatabai and R. Jalali, “Universal proof theory: Semi-analytic rules and craig interpolation,”Ann. Pure Appl. Log., vol. 176, no. 1, p. 103509,

work page

[7] [7]

Available: https://doi.org/10.1016/j.apal.2024.103509

[Online]. Available: https://doi.org/10.1016/j.apal.2024.103509

work page doi:10.1016/j.apal.2024.103509 2024

[8] [8]

Modal interpolation via nested sequents,

M. Fitting and R. Kuznets, “Modal interpolation via nested sequents,” Ann. Pure Appl. Log., vol. 166, no. 3, pp. 274–305, 2015. [Online]. Available: https://doi.org/10.1016/j.apal.2014.11.002

work page doi:10.1016/j.apal.2014.11.002 2015

[9] [9]

Beth definability in expressive description logics,

B. ten Cate, E. Franconi, and I. Seylan, “Beth definability in expressive description logics,”J. Artif. Intell. Res., vol. 48, pp. 347–414, 2013

work page 2013

[10] [10]

Interpolation for extended modal languages,

B. ten Cate, “Interpolation for extended modal languages,”J. Symb. Log., vol. 70, no. 1, pp. 223–234, 2005

work page 2005

[11] [11]

Interpolation in knowledge rep- resentation,

J. C. Jung, P. Koopmann, and M. Knorr, “Interpolation in knowledge rep- resentation,”arXiv preprint arXiv:2512.08833, 2025

work page arXiv 2025

[12] [12]

Formal properties of modularisation,

B. Konev, C. Lutz, D. Walther, and F. Wolter, “Formal properties of modularisation,” inModular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization, ser. Lecture Notes in Computer Science, H. Stuckenschmidt, C. Parent, and S. Spaccapietra, 30 Eds. Springer, 2009, vol. 5445, pp. 25–66. [Online]. Available: https://doi.org/10.1007/978-...

work page doi:10.1007/978-3-642-01907-4_3 2009

[13] [13]

Decomposing de- scription logic ontologies,

B. Konev, C. Lutz, D. K. Ponomaryov, and F. Wolter, “Decomposing de- scription logic ontologies,” inProceedings of the 12th International Confer- ence on Principles of Knowledge Representation and Reasoning, KR 2010. AAAI Press, 2010

work page 2010

[14] [14]

Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions,

A. Artale, J. C. Jung, A. Mazzullo, A. Ozaki, and F. Wolter, “Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions,”ACM Trans. Comput. Log., vol. 24, no. 4, pp. 34:1–34:51, 2023. [Online]. Available: https://doi.org/10.1145/3597301

work page doi:10.1145/3597301 2023

[15] [15]

An investigation of definability in ontology alignment,

D. Geleta, T. R. Payne, and V. Tamma, “An investigation of definability in ontology alignment,” inKnowledge Engineering and Knowledge Management - 20th International Conference, EKAW 2016, Bologna, Italy, November 19-23, 2016, Proceedings, ser. Lecture Notes in Computer Science, E. Blomqvist, P. Ciancarini, F. Poggi, and F. Vitali, Eds., vol. 10024, 2016,...

work page doi:10.1007/978-3-319-49004-5_17 2016

[16] [16]

On free description logics with definite descriptions,

A. Artale, A. Mazzullo, A. Ozaki, and F. Wolter, “On free description logics with definite descriptions,” inProceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, 2021, pp. 63–73. [Online]. Available: https://doi.org/10.24963/kr.2021/7

work page doi:10.24963/kr.2021/7 2021

[17] [17]

Graded modal logic and counting bisimulation

M. Otto, “Graded modal logic and counting bisimula- tion,”CoRR, vol. abs/1910.00039, 2019. [Online]. Available: http://arxiv.org/abs/1910.00039

work page arXiv 1910

[18] [18]

A note on graded modal logic,

M. de Rijke, “A note on graded modal logic,”Stud Log- ica, vol. 64, no. 2, pp. 271–283, 2000. [Online]. Available: https://doi.org/10.1023/A:1005245900406

work page doi:10.1023/a:1005245900406 2000

[19] [19]

A road-map on complexity for hybrid logics,

C. Areces, P. Blackburn, and M. Marx, “A road-map on complexity for hybrid logics,” inProceedings of the 8th Annual Conference of the European Association for Computer Science Logic, CSL 1999. Springer, 1999, pp. 307–321. [Online]. Available: https://doi.org/10.1007/3-540-48168-0_22

work page doi:10.1007/3-540-48168-0_22 1999

[20] [20]

The complexity of reasoning with cardinality restrictions and nominals in expressive description logics,

S. Tobies, “The complexity of reasoning with cardinality restrictions and nominals in expressive description logics,”J. Artif. Intell. Res., vol. 12, pp. 199–217, 2000. [Online]. Available: https://doi.org/10.1613/jair.705

work page doi:10.1613/jair.705 2000

[21] [21]

Integrating description logics and action formalisms for reasoning about web services,

F. Baader, M. Milicic, C. Lutz, U. Sattler, and F. Wolter, “Integrating description logics and action formalisms for reasoning about web services,” Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, LTCS-Report LTCS-05-02, 2005, see http://lat.inf.tu-dresden.de/research/reports.html. 31

work page 2005

[22] [22]

Interpolation in modal logic,

M. Marx, “Interpolation in modal logic,” inProceedings of the 7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998. Springer, 1998, pp. 154–163. [Online]. Available: https://doi.org/10.1007/3-540-49253-4_13

work page doi:10.1007/3-540-49253-4_13 1998

[23] [23]

From interpolating formulas to separating languages and back again,

A. Kurucz, F. Wolter, and M. Zakharyaschev, “From interpolating formulas to separating languages and back again,”CoRR, vol. abs/2508.12805,

work page arXiv

[24] [24]

From interpolating formulas to separating languages and back again,

[Online]. Available: https://doi.org/10.48550/arXiv.2508.12805

work page doi:10.48550/arxiv.2508.12805

[25] [25]

Effective interpolation and preservation in guarded logics,

M. Benedikt, B. ten Cate, and M. Vanden Boom, “Effective interpolation and preservation in guarded logics,”ACM Trans. Comput. Log., vol. 17, no. 2, pp. 8:1–8:46, 2016

work page 2016

[26] [26]

Six proofs of interpolation for the modal logic k,

N. Bezhanishvili, B. t. Cate, and R. Iemhoff, “Six proofs of interpolation for the modal logic k,”arXiv preprint arXiv:2510.16398, 2025

work page arXiv 2025

[27] [27]

In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

J. C. Jung and F. Wolter, “Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments,” in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. IEEE, 2021, pp. 1–14. [Online]. Available: https://doi.org/10.1109/LICS52264.2021.9470585

work page doi:10.1109/lics52264.2021.9470585 2021

[28] [28]

Deciding the existence of interpolants and definitions in first-order modal logic,

A. Kurucz, F. Wolter, and M. Zakharyaschev, “Deciding the existence of interpolants and definitions in first-order modal logic,”Log. Methods Comput. Sci., vol. 21, no. 4, 2025. [Online]. Available: https://doi.org/10.46298/lmcs-21(4:6)2025

work page doi:10.46298/lmcs-21(4:6)2025 2025

[29] [29]

Computation of interpolants for description logic concepts in hard cases,

J. C. Jung, J. Kołodziejski, and F. Wolter, “Computation of interpolants for description logic concepts in hard cases,” inProc. of DL 2025, 2025

work page 2025

[30] [30]

FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions,

Y. Zhao and R. A. Schmidt, “FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions,” inAutomated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, ser. Lecture Notes in Computer Science, vol. 11716. Springer, 2019, pp. 568–579. [Online]. A...

work page doi:10.1007/978-3-030-29436-6_34 2019

[31] [31]

LETHE:forgettinganduniforminterpolationforexpressive description logics,

P.Koopmann, “LETHE:forgettinganduniforminterpolationforexpressive description logics,”Künstliche Intell., vol. 34, no. 3, pp. 381–387, 2020. [Online]. Available: https://doi.org/10.1007/s13218-020-00655-w

work page doi:10.1007/s13218-020-00655-w 2020

[32] [32]

On an interpretation of second order quantification in first order intuitionistic propositional logic,

A. M. Pitts, “On an interpretation of second order quantification in first order intuitionistic propositional logic,”J. Symb. Log., vol. 57, no. 1, pp. 33–52, 1992. [Online]. Available: https://doi.org/10.2307/2275175

work page doi:10.2307/2275175 1992

[33] [33]

Uniform interpolation and layered bisimulation,

A. Visseret al., “Uniform interpolation and layered bisimulation,” in Gödel’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy. Association for Symbolic Logic, 1996, pp. 139–164. 32

work page 1996

[34] [34]

Definitorially complete description logics,

B. ten Cate, W. Conradie, M. Marx, and Y. Venema, “Definitorially complete description logics,” inProceedings of the 10th International Conference on Principles of Knowledge Representation and Reason- ing, KR 2006. AAAI Press, 2006, pp. 79–89. [Online]. Available: http://www.aaai.org/Library/KR/2006/kr06-011.php

work page 2006

[35] [35]

Constructive interpolation in hybrid logic,

P. Blackburn and M. Marx, “Constructive interpolation in hybrid logic,” J. Symb. Log., vol. 68, no. 2, pp. 463–480, 2003. [Online]. Available: https://doi.org/10.2178/jsl/1052669059

work page doi:10.2178/jsl/1052669059 2003

[36] [36]

Transfer results for hybrid logic. part I: the case without satisfaction operators,

N. Bezhanishvili and B. ten Cate, “Transfer results for hybrid logic. part I: the case without satisfaction operators,”J. Log. Comput., vol. 16, no. 2, pp. 177–197, 2006. [Online]. Available: https://doi.org/10.1093/logcom/exi056

work page doi:10.1093/logcom/exi056 2006

[37] [37]

Hybrid logics: Characterization, interpolation and complexity,

C. Areces, P. Blackburn, and M. Marx, “Hybrid logics: Characterization, interpolation and complexity,”J. Symb. Log., vol. 66, no. 3, pp. 977–1010,

work page

[38] [38]

Available: https://doi.org/10.2307/2695090

[Online]. Available: https://doi.org/10.2307/2695090

work page doi:10.2307/2695090

[39] [39]

Hybrid logics,

C. Areces and B. ten Cate, “Hybrid logics,” inHandbook of Modal Logic. Elsevier, 2007, vol. 3, pp. 821–868

work page 2007

[40] [40]

Goldman: The symplectic nature of fundamental groups of surfaces, Advances in Math

H. Friedman, “The complexity of explicit definitions,”Advances in Mathematics, vol. 20, no. 1, pp. 18–29, 1976. [Online]. Available: https://www.sciencedirect.com/science/article/pii/0001870876901675

work page arXiv 1976

[41] [41]

Baader, I

F. Baader, I. Horrocks, C. Lutz, and U. Sattler,An Introduction to De- scription Logic. Cambridge University Press, 2017

work page 2017

[42] [42]

Uniform interpolation, automata and the modalµ-calculus,

G. D’Agostino and M. Hollenberg, “Uniform interpolation, automata and the modalµ-calculus,” inProceedings of the 1st Workshop on Advances in Modal Logic, AiML-1. CSLI Publications, 1996, pp. 73–84

work page 1996

[43] [43]

Ebbinghaus and J

H. Ebbinghaus and J. Flum,Finite model theory, ser. Perspectives in Math- ematical Logic. Springer, 1995

work page 1995

[44] [44]

Baader, Diego

Franz. Baader, Diego. Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F.. Patel-Schneider, Eds.,The Description Logic Handbook: The- ory, Implementation, and Applications. Cambridge University Press, 2003

work page 2003

[45] [45]

The interpolant existence problem for weak K4 and difference logic,

A. Kurucz, F. Wolter, and M. Zakharyaschev, “The interpolant existence problem for weak K4 and difference logic,” inAdvances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024, A. Ciabattoni, D. Gabelaia, and I. Sedlár, Eds. College Publications, 2024, pp. 465–484

work page 2024

[46] [46]

Separation and definability in fragments of two-variable first-order logic with counting,

L. Kuijer, T. Tan, F. Wolter, and M. Zakharyaschev, “Separation and definability in fragments of two-variable first-order logic with counting,” in 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025. IEEE, 2025, pp. 329–343. [Online]. Available: https://doi.org/10.1109/LICS65433.2025.00032 33

work page doi:10.1109/lics65433.2025.00032 2025

[47] [47]

The convenience of tilings,

P. van Emde Boas, “The convenience of tilings,” inComplexity, Logic, and Recursion Theory, 1997, pp. 331–363. 34 A Proofs for Section 3 Lemma 9.The following conditions are equivalent for allm: •m 1 ∧case(c 1),m 2 ∧case(c 2)are jointlyH(σ)-consistent; •m∈ Y ∗. Proof.Assumem= (m 1,m 2)andM 1, w1 ∼H,σ M2, w2 withM i, wi |=m i ∧ case(ci), fori= 1,2. We show ...

work page 1997

[48] [48]

, λ×|Type|}and a weakR-counting function with codomain{0,

Moreover, if either condition holds forH ′,m, then they admit anR- counting function with codomain{0, . . . , λ×|Type|}and a weakR-counting function with codomain{0, . . . , λ}. Proof.We show (1). Only the right-to-left implication is nontrivial. Assume Ris a weakR-counting function form, H ′. We first obtain a weakR-counting functionR ′ bounded byλform, ...

work page

[49] [49]

there is a uniform FO(σ)-interpolant forφS inH

work page

[50] [50]

there is a uniformH(σ)-interpolant forφS in FO. (Observe that (2)⇒(3) always holds.) To constructφS, regard the tilest∈ T as propositional variables and letσcontainT, the symbolsS, E,minintroduced in the paper, propositional variablesleft,right,top,bottom, and binary relations F, Rx, Ry. Ewill again allow us to access the nodes in a finite linear order.Fw...

work page