Interpolation in Classical Propositional Logic
Logic in Computer Science
2026-02-24 v2
Abstract
We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.
Cite
@article{arxiv.2508.11449,
title = {Interpolation in Classical Propositional Logic},
author = {Patrick Koopmann and Christoph Wernhard and Frank Wolter},
journal= {arXiv preprint arXiv:2508.11449},
year = {2026}
}
Comments
The article will appear in Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter, editors. Theory and Applications of Craig Interpolation. Ubiquity Press, 2026