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

Lectures for CS 576: Topics in Automated Deduction (Spring 2010) Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Jan 20 Course Introduction & Introduction to Operational Semantics slides (full sized PDF) (six up PDF) files Demo1.thy Jan 22 Intro continued Slides continued from last time files Demo2.thy, assume style files Demo2.thy, isar style   Jan 27 Basic Isabelle syntax slides (revised) (full sized PDF) (six up PDF) Jan 29 Introducing new types and terms Revised slides continued from last time files Demo3.thy   Feb 3 Rewriting Simplification slides (full sized PDF) (six up PDF) files Demo4.thy Feb 5 Basic Introduction and Elimination Rules in HOL slides (full sized PDF) (six up PDF) files Demo5.thy   Feb 10 Introduction and Elimination Rules in HOL (cont) slides (full sized PDF) (six up PDF) files Demo6.thy Feb 12 Introduction and Elimination Rules in HOL (cont) slides (full sized PDF) (six up PDF)   Feb 17 Quantifier Intro and Elim Rules in HOL slides (full sized PDF) (six up PDF) files Demo7.thy Feb 19 slides Contiuned from last time   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 slides (full sized PDF) (six up PDF) Mar 5 General Recursive Functions, New Type Definitions slides (full sized PDF) (six up PDF)   Mar 10 Isar Overview slides (full sized PDF) (six up PDF) files IsarDemo1.thy, IsarDemo2.thy Mar 12 New Types, Records Slides continued from lecture 14 files Demo10.thy   Mar 17 Records files Demo11.thy Mar 19 Locales files Demo12.thy   Mar 24 SPRING BREAK Mar 26 SPRING BREAK   Mar 31 Example presentation of a project Apr 2 William TRANS and SSA Dennis Myhill-Nerode Nathan Linear Logic Edgar INS   Apr 7 James Concurrent Game Structures Vijay ATL* Matt ATL Sridhar Needham-Schroeder Apr 9 Core ML Dongyun PTLTL Francisco Owicki-Gries   Apr 14 William TRANS and SSA -- Excused because of seminar Dennis Myhill-Nerode Nathan Linear Logic Edgar INS Apr 16 James Concurrent Game Structures Vijay ATL* Matt ATL   Apr 19 Sridhar Needham-Schroeder Dongyun PTLTL Francisco Owicki-Gries Core ML -- ? Apr 21 William TRANS and SSA -- Excused because of seminar Dennis Myhill-Nerode Nathan Linear Logic Edgar INS   Apr 28 James Concurrent Game Structures Matt ATL Core ML Apr 30 Sridhar Needham-Schroeder Vijay ATL* Dongyun PTLTL Francisco Owicki-Gries   May 5 William TRANS and SSA Dennis Myhill-Nerode Nathan Linear Logic Edgar INS