English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We study extensions of Sem\"enov arithmetic, the first-order theory of thestructure $(\mathbb{N}, +, 2^x)$. It is well-knonw that this theory becomesundecidable when extended with regular predicates over tuples of numberstrings, such as the B\"uchi $V_2$-predicate. We therefore restrict ourselvesto the existential theory of Sem\"enov arithmetic and show that this theory isdecidable in EXPSPACE when extended with arbitrary regular predicates overtuples of number strings. Our approach relies on a reduction to the languageemptiness problem for a restricted class of affine vector addition systems withstates, which we show decidable in EXPSPACE. As an application of our results,we settle an open problem from the literature and show decidability of a classof string constraints involving length constraints.

Sem\"enov Arithmetic, Affine VASS, and String Constraints