Interpolation in Classical Propositional Logic

TL;DR

This paper explores various methods for computing Craig interpolants in classical propositional logic, discussing their theoretical properties, computational techniques, and implications for circuit complexity.

Contribution

It introduces four approaches to compute interpolants, connecting interpolation with quantifier elimination, normal forms, resolution, and tableau methods, and discusses their complexity.

Findings

Four methods for computing interpolants are detailed.

Interpolant size and circuit complexity are analyzed.

Connections between interpolation and logical proof systems are established.

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.