Proof Complexity - Interpolation

Interpolation

Consider a tautology of the form . The tautology is true for every choice of, and after fixing the evaluation of and are independent because are defined on disjoint sets of variables. This means that it is possible to define an interpolant circuit, such that both and hold. The interpolant circuit decides either if is false or if is true, by only considering . The nature of the interpolant circuit can be arbitrary. Nevertheless it is possible to use a proof of the initial tautology as a hint on how to construct . Some proof systems (e.g. resolution) are said to have efficient interpolation because the interpolant is efficiently computable from any proof of the tautology in such proof system. The efficiency is measured with respect to the length of the proof: it is easier to compute interpolants for longer proofs, so this property seems to be anti-monotone in the strength of the proof system.

Interpolation is a weak form of automatization: a way to deduce the existence of small circuits from the existence of small proofs. In particular the following three statements cannot be simultaneously true: (a) has a short proof in a some proof system; (b) such proof system has efficient interpolation; (c) the interpolant circuit solves a computationally hard problem. It is clear that (a) and (b) imply that there is a small interpolant circuit, which is in contradiction with (c). Such relation allows to turn proof length upper bounds into lower bounds on computations, and dually to turn efficient interpolation algorithms into lower bounds on proof length.