First-Order Interpolation Derived from Propositional Interpolation
Logic
2020-02-14 v1
Abstract
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.
Cite
@article{arxiv.2002.05404,
title = {First-Order Interpolation Derived from Propositional Interpolation},
author = {Matthias Baaz and Anela Lolic},
journal= {arXiv preprint arXiv:2002.05404},
year = {2020}
}