CIS700

CIS700 — Fall 2023

Modern Symbolic AI and Automated Reasoning

</a></b></td>
Date Type Unit Material
8/29 Lecture L0 Course Intro and Propositional Logic (Slides)
8/31 Lecture L1 Finishing L0; Intuitionistic Propositional Logic (Part 1) (Slides)
9/5 Lecture L2 Kris gone at ICFP '23, class canceled
9/7 Lecture L3 Intuitionistic Propositional Logic (Slides)
9/12 Lecture L4 Propositional Resolution and DPLL (Slides)
9/14 Lecture L5 DPLL paper discussion
9/14 Project P1 SAT Solving -- Released (Slides/Specification)
9/19 Lecture L6 Conflict-Directed Clause Learning (Reading) (Slides)
9/21 Lecture L7 Chaff: Engineering an Efficient SAT Solver
9/26 Lecture L8 Learning in CDCL; Horn-SAT and Datalog (Slides)
9/28 Lecture L9 An Extensible SAT-solver
9/28 Project P1 PROJECT 1 DEADLINE
9/28 Project P2 Implementing Datalog -- Released (click me!)
10/3 Lecture L11 Datalog Implementation; First-Order Logic and SMT primer
10/5 Lecture L11 Automatic Index Selection for Large-Scale Datalog Computation
10/10 Fall Break
10/12 Lecture L12 EXE: Automatically Generating Inputs of Death
10/12 Project P2 PROJECT 2 DEADLINE
10/17 Lecture L13 Satisfiability Modulo Theories (SMT) introduction (Slides)
10/19 Lecture L14 First order theories: bitvectors, uninterpreted functions, and arrays
10/24 Lecture L15 Extending Datalog to Recursive Aggregation (led by Yihao)
10/26 Exam M1 Bonus Take-Home Midterm 1 (no class!)
10/31 Lecture L16 Extending DPLL to SMT via DPLL(T)
11/2 Lecture L17 (Kris Gone): Meet to work on P3
11/2 Project P3 Symbolic Executor -- Released
11/7 Lecture L18 Strucured Datalog and Slog
11/9 Lecture L19 Higher-Order, Data-Parallel Structured Deduction
11/9 Project P3 PROJECT 3 DEADLINE
11/9 Project P4 Final Project: Prepare a Lecture -- Released
11/14 Lecture L20 Model Checking, Buchi Automata, LTL and CTL
11/16 Lecture L21 Software Model Checking
11/21 Thanksgiving Break (Tu)
11/23 Thanksgiving Break (Th)
11/28 Lecture L22 Generalized Property-Directed Reachability
11/30 Lecture L23 Student Group Lectures -- Day 1
12/5 Lecture L24 Student Group Lectures -- Day 2
12/7 Lecture L25 Student Group Lectures -- Day 3
Final Final Project (Detailed Notes and Slides) -- Due