Efficient Interpolation Beyond Cut-Free Proofs: Admissible Cuts and Optimized Extraction

Abstract

Craig interpolation is a foundational concept in logic with broad applications in formal verification, automated reasoning, and modular system design. While Maehara’s lemma enables interpolant extraction from cut-free proofs, extending interpolation to proofs with cuts has remained challenging. In this paper, we propose a generalization of Maehara’s lemma to admissible cuts – a class of cut-formulas satisfying structural constraints defined via end-sequent partitions. Our approach leverages the Ceres cut-elimination framework to identify cut-free components critical for interpolation. We show that this method not only generalizes previous results on atomic cuts but also reduces the asymptotic complexity of interpolant extraction from cubic to quadratic, thus enhancing the scalability of interpolation techniques in proof-theoretic reasoning.