Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications
2026-07-06 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study certain logical properties called quantifier-free interpolation in advanced versions of array theories used in computer science. They focus on fragments that extend the usual theory of arrays and show new positive results for these properties, including in contexts with complex specifications over unlimited domains. Their work is the first to demonstrate such interpolation results in these more expressive array theories.
quantifier-free interpolationextensional theory of arrayscombinatory array logiciterated diffsuniform interpolationlogical fragmentsunbounded domainstheory of arrays
Authors
Rodrigo Raya, Christophe Ringeissen
Abstract
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.