Automata-based decision procedures for weak arithmetics [Elektronische Ressource] / Felix Christopher Klaedtke

AUTOMATA-BASED DECISIONPROCEDURES FOR WEAK ARITHMETICSFebruary 2004Dissertation zur Erlangung des Doktorgradesder Fakult at fur Angewandte Wissenschaftender Albert-Ludwigs-Universit at Freiburg im BreisgauFelix Christopher Klaedtkeklaedtke@informatik.uni-freiburg.de Institut fur Informatik, Albert-Ludwigs-Universitat FreiburgGeorges-K ohler-Allee 52, 79110 Freiburg i. Br., GermanyDekan: Prof. Dr. Thomas OttmannErstreferent: Prof. Dr. David BasinZweitreferent: Prof. Dr. Wolfgang ThomasDatum der Promotion: 2. Juli 2004In memory of Alexander Schneider\Well, don’ tell ’em. Go down the river an’ stickyour head under an’ whisper ’em in the stream."| Steinbeck, The Grapes of WrathContentsAcknowledgments ::::::::::::::::::::::::::::::::::::::::::::::: viiZusammenfassung ::::::::::::::::::::::::::::::::::::::::::::::: ixAbstract::::::::::::::::::::::::::::::::::::::::::::::::::::::::: xi1 Introduction ::::::::::::::::::::::::::::::::::::::::::::::::: 11.1 Motivation, Scope, and Contributions . . . . . . . . . . . . . . . . . . . . . . . . . 11.2 Standard Notation and De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6Part I: On the Automata Size for Presburger Arithmetic 92 Automata Constructions ::::::::::::::::::::::::::::::::::::: 132.1 Representing Sets of Integers with Automata . . . . . . . . . . . . . . . . . . . 132.2 Linear Equations and Inequations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142.