# Tutorial on SMT and Polynomial Arithmetic

**Tutorial dates: May 26-27, 2016**

**Tutorial location: EDIT 3364 (May 26) and EDIT 8103 (May 27)**

**Lecturers:**

## Information on Tutorial

The tutorial serves as a crash course in polynomial algebra.

We will first discuss the satisfiability problem modulo various theories, known as the SMT problem.

Then, we will focus on the theory of polynomial arithmetic and introduce decision procedures from polynomial algebra.
In particular, we will present decision procesures using Groebner basis computation
and quantifier elimination via Cylindrical Algebraic Decomposition.

## Tutorial Schedule

There will be 3 lectures, each lecture of 90 minutes. The tentative course schedule is as follows:

**Thursday, May 26, EDIT 3364:**

- 10:00-12:00 - Martina Seidl: SAT/SMT solving (slides)
- 14:00-16:00 - Manuel Kauers: SMT and Polynomial Arithmetic - Groebner Basis (slides)

**Friday, May 27, EDIT 8103:**

- 10:00-12:00 - Maximillian Jaroschek: Quantifier Elimination (slides)