CIS700

CIS700 — Fall 2024

Modern Symbolic AI and Automated Reasoning

Date Type Unit Material
Module 1 Course Intro and Basic Concepts (until 9/12)
8/27 Lecture L0 Course Intro, Sets, Bags, and Discrete Math (Slides)
8/29 Lecture L1 Propositional Logic, Truth Tables, Analytic Tableaux
9/3 Lecture L2 (Led by Yihao) "Basics" from Software Foundations
9/3 Homework HW1 Homework 1 -- "Basics" in Rocq
9/5 Lecture L3 No class (Kris at ICFP) -- work in groups on homework H1
9/10 Lecture L4 Propositional Resolution and DPLL (Slides)
9/12 Paper L5 DPLL paper discussion and HW1 Discussion
Module 2 Intuitionistic Type Theory (until 10/10)
9/17 Lecture L6 Lists and Inductively-Defined Data ("Lists")
9/19 Lecture L7 Natural Deduction and Intuitionistic Logic
9/17 Homework HW2 Homework 2 -- "Lists," "Polymorphism," and "Tactics" (subset)
9/24 Lecture L8 The Sequent Calculus
9/26 Lecture L9 Lists and Polymorphism in Coq
10/1 Lecture L10 Coq Tactics, Tactic-Based Proof Search
10/3 Lecture L11 ITT in Coq ("Logic")
10/8 Lecture L12 More ITT in Coq
10/10 Paper L13 "Formal verification of a realistic compiler" by Xavier Leroy
10/15 No Class -- Fall Break
Module 3 SAT Solving, First-Order Logic, and First-Order SMT
10/17 Lecture L14 Software Foundations: Logic
10/22 Lecture L15 Software Foundations: Inductively-Defined Propositions
10/17 Homework HW3 Homework 3 -- Inductive Propositions from SF
10/24 Paper L16 Conflicted-Directed Clause Learning (New slides) (Old Slides)
10/29 Lecture L17 MiniSAT: An Extensible SAT solver and SAT implementation tricks
10/31 Lecture L18 SMT Intro
11/5 Lecture L19 First-Order Logic and more SMT Intro (Slides)
11/7 Lecture L20 Combining SAT and Theory-Specific Solving: DPLL(T) (paper)
Module 4 Datalog and Logic Programming
11/12 Lecture L21 LeanDojo paper by Harshit
11/14 Lecture L22 EXE: Automatically Generating Inputs of Death
11/19 Lecture L23 Datalog (Slides)
11/21 Paper L24 Datalog Disassembly
11/26 Thanksgiving Break (Tu)
11/28 Thanksgiving Break (Th)
12/3 Lecture L25 Optimizing Datalog for the GPU
12/5 Paper L26 Better Together: Unifying Datalog and Equality Saturation
12/10 Paper L27 Datalog with First-Class Facts