Complexity of Craig's interpolation

In this paper we investigate the length ‖ χ ‖ of the shortest interpolant of a valid implication φ → ψ in terms of ‖ φ ‖ + ‖ ψ ‖ , both in sentential and in first-order logic. In the case of sentential logic, we give a precise exponential upper bound for ‖ χ ‖ . We also show that the information about the growth of ‖ χ ‖ has some implications for computation theory. In the case of first-order logic we exhibit a very short valid implication whose interpolants are all impossibly long.