2020/02/13 by Baaz, Matthias, Lolic, Anela
#FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.2002.05404
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.