Skip to main content

Decision Procedures for Linear Arithmetic Theories


Christoph Haase

Suitable for

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


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