This course covers the foundations of computational logic. We will cover the following three topics.
- First Order Logic. The development will start from first principles and will cover some of the most important results of modern logic, including Godel's completeness and incompleteness theorems, the Lowenheim-Skolem theorems, the compactness theorem, and undecidability results.
- Decision Procedures. We will look at how one can mechanize and automate various logics. In particular, we will study recent advances in decision procedures, including for SAT (Boolean Satisfiability) and the SMT (Satisfiability modulo theories) framework.
- Computer Aided Reasoning. The focus here is on using logic to describe and reason about computation. We will explore the foundations of the ACL2 theorem proving system, paying close attention to recursion and induction. We will use the ACL2 Sedan to reason about programs.
The intended audience is PhD students with a strong mathematical background, but gifted Undergraduate and Masters students are also welcome. If you're not sure if this class is appropriate for you, feel free to contact me.
Grades will be based on homeworks, exams, and a class project.