Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity (Q1076669)

In this paper, the author continues his investigation of the relations among the complexities of computations, of circuits, of interpolation formulas, and of formal proofs. Some of the main results are as follows. (i) Consider tautologies \(H\to K\) that have a unique (up to logical equivalence) interpolant J. If \(P\neq NP\cap coNP\), then no deterministic Turing machine M can produce such J in polynomial time in terms of the length of \(H\to K\). (ii) Consider a finitely axiomatized, complete, first order theory \(\Theta\), and let \(\lambda_{\Theta}\) be a function of the lengths of formulas that give upper bounds on the lengths of their proofs. Further, let T be a function giving an upper bound on the time to produce J in (i). Then an upper bound for a decision procedure of \(\Theta\) in terms of a deterministic Turing machine is \(T^ q\circ \lambda^ p_{\Theta}\) for some p,q\(\in \omega\). (iii) Let \(\delta\) be a function of lengths of tautologies of the nature in (i) that gives the lengths of interpolants. Then any \(S\in NP\cap coNP\) can be computed by circuits \(\{\alpha_ n\}\) whose \(depth(\alpha_ n)'s\) do not exceed the bounds \(k\cdot \log \delta (n^ p)\) where \(k,p>0\) depend only on S.