2025/08/15 by Koopmann, Patrick, Wernhard, Christoph, Wolter, Frank · 2 citations
#03B05 (Primary) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2508.11449
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.