@incollection(AkbarTabatabai2022,
 author       = {A.~{Akbar Tabatabai} and R.~Iemhoff and R.~Jalali},
 year         = {2022},
 title        = {Uniform Lyndon interpolation for intuitionistic monotone modal logic},
 editor       = {D.~Fern{\'a}ndez-Duque and A.~Palmigiano and S.~Pinchinat},
 booktitle    = {Advances in Modal Logic},
 volume       = {14},
 publisher    = {Colledge Publications},
 pages        = {77--96},
 url          = {http://www.aiml.net/volumes/volume14/09-AkbarTabatabai-Iemhoff-Jalali.pdf},
)
@article(AkbarTabatabai2024,
 author       = {A.~{Akbar Tabatabai} and R.~Iemhoff and R.~Jalali},
 year         = {2024},
 title        = {Uniform lyndon interpolation for basic non-normal modal and conditional logics},
 journal      = {Journal of Logic and Computation},
 doi          = {10.1093/logcom/exae057},
)
@book(Benthem1991,
 author       = {J.~van Benthem},
 year         = {1991},
 title        = {The Logic of Time},
 edition      = {2},
 series       = {Synthese Library},
 volume       = {156},
 publisher    = {Reidel},
 address      = {Dordrecht},
)
@misc(Bezhanishvili2025,
 author       = {N.~Bezhanishvili and B.~ten Cate and R.~Iemhoff},
 year         = {2025},
 title        = {Six Proofs of Interpolation for the Modal Logic $\mathbf{K}$},
 doi          = {10.48550/ARXIV.2510.16398},
)
@article(Bilkova2007,
 author       = {M.~B\'{i}lkov\'{a}},
 year         = {2007},
 title        = {Uniform Interpolation and Propositional Quantifiers in Modal Logics},
 journal      = {Studia Logica},
 volume       = {85},
 pages        = {1--31},
 doi          = {10.1007/s11225-007-9021-5},
)
@phdthesis(Blackburn1990,
 author       = {P.~Blackburn},
 year         = {1990},
 title        = {Nominal Tense Logic and Other Sorted Intensional Frameworks},
 school       = {Centre for Cognitive Science, University of Edinburgh},
)
@book(BdRV2001,
 author       = {P.~Blackburn and M.~de~Rijke and Y.~Venema},
 year         = {2001},
 title        = {Modal Logic},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
)
@incollection(Blackburn2023,
 author       = {P.~Blackburn and T.~Bra{\"u}ner and J.~L. Kofod},
 year         = {2023},
 title        = {An Axiom System for Basic Hybrid Logic with Propositional Quantifiers},
 booktitle    = {Logic, Language, Information, and Computation},
 publisher    = {Springer Nature Switzerland},
 pages        = {118--134},
 doi          = {10.1007/978-3-031-39784-4_8},
)
@incollection(Blackburn2020,
 author       = {P.~R. Blackburn and T.~Bra{\"u}ner and J.~L. Kofod},
 year         = {2020},
 title        = {Remarks on Hybrid Modal Logic with Propositional Quantfiers},
 editor       = {P.~Hasle and D.~Jakobsen and P.~{\O}hrstr{\o}m},
 booktitle    = {The Metaphysics of Time: Themes from Prior},
 series       = {Logic and Philosophy of Time},
 volume       = {4},
 publisher    = {Aalborg Universitetsforlag},
 pages        = {401--426},
)
@incollection(Burgess1984,
 author       = {J.~P. Burgess},
 year         = {1984},
 title        = {Basic Tense Logic},
 editor       = {D.~Gabbay and F.~Guenthner},
 booktitle    = {Handbook of Philosophical Logic},
 volume       = {II},
 publisher    = {Reidel},
 address      = {Dordrecht},
 pages        = {89--133},
)
@phdthesis(tenCate2005,
 author       = {B.~ten Cate},
 year         = {2005},
 title        = {Model theory for extended modal languages},
 school       = {University of Amsterdam},
 address      = {Institute for Logic, Language and Computation},
)
@article(tenCate2013,
 author       = {B.~ten Cate and E.~Franconi and I.~Seylan},
 year         = {2013},
 title        = {Beth Definability in Expressive Description Logics},
 journal      = {Journal of Artificial Intelligence Research},
 volume       = {48},
 pages        = {347--414},
 doi          = {10.1613/jair.4057},
)
@book(CZ1997,
 author       = {A.~Chagrov and M.~Zakharyaschev},
 year         = {1997},
 title        = {Modal Logic},
 series       = {Oxford Logic Guides},
 volume       = {35},
 publisher    = {Oxford Science Publications},
 address      = {Oxford},
)
@article(DAgostino2008,
 author       = {G.~D'Agostino},
 year         = {2008},
 title        = {Interpolation in non-classical logics},
 journal      = {Synthese},
 volume       = {164},
 number       = {3},
 pages        = {421--435},
 doi          = {10.1007/s11229-008-9359-x},
)
@article(D’Agostino2015,
 author       = {G.~D'Agostino and G.~Lenzi},
 year         = {2015},
 title        = {Bisimulation quantifiers and uniform interpolation for guarded first order logic},
 journal      = {Theoretical Computer Science},
 volume       = {563},
 pages        = {75--85},
 doi          = {10.1016/j.tcs.2014.08.015},
)
@article(DAgostino2006,
 author       = {G.~D'Agostino and G.~Lenzi and T.~French},
 year         = {2006},
 title        = {$\mu$-programs, uniform interpolation and bisimulation quantifiers for modal logics},
 journal      = {Journal of Applied Non-Classical Logics},
 volume       = {16},
 number       = {3-4},
 pages        = {297--309},
 doi          = {10.3166/jancl.16.297-309},
)
@article(Fang2019,
 author       = {L.~Fang and Y.~Liu and H.~van Ditmarsch},
 year         = {2019},
 title        = {Forgetting in multi-agent modal logics},
 journal      = {Artificial Intelligence},
 volume       = {266},
 pages        = {51--80},
 doi          = {10.1016/j.artint.2018.08.003},
)
@inproceedings(Feree2024,
 author       = {H.~F{\'e}r{\'e}e and I.~{van der}~Giessen and S.~{van}~Gool and I.~Shillito},
 year         = {2024},
 title        = {Mechanised Uniform Interpolation for Modal Logics {K}, {GL}, and {iSL}},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer Nature Switzerland},
 pages        = {43--60},
 doi          = {10.1007/978-3-031-63501-4_3},
)
@article(Fine1975,
 author       = {K.~Fine},
 year         = {1975},
 title        = {Normal forms in modal logic.},
 journal      = {Notre Dame Journal of Formal Logic},
 volume       = {16},
 number       = {2},
 pages        = {229--237},
 doi          = {10.1305/ndjfl/1093891703},
)
@phdthesis(French2006,
 author       = {T.~N. French},
 year         = {2006},
 title        = {Bisimulation Quantifiers for Modal Logics},
 school       = {The University of Western Australia},
)
@book(GHR1994,
 author       = {D.~M. Gabbay and I.~M. Hodkinson and M.~Reynolds},
 year         = {1994},
 title        = {Temporal Logic: Mathematical Foundations and Computational Aspects},
 series       = {Oxford Logic Guides},
 volume       = {1},
 publisher    = {Oxford University Press},
)
@article(Ghilardi1995a,
 author       = {S.~Ghilardi and M.~Zawadowski},
 year         = {1995},
 title        = {A sheaf representation and duality for finitely presented {H}eyting algebras},
 journal      = {Journal of Symbolic Logic},
 volume       = {60},
 number       = {3},
 pages        = {911--939},
 doi          = {10.2307/2275765},
)
@article(Ghilardi1995,
 author       = {S.~Ghilardi and M.~Zawadowski},
 year         = {1995},
 title        = {Undefinability of propositional quantifiers in the modal system {S4}},
 journal      = {Studia Logica},
 volume       = {55},
 number       = {2},
 pages        = {259--271},
 doi          = {10.1007/bf01061237},
)
@book(Goldblatt1992,
 author       = {R.~Goldblatt},
 year         = {1992},
 title        = {Logics of Time and Computation},
 edition      = {2},
 publisher    = {CSLI Publications},
)
@book(Harel2000,
 author       = {D.~Harel and D.~Kozen and J.~Tiuryn},
 year         = {2000},
 title        = {Dynamic Logic},
 publisher    = {MIT press},
)
@article(Iemhoff2019,
 author       = {R.~Iemhoff},
 year         = {2019},
 title        = {Uniform interpolation and the existence of sequent calculi},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {170},
 number       = {11},
 pages        = {102711},
 doi          = {10.1016/j.apal.2019.05.008},
)
@phdthesis(Kamp1968,
 author       = {H.~Kamp},
 year         = {1968},
 title        = {Tense Logic and the Theory of Linear Order},
 school       = {University of California},
 address      = {Los Angeles, CA, USA},
)
@article(Kurahashi2020,
 author       = {T.~Kurahashi},
 year         = {2020},
 title        = {Uniform {L}yndon interpolation property in propositional modal logics},
 journal      = {Archive for Mathematical Logic},
 volume       = {59},
 number       = {5-6},
 pages        = {659--678},
 doi          = {10.1007/s00153-020-00713-y},
)
@inproceedings(Lyon2020,
 author       = {T.~Lyon and A.~Tiu and R.~Gor{\'e} and R.~Clouston},
 year         = {2020},
 title        = {{Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents}},
 editor       = {M.~Fern{\'a}ndez and A.~Muscholl},
 booktitle    = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {152},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {28:1--28:16},
 doi          = {10.4230/LIPIcs.CSL.2020.28},
)
@article(Maehara1960,
 author       = {S.~Maehara},
 year         = {1961},
 title        = {Craig no Interpolation Theorem},
 journal      = {Sugaku},
 volume       = {12},
 pages        = {235--237},
 doi          = {10.11429/sugaku1947.12.235},
)
@article(Maruyama2001,
 author       = {A.~Maruyama and S.~Tojo and H.~Ono},
 year         = {2001},
 title        = {Decidability of temporal epistemic logics for multi-agent models},
 journal      = {Proceedings of the ICLP'01 Workshop on Computational Logic in Multi-Agent Systems (CLIMA-01)},
 pages        = {31--40},
)
@book(Mcarthur1976,
 author       = {R.~P. McArthur},
 year         = {1976},
 title        = {Tense Logic},
 publisher    = {Reidel Publishing Company},
 address      = {Dordrecht, Boston},
)
@article(Moss2007,
 author       = {L.~S. Moss},
 year         = {2007},
 title        = {Finte Models Constructed From Canonical Formulas},
 journal      = {Journal of Philosophical Logic},
 volume       = {36},
 number       = {6},
 pages        = {605--640},
 doi          = {10.1007/s10992-007-9052-4},
)
@article(Pitts1992,
 author       = {A.~M. Pitts},
 year         = {1992},
 title        = {On an interpretation of second order quantification in first order intuitionistic propositional logic},
 journal      = {Journal of Symbolic Logic},
 volume       = {57},
 number       = {1},
 pages        = {33--52},
 doi          = {10.2307/2275175},
)
@book(Prior1957,
 author       = {A.~N. Prior},
 year         = {1957},
 title        = {Time and Modality},
 publisher    = {Clarendon Press},
 address      = {Oxford},
)
@book(Prior1967,
 author       = {A.~N. Prior},
 year         = {1967},
 title        = {Past, Present and Future},
 publisher    = {Clarendon Press},
 address      = {Oxford},
)
@book(Prior1968,
 author       = {A.~N. Prior},
 year         = {1968},
 title        = {Papers on Time and Tense},
 publisher    = {Clarendon Press},
 address      = {Oxford},
)
@book(Prior2003,
 author       = {A.~N. Prior},
 year         = {2003},
 title        = {Papers on Time and Tense},
 edition      = {new},
 publisher    = {Oxford University Press},
)
@article(Rautenberg1983,
 author       = {W.~Rautenberg},
 year         = {1983},
 title        = {Modal tableau calculi and interpolation},
 journal      = {Journal of Philosophical Logic},
 volume       = {12},
 number       = {4},
 pages        = {403--423},
 doi          = {10.1007/bf00249258},
)
@inproceedings(Sano2020a,
 author       = {K.~Sano and S.~Yamasaki},
 year         = {2020},
 title        = {Subformula property and {C}raig interpolation theorem of sequent calculi for tense logics},
 editor       = {N.~Olivetti and R.~Verbrugge},
 booktitle    = {Short Papers of Advances in Modal Logic (AiML 2020)},
 pages        = {97--101},
 url          = {https://rinekeverbrugge.nl/wp-content/uploads/2024/09/FinalShortPaperMain-AiML2020.pdf},
)
@article(Shavrukov1993,
 author       = {V.~Y. Shavrukov},
 year         = {1993},
 title        = {Subalgebras of diagonalizable algebras of theories containing arithmetic},
 journal      = {Dissertationes Mathematicae (Rozprawy Matematyczne)},
 volume       = {323},
 pages        = {1--82},
)
@incollection(Visser1996,
 author       = {A.~Visser},
 year         = {1996},
 title        = {Uniform Interpolation and Layered Bisimulation},
 booktitle    = {G{\"o}del'96: Logical foundations of mathematics, computer science and physics---Kurt G{\"o}del's legacy, Brno, Czech Republic, August 1996},
 publisher    = {Spriinger-Verlag},
 address      = {Berlin},
 pages        = {139--164},
 url          = {http://projecteuclid.org/euclid.lnl/1235417019},
)
@misc(Visser1996preprint,
 author       = {A.~Visser},
 year         = {1996},
 title        = {Bisimulations, model descriptions and propositional quantifiers},
 howpublished = {Logic Group Preprint Series, No. 161, Utrecht University10.1006/inco.1997.2627},
 url          = {https://dspace.library.uu.nl/handle/1874/26710},
)
@article(Wolter1997a,
 author       = {F.~Wolter},
 year         = {1997},
 title        = {A Note on the Interpolation Property in Tense Logic},
 journal      = {Journal of Philosophical Logic},
 volume       = {26},
 number       = {5},
 pages        = {545--551},
 doi          = {10.1023/a:1017956722866},
)
@incollection(Zakharyaschev2001,
 author       = {M.~Zakharyaschev and F.~Wolter and A.~Chagrov},
 year         = {2001},
 title        = {Advanced Modal Logic},
 booktitle    = {Handbook of Philosophical Logic},
 volume       = {3},
 publisher    = {Springer Netherlands},
 pages        = {83--266},
 doi          = {10.1007/978-94-017-0454-0_2},
)