Skip to main content

Decision Procedures for Linear Arithmetic Theories

Supervisor

Christoph Haase

Suitable for

Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C

Abstract

Arithmetic theories are logical theories for reasoning about number systems, such as the integers, rationals, and reals, together with associated arithmetic operations such as addition and multiplication. The goal of this project is to give a comprehensive overview over different approaches to deciding linear arithmetic theories based on quantifier elimination, finite-state automata and generating sets