Decision Procedures for Linear Arithmetic Theories
Supervisor
Suitable for
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