2026-07-21T12:28:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23647 2025-10-27T10:30:38Z ddc:004 open_access

Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation Saurin, Alexis Classical Logic Interpolation Cut Elimination Linear Logic Sequent calculus System L Analyzing Maehara’s method for proving Craig’s interpolation theorem, we extract a "proof relevant" interpolation theorem for first-order LL in the sense that if π is a cut-free sequent proof of A⊢ B, we can find a formula C in the common vocabulary of A and B and proofs π₁,π₂ of A⊢ C and C⊢ B respectively such that π₁ composed with π₂ cut-reduces to π. As a direct corollary, we get similar proof relevant interpolation results for LJ and LK using linear translations. This refined interpolation is then rephrased in terms of a cut-introduction process synthetizing the interpolant. Finally, we analyze the computational content of interpolation by proving an interpolation result for Curien and Herbelin’s Duality of Computation. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexis Saurin 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.32 urn:nbn:de:0030-drops-236478 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.32 eng https://creativecommons.org/licenses/by/4.0/legalcode