Automated Reasoning

2IMF25

About this course

Many problems, such as planning logistics, optimising production processes, verification of computer systems, and also all kinds of puzzles, can be expressed as proving that a formal specification has a satisfying assignment. In this course we will concentrate on various methods for treating these kinds of problems and show the inner working of relevant algorithms. We discuss several theoretical aspects of these methods, like correctness, completeness, efficiency and usability, and also their practical application. In particular we will consider:

  • Resolution as a proof rule to prove propositions, and algorithms for satisfiability of propositions (SAT) based on resolution.
  • Extension to Satisfaction Modulo Theories (SMT).
  • Unification; resolution on predicates.
  • Binary Decision Diagrams (BDDs) to efficiently represent Boolean functions.
  • Application of BDDs to CTL-based symbolic model checking.

Learning outcomes

After completing this course, you will be able to apply various automatic techniques for reasoning about logical formulas to solve real-world problems. Specifically, at the end of this course, you will be able to:

  • Apply resolution, unification and related algorithms to prove (un)satisfiability of propositional and predicate formulas
  • Explain how SMT-solvers support general theories and apply the simplex algorithm to reason about linear inequalities.
  • Construct the Reduced Ordered Binary Decision Diagram (BDD) of a propositional formula
  • Use BDDs to perform symbolic model checking
  • Use tools that implement the above techniques to solve planning problems, verify software and detect deadlocks in hardware.

Prior knowledge

Basic programming skills.

Resources

  • Mathematical Logic for Computer Science by Mordechai Ben-Ari (https://doi.org/10.1007/978-1-4471-4129-7)
  • Slides available on course web page

Additional information

  • Credits
    ECTS 5
  • Level
    master
If anything remains unclear, please check the FAQ of TU Eindhoven.

Offering(s)

  • Start date

    2 September 2024

    • Ends
      27 October 2024
    • Term *
      Block GS1
    • Location
      Eindhoven
    • Instruction language
      English
    Course is currently running
For guests registration, this course is handled by TU Eindhoven