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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Simon Corbard,
  • Anela Lolić

摘要

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.