3 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.FL2023
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
Rodrigo Raya
We study the satisfiability problem of symbolic tree automata and decompose it into the satisfiability problem of the existential first-order theory of the input characters and the…
cs.LO2023
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…