arXiv · 2002.05404
First-Order Interpolation Derived from Propositional Interpolation
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.
Explore related subjects
Keep this discovery
Matthias Baaz, Anela Lolic. 2020-02-13. First-Order Interpolation Derived from Propositional Interpolation. https://arxiv.org/abs/2002.05404
Cite the original work for its findings. Save a collection to share your selection of sources.