Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications
计算机科学中的逻辑
2026-07-06 v1
摘要
We investigate quantifier-free interpolation properties for several fragments generalising the extensional theory of arrays. Our results include the (general) quantifier-free interpolation properties of combinatory array logic with iterated diffs and the uniform interpolation property of the simple flat array fragment. To our knowledge, these are the first positive quantifier-free interpolation results obtained for theories of arrays featuring expressive specifications over unbounded domains.
引用
@article{arxiv.2607.05126,
title = {Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications},
author = {Rodrigo Raya and Christophe Ringeissen},
journal= {arXiv preprint arXiv:2607.05126},
year = {2026}
}