CS-E3220: SMT — Satisfiability Modulo Theories¶
These are the lecture notes for the rounds 9 (Part I) and 10 (Part II) in the Aalto University course CS-E3220 Declarative Programming organized in Autumn \(2020\).
Note: the Part III is not included in the course material in Autumn 2020 but is only included here as an extra material for the interested reader.
The lecture notes and slides for other rounds are given elsewhere, please see the MyCourses page of the course.
- Part I: Basic Definitions
- Part II: Solving Satisfiability of Quantifier-Free Formulas
- Part III: Some further topics (NOT INCLUDED IN THE AUTUMN 2020 VERSION)