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.

Module Propositional Logic

• Introduction to propositional logic
  • Syntax
  • Semantics
  • Conjunctive and disjunctive normal forms
  • Interpretation and model of a formula
• Reasoning in propositional logic
  • Resolution
• Satisfiability Checking
  • Davis-Putnam Logemann-Loveland algorithm

Module First-Order Predicate Logic

• Introduction to first-order predicate logic
  • Syntax
  • Semantics
  • Satisfiability
• Normal Forms
  • Prenex normal form
  • Skolem normal form
  • Clausal normal form
• Herbrand's Theory
  • Herbrand universe and Herbrand structure
  • Herbrand expansion
  • Gödel-Herbrand-Skolem and Herbrand theorem
  • Ground Substitution

By the end of the course, you‘ll be able to

• understand the logical foundations of logic-based methods used in and developed by AI,
• understand the practical importance of satisfiability checking,
• formalize a simple problem in propositional logic or first-order predicate logic,
• compute normal forms for formulas in propositional logic and first-order predicate logic,
• understand how resolution and the Davis-Putnam Logemann-Loveland Algorithm work and apply these algorithms to small examples

None.