Semënov arithmetic, affine \{VASS\}, and string constraints

DOI10.4230/LIPICS.STACS.2024.29MaRDI QIDQ6902695zbMATH OpenFDO

Authors Andrei Draghici, Christoph Haase, Florin Manea

Publication date 10 November 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.STACS.2024.29

zbMATH Keywords

arithmetic theoriesBüchi arithmeticexponentiationstring constraintsvector addition systems with states

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A decision procedure for string constraints with string/integer conversion and flat regular constraints
• An SMT solver for regular expressions and linear arithmetic over string length
• Automatic presentations of structures
• scientific article; zbMATH DE number 4031630 (Why is no real title available?)
• scientific article; zbMATH DE number 1538036 (Why is no real title available?)
• Logic and p-recognizable sets of integers
• ON CERTAIN EXTENSIONS OF THE ARITHMETIC OF ADDITION OF NATURAL NUMBERS
• On the existential theories of Büchi arithmetic and linear p-adic fields
• Reachability in register machines with polynomial updates
• The complexity of Presburger arithmetic with power or powers
• Towards more efficient methods for solving regular-expression heavy string constraints

Cited in

(5)

• Formal languages and arithmetic theories: recent results and open problems
• Integer linear-exponential programming in NP by quantifier elimination
• On the decidability and expressive power of several theories based on string constraints
• An introduction to the theory of linear integer arithmetic (invited paper)
• Word equations with length constraints via weak arithmetics and matrix reachability problems

This page was built for publication: Semënov arithmetic, affine \{VASS\}, and string constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6902695)