Foundations of Artificial Intelligence III

The course "Foundations of Artificial Intelligence III" introduces into the foundations of mathematical logic and satisfiability checking. The course covers the languages of propositional and first-order logic. It introduces their syntax and semantics, defines several normal forms used by AI algorithms to perform logical reasoning, and introduces resolution and the Davis-Putman Logemann-Loveland (DPLL) algorithm.

We especially discuss how the satisfiability of logical formulas can be checked automatically and introduce the foundations of modern Satisfiability (SAT) solvers, which gain increasing importance to solve large search, optimization, and verification problems with AI methods. 

The thorough theoretical treatment of the logical languages and the algorithms is complemented with numerous examples.

The course also provides the theoretical background for the courses on Knowledge Representation and Constraint Optimization in this course series. 

The course is based on the textbook by Stuart Russell and Peter Norvig: Introduction to Artificial Intelligence - A Modern Approach, 3rd edition, 2012, or 4th edition 2020. The 3rd edition is also available in German: Stuart Russell und Peter Norvig: Künstliche Intelligenz - Ein Moderner Ansatz, 3. aktualisierte Auflage, Pearson 2012.

The course also uses material from the book by Uwe Schönig: Logic for Computer Scientists, Modern Birkhäuser Classics, 1989.