Methods of AI III – Logical Reasoning
This course introduces logical reasoning and how it can be implemented in AI systems using mathematical/philosophical logic.
Overview
This course addresses questions such as what is logical reasoning about and how can it help AI agents to successfully act in the world? The course discusses the potential and limitations of modeling logical reasoning using propositional and first-order predicate logic. Methods to determine the consistency of a logical knowledge base are introduced based on the notion of satisfiability. Algorithms such as resolution and the Davis-Putman Logemann-Loveland (DPLL) algorithm are discussed, which enable logical agents to draw correct conclusions and to make implicit knowledge explicit. DPLL underlies modern SAT solvers that can solve large problems in AI optimization, which are described with billions of logical variables.
The precise treatment of logical languages and algorithms is complemented with numerous practical examples.
This course is partially based on chapters 7,8 and 9 of the textbook by Stuart Russell and Peter Norvig: Introduction to Artificial Intelligence - A Modern Approach.
The course is held in English language with German subtitles.
Which topics will be covered?
- Propositional logic (syntax, semantics, normal forms)
- Resolution
- Davis-Putnam Logemann-Loveland (DPLL) algorithm
- Satisfiability (SAT) checking
- First-order predicate logic (syntax, semantics, normal forms)
- Herbrand's theory and the reduction of predicate logic reasoning to SAT checking
- Forward and backward chaining
What will I achieve?
By the end of the course, you‘ll be able to
- understand logical methods used in AI,
- model simple application problems with logic,
- understand the capabilities and limitations of logical methods and algorithms in practice,
- understand the importance of satisfiability checking for AI optimization.
Which prerequisites do I need to fulfill?
None.
The course “Methods of AI IV – Knowledge Representation” deepens the use of logic for the representation of conceptual and factual knowledge.
The course “Methods of AI V – Constraint programming” provides additional background on SAT solvers and explains how AI optimization and constraint problems are solved with modern CP-SAT solvers.
