Go to page
 

Bibliographic Metadata

Title
Deciding Presburger Arithmetic Using Automata Theory / submitted by Fritz Kliemann, BSc
Additional Titles
Entscheidung der Presburger Arithmetik mit Automatentheorie
AuthorKliemann, Fritz
CensorAichinger, Erhard
PublishedLinz, 2018
Descriptionix, 153 Seiten : Illustrationen
Institutional NoteUniversität Linz, Masterarbeit, 2018
Annotation
Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers
LanguageEnglish
Document typeMaster Thesis
Keywords (DE)Presburger Arithmetik / Automatentheorie / Entscheidbarkeit / entscheidbar / Predicata
Keywords (EN)Presburger arithmetic/ automata theory / decidability / decidable / Predicata
URNurn:nbn:at:at-ubl:1-25284 Persistent Identifier (URN)
Restriction-Information
 The work is publicly available
Files
Deciding Presburger Arithmetic Using Automata Theory [1.88 mb]
Links
Reference
Classification
Abstract (German)

Die Presburger Arithmetik, benannt nach M. Presburger, ist die Theorie der natürlichen Zahlen mit der Addition als der einzigen Operation. M. Presburger bewies 1929 ihre Vollständigkeit und aufgrund des konstruktiven Beweises zeigte er außerdem, durch die Benützung von Quantorenelimination, dass die Presburger Arithmetik entscheidbar ist. Diese Masterarbeit beschreibt eine Entscheidungsprozedur für die Presburger Arithmetik, die auf J. R. Büchi (1960) zurückgeht und Automatentheorie verwendet, um die Ausdrücke erster Ordnung zu beschreiben. Die Prozedur beschreibt einen Ausdruck erster Ordnung als eine Teilmenge von den natürlichen Zahlen, die den Ausdruck erfüllen. Diese Menge, genannt die Lösung des Ausdrucks, wird mit einem minimalen deterministischen endlichen Automaten so in Verbindung gebracht, dass die Sprache des Automaten gleich der Lösungen des Ausdrucks ist. Für einen Ausdruck erster Ordnung, welcher keine freien Variablen enthält, entscheidet der dazugehörige minimale deterministische endliche Automat, ob der Ausdruck ein Satz der Presburger Arithmetik ist oder nicht. Zusätzlich ist das implementierte Entscheidungsverfahren in GAP Groups, Algorithms, and Programming ein Teil dieser Masterarbeit, welches für jeden Ausdruck einen minimalen deterministischen Automaten erzeugt.

Abstract (English)

The Presburger arithmetic, named after M. Presburger, is the first-order theory of the natural numbers with the addition as the only operation. In 1929, M. Presburger proved its completeness and due to his constructive proof he also showed, using quantifier elimination, that the Presburger arithmetic is decidable. This thesis describes a decision procedure for the Presburger arithmetic based on J. R. Büchi (1960), which uses automata theory to describe the first-order formulas. The procedure describes a first-order formula as a set of natural numbers which satisfy the formula. This set, called the solutions of the formula, is associated with a minimal deterministic finite automaton such that the language of the automaton is equal to the solutions of the formula. Hence for a first-order formula, containing no free variables, the corresponding minimal deterministic finite automaton decides if the formula is an element of the Presburger arithmetic or not. Additionally, the implemented decision procedure in GAP Groups, Algorithms, and Programming is part of this thesis, allowing to construct a minimal deterministic finite automaton for any first-order formula.

Stats
The PDF-Document has been downloaded 6 times.