Deciding Presburger Arithmetic Using Automata Theory

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.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.submitted by Fritz Kliemann, BScAbweichender Titel laut Übersetzung der Verfasserin/des VerfassersUniversität Linz, Masterarbeit, 2018(VLID)313091