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 and defines several normal forms used by AI algorithms to perform logical reasoning.
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 course also provides the theoretical background for the courses on Knowledge Representation and Constraint Reasoning in this course series.
The thorough theoretical treatment of the logical languages and the algorithms is complemented with numerous examples.
The first module introduces propositional logic.
The first part defines the syntax and semantics of propositional logic. The interpretation of a logical formula is explained, which assigns truth values to the Boolean variables of a formula. Properties of a formula such as satisfiability, unsatisfiability, falsifiability, and validity are discussed. Two normal forms for formulas in propositional logic are introduced: conjunctive and disjunctive normal form.
The second part introduces into reasoning in propositional logic. The entailment relation between logical formulas is defined and the role of the contradiction theorem is discussed, which allows an AI system to show that a logical sentence is entailed by a knowledge base through an indirect proof. A proof calculus for such an indirect proof based on resolution is introduced and its properties of soundness and refutation-completeness are discussed.
The third part introduces the Davis-Putnam Logemann-Loveland algorithm as a sound and complete calculus for propositional logic, which forms the foundation for algorithms used in SAT-solvers. Heuristics and algorithmic techniques exploited in this algorithm are discussed.
The second module in this course introduces first-order predicate logic.
The first part defines the syntax and semantics of first-order predicate logic. The notions of interpretation, satisfiability, and entailment for a formula in first-order predicate logic are introduced.
The second part defines three normal forms: prenex normal form, skolem normal form, and clausal normal form used by AI systems to perform reasoning in first-order predicate logic.
The third part deals with Herbrand´s theory and shows how reasoning in first-order predicate logic can be reduced to satisfiability checking in propositional logic.
The course is based on the textbook by Stuart Russell and Peter Norvig: Introduction to Artificial Intelligence, 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.
The course is held in English language with German subtitles.
This course is part of the course series "Foundations of Artificial Intelligence I-V":
- Foundations of Artificial Intelligence I: Introduction to AI, Agents
- Foundations of Artificial Intelligence II: Search algorithms
- Foundations of Artificial Intelligence III: Logic and satisfiability
- Foundations of Artificial Intelligence IV: Knowledge representation
- Foundations of Artificial Intelligence V: Constraint solving problems
The single courses deal with different methodological complexes of AI.
Which topics will be covered?
Module Propositional Logic
- Introduction to propositional logic
- Conjunctive and disjunctive normal forms
- Interpretation and model of a formula
- Reasoning in propositional logic
- Satisfiability Checking
- Davis-Putnam Logemann-Loveland algorithm
Module First-Order Predicate Logic
- Introduction to first-order predicate logic
- 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
What will I achieve?
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
Which prerequisites do I need to fulfill?