Automated Logical Reasoning

(CS 389L)

Request Info

This is a course on computational logic and its applications in computer science, particularly in the context of software verification. Computational logic is a fundamental part of many areas of computer science, including artificial intelligence and programming languages. This class introduces the fundamentals of computational logic and investigates its many applications in computer science. Specifically, the course covers a variety of widely used logical theories and looks at algorithms for determining satisfiability in these logics as well as their applications.

  • Syllabus

    • Normal forms; decision procedures for propositional logic; SAT solvers (2 weeks)
    • Applications of SAT solvers and binary decision diagrams (1 week)
    • Semantics of to first-order logic and theoretical properties (1 weeks)
    • First-order theorem proving (1.5 weeks)
    • Intro to first-order theories (0.5 week)
    • Theory of equality (0.5 week)
    • Decision procedures for rationals and integers (1.5 weeks)
    • DPLL(T) framework and SMT solvers (1 week)
    • Basics of software verification (1 week)
    • Automating software verification (2 weeks)
  • Course Category

    Theory Course

    Course Availability

    • Spring 2022

Meet Your Instructor

Take the Next Step

Advance your computer science career with UT Austin's Master of Computer Science Online.