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

The first-order theory of addition over the natural numbers, known asPresburger arithmetic, is decidable in double exponential time. Adding anuninterpreted unary predicate to the language leads to an undecidable theory.We sharpen the known boundary between decidable and undecidable in that we showthat the purely universal fragment of the extended theory is alreadyundecidable. Our proof is based on a reduction of the halting problem fortwo-counter machines to unsatisfiability of sentences in the extended languageof Presburger arithmetic that does not use existential quantification. On theother hand, we argue that a single $\forall\exists$ quantifier alternationturns the set of satisfiable sentences of the extended language into a$\Sigma^1_1$-complete set. Some of the mentioned results can be transfered tothe realm of linear arithmetic over the ordered real numbers. This concerns theundecidability of the purely universal fragment and the $\Sigma^1_1$-hardnessfor sentences with at least one quantifier alternation. Finally, we discuss therelevance of our results to verification. In particular, we deriveundecidability results for quantified fragments of separation logic, the theoryof arrays, and combinations of the theory of equality over uninterpretedfunctions with restricted forms of integer arithmetic. In certain cases ourresults even imply the absence of sound and complete deductive calculi.

The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable