Exercises

Here you can download the exercise sheets.

Exercise 1

Normal Forms, Satisfiability/Validity, conversion to DNF NP complete

Exercise 2

First Order Logic: Syntax, Validity, Prenex Normal Form.

Exercise 3

T-Validity in Theory of equality, peano arithmetic, recursive data structures and combined theories.

Exercise 4

Theory of Arrays, Well-founded Induction, Structural Induction

Exercise 5

Quantifier Elimination

Exercise 6

Quantifier-free conjunctive rational arithmetic

Exercise 7

Quantifier Free Theory of Equality

Exercise 8

Quantifier-free conjunctive theories (equality, lists, arrays).

Exercise 9

Array Property Fragment for T_A^= and T_A^Z.

Exercise 10

Program Correctness with PiVC

Exercise 11

piVC, DPLL(T)

Exercise 12

DPLL(T) with Nelson-Oppen, Minimal Unsatisfiable Core

Exercise 13

Interpolants