  This paper develops a general methodology to connect propositional and
first-order interpolation. In fact, the existence of suitable skolemizations
and of Herbrand expansions together with a propositional interpolant suffice to
construct a first-order interpolant. This methodology is realized for
lattice-based finitely-valued logics, the top element representing true. It is
shown that interpolation is decidable for these logics.
