arXiv subjects

Rodrigo Raya

Publications and source records attributed to Rodrigo Raya.

7 recordsLinked to original sources

arXiv2026

Towards Quantifier-Free Interpolation in Array Languages with Unbounded Data Specifications

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.

cs.LO↗

arXiv2023

Combinatory Array Logic with Sums

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 express sums of elements. We compare our fragment with seven other fragments in the literature in terms of their expressiveness and computational complexity.

cs.LO↗

arXiv2023

The Complexity of Checking Non-Emptiness in Symbolic Tree Automata

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 existential monadic second-order theory of the indices of the accepted words. We use our decomposition to obtain tight computational complexity bounds on the decision problem for this automata class and an extension that considers linear arithmetic constraints on the underlying effective Boolean algebra

cs.FL↗

arXiv2023

The Complexity of Satisfiability Checking for Symbolic Finite Automata

We study the satisfiability problem of symbolic finite automata and decompose it into the satisfiability problem of the theory of the input characters and the monadic second-order theory of the indices of accepted words. We use our decomposition to obtain tight computational complexity bounds on the decision problem for this automata class and an extension that considers linear arithmetic constraints on the underlying effective Boolean algebra.

cs.LO↗

arXiv2022

NP Decision Procedure for Monomial and Linear Integer Constraints

Motivated by satisfiability of constraints with function symbols, we consider numerical inequalities on non-negative integers. The constraints we consider are a conjunction of a linear system Ax = b and a conjunction of (non-)convex constraints of the form x_i >= x_j^n (x_i <= x_j^n). We show that the satisfiability of these constraints is NP-complete even if the solution to the linear part is given explicitly. As a consequence, we obtain NP completeness for an extension of certain quantifier-free constraints on sets with cardinalities (QFBAPA) with function images S = f[P^n].

cs.LO↗

arXiv2021

NP Satisfiability for Arrays as Powers

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinatory array logic fragment to handle cardinality constraints. The resulting fragment is independent of the base element and index set theories.

cs.LO↗

arXiv2020

Formal Proof of the Group Law for Edwards Elliptic Curves

This article gives an elementary computational proof of the group law for Edwards elliptic curves. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. Unlike other proofs, no preliminaries such as intersection numbers, Bezout's theorem, projective geometry, divisors, or Riemann Roch are required. The proof of the group law has been formalized in the Isabelle/HOL proof assistant.

math.AG↗