Efficient interpolation beyond cut-free proofs

DOI10.1016/J.TCS.2026.116212MaRDI QIDQ7363135zbMATH OpenFDO

Authors Simon Corbard, Anela Lolic

Publication date 29 September 2026

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.TCS.2026.116212

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• An interpolation theorem in the predicate calculus
• CERES for first-order schemata
• Cut-elimination and redundancy-elimination by resolution
• Efficient interpolation beyond cut-free proofs: admissible cuts and optimized extraction
• Extracting Herbrand systems from refutation schemata
• Extraction of expansion trees
• Herbrand's theorem in inductive proofs
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• Interpolants, cut elimination and flow graphs for the propositional calculus
• Interpolation and model checking
• Interpolation in computing science: The semantics of modularization
• Interpolation in extensions of first-order logic
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Methods of cut-elimination
• Proof theory. 2nd ed
• Schematic cut elimination and the ordered pigeonhole principle
• Schematic refutations of formula schemata
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Towards a clausal analysis of cut-elimination
• Untersuchungen über das logische Schließen. II.

This page was built for publication: Efficient interpolation beyond cut-free proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7363135)