Document Open Access Logo

The Size of Interpolants in Modal Logics

Authors Balder ten Cate , Louwe B. Kuijer , Frank Wolter

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.26.pdf
  • Filesize: 1.11 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Modal logic
  • strongest implicates
  • uniform interpolants
  • Craig interpolants

Metrics

Abstract

We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP is included in P/poly. The reduction also holds for Craig interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or GL we obtain the following dichotomy: tabular logics have "propositionally sized" interpolants while for non-tabular logics an unconditional exponential lower bound holds.

Cite As Get BibTex

Balder ten Cate, Louwe B. Kuijer, and Frank Wolter. The Size of Interpolants in Modal Logics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 26:1-26:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.26

Author Details

Balder ten Cate
  • University of Amsterdam, The Netherlands
Louwe B. Kuijer
  • University of Liverpool, UK
Frank Wolter
  • University of Liverpool, UK

References

  1. Noga Alon and Ravi B. Boppana. The monotone circuit complexity of boolean functions. Comb., 7(1):1-22, 1987. URL: https://doi.org/10.1007/BF02579196.
  2. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  3. Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in description and modal logics with nominals and role inclusions. ACM Trans. Comput. Log., 24(4):34:1-34:51, 2023. URL: https://doi.org/10.1145/3597301.
  4. Marta Bílková. Uniform interpolation and propositional quantifiers in modal logics. Stud Logica, 85(1):1-31, 2007. URL: https://doi.org/10.1007/S11225-007-9021-5.
  5. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  6. Balder ten Cate, Willem Conradie, Maarten Marx, and Yde Venema. Definitorially complete description logics. In Proc. of KR, pages 79-89, 2006. URL: https://aaai.org/papers/KR06-011-definitorially-complete-description-logics/.
  7. Balder ten Cate, Enrico Franconi, and Inanç Seylan. Beth definability in expressive description logics. J. Artif. Intell. Res., 48:347-414, 2013. URL: https://doi.org/10.1613/JAIR.4057.
  8. Alexander V. Chagrov and Michael Zakharyaschev. Modal Logic, volume 35 of Oxford logic guides. Oxford University Press, 1997. Google Scholar
  9. William Craig. Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. J. Symb. Log., 22(3):269-285, 1957. URL: https://doi.org/10.2307/2963594.
  10. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the mu-calculus: Interpolation, lyndon and los-tarski. J. Symb. Log., 65(1):310-332, 2000. URL: https://doi.org/10.2307/2586539.
  11. Hugo Férée, Iris van der Giessen, Sam van Gool, and Ian Shillito. Mechanised uniform interpolation for modal logics k, gl, and isl. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 43-60. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_3.
  12. Dov M. Gabbay and Larisa Maksimova. Interpolation and Definability: Modal and Intuitionistic Logics. Oxford University Press, May 2005. URL: https://doi.org/10.1093/acprof:oso/9780198511748.001.0001.
  13. Silvio Ghilardi, Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Conservative extensions in modal logic. In Guido Governatori, Ian M. Hodkinson, and Yde Venema, editors, Advances in Modal Logic 6, papers from the sixth conference on "Advances in Modal Logic," held in Noosa, Queensland, Australia, on 25-28 September 2006, pages 187-207. College Publications, 2006. URL: http://www.aiml.net/volumes/volume6/Ghilardi-Lutz-Wolter-Zakharyaschev.ps.
  14. Silvio Ghilardi and Marek W. Zawadowski. Undefinability of propositional quantifiers in the modal system S4. Stud Logica, 55(2):259-271, 1995. URL: https://doi.org/10.1007/BF01061237.
  15. Jean Christoph Jung, Jędrzej Kołodziejski, and Frank Wolter. Computation of interpolants for description logic concepts in hard cases. arXiv preprint, 2025. URL: https://arxiv.org/abs/2507.15689.
  16. Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, and Frank Wolter. Separating data examples by description logic concepts with restricted signatures. In Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem, editors, Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021, pages 390-399, 2021. URL: https://doi.org/10.24963/KR.2021/37.
  17. Jean Christoph Jung and Frank Wolter. Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470585.
  18. Richard Karp. Turing machines that take advice. Enseign. Math., 28:191-209, 1982. Google Scholar
  19. Richard M Karp and Richard J Lipton. Some connections between nonuniform and uniform complexity classes. In Proceedings of the twelfth annual ACM symposium on Theory of computing, pages 302-309, 1980. URL: https://doi.org/10.1145/800141.804678.
  20. Patrick Koopmann, Christoph Wernhard, and Frank Wolter. Interpolation in classical propositional logic, 2025. URL: https://doi.org/10.48550/arXiv.2508.11449.
  21. Marcus Kracht. Tools and Techniques in Modal Logic. Elsevier, 1999. Google Scholar
  22. Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. A non-uniform view of Craig interpolation in modal logics with linear frames. CoRR, abs/2312.05929, 2023. URL: https://doi.org/10.48550/arXiv.2312.05929.
  23. Paolo Liberatore. The ghosts of forgotten things: A study on size after forgetting. Ann. Pure Appl. Log., 175(8):103456, 2024. URL: https://doi.org/10.1016/J.APAL.2024.103456.
  24. Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 989-995. IJCAI/AAAI, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-170.
  25. Maarten Marx. Interpolation in modal logic. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998, pages 154-163. Springer, 1998. URL: https://doi.org/10.1007/3-540-49253-4_13.
  26. Daniele Mundici. A lower bound for the complexity of Craig’s interpolants in sentential logic. Arch. Math. Log., 23(1):27-36, 1983. URL: https://doi.org/10.1007/BF02023010.
  27. Konstantinos Papafilippou and David Fernández-Duque. Exponential lower bounds on definable fixed points. In Jörg Endrullis and Sylvain Schmitz, editors, 33rd EACSL Annual Conference on Computer Science Logic, CSL 2025, February 10-14, 2025, Amsterdam, Netherlands, volume 326 of LIPIcs, pages 25:1-25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CSL.2025.25.
  28. Andrew M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log., 57(1):33-52, 1992. URL: https://doi.org/10.2307/2275175.
  29. Alexander Alexandrovich Razborov. Lower bounds on the monotone complexity of some boolean functions. In Doklady Akademii Nauk, volume 281(4), pages 798-801. Russian Academy of Sciences, 1985. Google Scholar
  30. Benjamin Rossman. Formulas versus circuits for small distance connectivity. SIAM J. Comput., 47(5):1986-2028, 2018. URL: https://doi.org/10.1137/15M1027310.
  31. Uwe Schöning and Jacobo Torán. A note on the size of Craig Interpolants. In Circuits, Logic, and Games, volume 6451 of Dagstuhl Seminar Proceedings (DagSemProc), pages 1-9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2007. URL: https://doi.org/10.4230/DagSemProc.06451.3.
  32. Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard, and Frank Wolter, editors. Theory and Applications of Craig Interpolation. Ubiquity Press, 2026. Google Scholar
  33. Iris van der Giessen, Raheleh Jalali, and Roman Kuznets. Uniform interpolation via nested sequents and hypersequents. J. Log. Comput., 35(6), 2025. URL: https://doi.org/10.1093/LOGCOM/EXAE053.
  34. Albert Visser et al. Uniform interpolation and layered bisimulation. In Gödel'96: Logical foundations of mathematics, computer science and physics - Kurt Gödel’s legacy, pages 139-164. Association for Symbolic Logic, 1996. Google Scholar
  35. Frank Wolter and Michael Zakharyaschev. Modal decision problems. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 427-489. North-Holland, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80010-3.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact