CS 576: Topics in Automated Deduction (Spring 2026): Lectures main  ::  policy  ::  lectures  ::  mps  ::  project  ::  faq  ::  doc  ::  downloads

Videos of class lectures Lecture Schedule for Spring 2026 Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Jan 20 Course Introduction slides (full sized PDF) (six up PDF) files Demo1.thy files Demo2_inc.thy Jan 22 Intro continued slides (full sized PDF) (six up PDF)   Jan 27 Basic Isabelle syntax slides (revised) (full sized PDF) (six up PDF) Jan 29 Introducing new types and terms slides (full sized PDF) (six up PDF) files Demo3.thy   Feb 3 Datatypes and Definitions slides (full sized PDF) (six up PDF) files Demo4.thy Feb 5 Rewriting Simplification slides (full sized PDF) (six up PDF) files Demo4.thy files Demo5.thy   Feb 10 Rewriting, Introduction and Elimination Rules in HOL slides (full sized PDF) (six up PDF) Feb 12 Introduction and Elimination Rules in HOL (cont) slides (full sized PDF) (six up PDF) files Demo6.thy   Feb 17 Quantifier Intro and Elim Rules in HOL slides (full sized PDF) (six up PDF) files Demo7.thy Feb 19 Basic Proof Methods slides (full sized PDF) (six up PDF) files Demo7.thy   Feb 24 Proof Methods and Intro to Set Theory slides (full sized PDF) (six up PDF) files Demo8.thy Feb 26 Inductive Sets slides (full sized PDF) (six up PDF) files Demo9.thy   Mar 3 Inductive Relations, General Recursive Functions No slides, demo continued from last time Mar 5 General Recursive Functions, New Type Definitions slides (full sized PDF) (six up PDF)   Mar 10 Records slides (full sized PDF) (six up PDF) files Demo11.thy, Mar 12 Locales slides (full sized PDF) (six up PDF) files Demo12.thy   Mar 17 SPRING BREAK Mar 19 SPRING BREAK   Mar 24 Control Flow Graphs in Isabelle files Start of induction example - Scratch.thy Mar 26 PTRANS No slides   Mar 31   Student's name   Topic             Apr 2   Student's name   Topic                   Apr 7   Student's name   Topic             Apr 9   Student's name   Topic            n   Apr 14   Round 2;   Preliminary Problem Statement in Isabelle   Student's name   Topic            C     Apr 16   Student's name   Topic                   Apr 21 Apr 23       i             Apr 28   s                   April 30   Kang, Zheng   Ramsey's Theorem   Maria Kotsifakou   Correctness of Loop Peeling< Node Copying/td>   Amarin Phaosawasdi<   Data Dependency in a Subset of C   Liyi Li  MSOS   Wenjie Zhu   Dead Code Elimination   May 5                    w