First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation.

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 and for (fragments of) infinitely-valued firstorder Godel logic, the logic of all linearly ordered constant domain Kripke frames.