Image
Foundations of AI III
KI-Campus-Original
Foundations of Artificial Intelligence III

Logic and satisfiability

This course is part of the course series "Foundations of Artificial Intelligence I-VI" that covers a variety of algorithms and methods that are of central importance in AI and of major practical relevance.

Start date
November 2021
Duration
4 weeks à 3 hours
Language
English

Overview

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.

Which topics will be covered?

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

 

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?

None. 

Who is offering this course?

Jana Koehler
Prof. Dr. Jana Koehler
Deutsches Forschungszentrum für Künstliche Intelligenz
Universität des Saarlandes
Artificial Intelligence Group / Saarland University
Sophia Saller
Dr. Sophia Saller
Deutsches Forschungszentrum für Künstliche Intelligenz
Annika Engel
Annika Engel
Deutsches Forschungszentrum für Künstliche Intelligenz
Prof. Dr. Jörg Hoffmann
Prof. Dr. Jörg Hoffmann
Artificial Intelligence Group / Saarland University
Lena Marie Budde
Lena Marie Budde
Artificial Intelligence Group / Saarland University
Anna Kenter
Anna Kenter
Artificial Intelligence Group / Saarland University
Andrea Nawrath-Herz
Andrea Nawrath-Herz
Deutsches Forschungszentrum für Künstliche Intelligenz

The creators of the learning opportunities are responsible for their content.

What else should I know?

The creators of the learning opportunities are responsible for their content.

Learning format:
Online course
Level:
Beginner
License
CC-BY-SA 4.0