2025/08/15 by Maximiliano Cristiá, Cristiá, Maximiliano, Gianfranco Rossi +1
Computer Science · #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · doi:10.48550/arxiv.2508.11447
openalex publication_date 2025/08/15 · openalex created_date 2026/05/13 · openalex updated_date 2026/07/28
We encode arrays as functions which, in turn, are encoded as sets of ordered pairs. The set cardinality of each of these functions coincides with the length of the array it is representing. Then we define a fragment of set theory that is used to give the specifications of a non-trivial class of programs with arrays. In this way, array reasoning becomes set reasoning. Furthermore, a decision procedure for this fragment is also provided and implemented as part of the log (read 'setlog') tool. log is a constraint logic programming language and satisfiability solver where sets and binary relations are first-class citizens. The tool already implements a few decision procedures for different fragments of set theory. In this way, arrays are seamlessly integrated into log thus allowing users to reason about sets, functions and arrays all in the same language and with the same solver. The decision procedure presented in this paper is an extension of decision procedures defined in earlier works not supporting arrays.