Automated Reasoning

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.

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.

Basic programming skills.

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