Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

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

Horbach, M., Voigt, M., & Weidenbach, C. (2017). The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. Retrieved from http://arxiv.org/abs/1703.01212.

Item is

Dateien

einblenden: Dateien
ausblenden: Dateien
:
arXiv:1703.01212.pdf (Preprint), 298KB
Name:
arXiv:1703.01212.pdf
Beschreibung:
File downloaded from arXiv at 2017-03-13 08:10
OA-Status:
Sichtbarkeit:
Öffentlich
MIME-Typ / Prüfsumme:
application/pdf / [MD5]
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Horbach, Matthias1, Autor           
Voigt, Marco1, Autor           
Weidenbach, Christoph1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: Computer Science, Logic in Computer Science, cs.LO
 Zusammenfassung: The first-order theory of addition over the natural numbers, known as Presburger arithmetic, is decidable in double exponential time. Adding an uninterpreted unary predicate to the language leads to an undecidable theory. We sharpen the known boundary between decidable and undecidable in that we show that the purely universal fragment of the extended theory is already undecidable. Our proof is based on a reduction of the halting problem for two-counter machines to unsatisfiability of sentences in the extended language of Presburger arithmetic that does not use existential quantification. On the other hand, we argue that a single $\forall\exists$ quantifier alternation turns the set of satisfiable sentences of the extended language into a $\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to the realm of linear arithmetic over the ordered real numbers. This concerns the undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness for sentences with at least one quantifier alternation. Finally, we discuss the relevance of our results to verification. In particular, we derive undecidability results for quantified fragments of separation logic, the theory of arrays, and combinations of the theory of equality over uninterpreted functions with restricted forms of integer arithmetic. In certain cases our results even imply the absence of sound and complete deductive calculi.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2017-03-032017
 Publikationsstatus: Online veröffentlicht
 Seiten: 22 p.
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: arXiv: 1703.01212
URI: http://arxiv.org/abs/1703.01212
BibTex Citekey: VoigtHorbachWeidenbacharXiv2017
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: