2 papers
cs.LO2026
Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications
Rodrigo Raya, Christophe Ringeissen
We investigate quantifier-free interpolation properties for several fragments generalising the extensional theory of arrays. Our results include the (general) quantifier-free inter…
cs.LO2024
Combinatory Array Logic with Sums
Rodrigo Raya
We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combinatory array logic with an ordering relation on the index set and the ability to e…