CS/Math 4860 :: Applied Logic

CS/Math 4860 Fall 16:

Announcements:

11/11/16: Course projects will be accepted from Dec 1 until 5pm Dec 6.

9/23/16: A Nuprl demonstration for the course will occur in Gates Hall room 114 at 4 PM. Attendance is expected.

9/13/16: No class meeting on 9/15/2016 .

7/20/16: A short detailed description of the course can be found here.

Instructor:

Robert Constable

Time:

Tues/Thurs

1:25PM - 2:40PM

Location:

Rockefeller Hall 112

Schedule & Notes
CS/Math 4860 - Fall 2016

Date Topic Notes/Readings
August 23 Introduction to Course
August 25 Introduction to Course Topics
August 30 Introduction to Boolean Propositional Logic
Sept. 1 Chapter 1 of First-Order Logic and an introduction to polymorphic types
Sept. 6 Tableaux Rules
Sept. 8 Refinement Rules
Sept. 13 Lecture 7
Sept. 15 Reading (no class 9/15/2016)
Sept. 20 Review of Smullyan's Trees
Sept. 22 König's Lemma and the Fan Theorem
Sept. 23 Nuprl Demonstration
Sept. 27 Lecture 10
Sept. 29 Developing a Theory of Polymorphic Programming Logics
October 4th First Order Logic
October 6th First Order Tableaux
October 13th Tableaux Rules
October 18 Tableaux Completness
October 20 Consistency and Completeness
October 25 Non-Standard Models
October 27 Reals, Hyperreals, and Infinitesimals
November 1 Primitive Recursive Arithmetic
November 3 Introduction to Constructive Mathematics
November 8 Introduction to Constructive Mathematics - II
November 10 Constructive FOL
November 15 The Constructive Reals
November 17 Constructive Type Theory
November 22 Discussion of Course Projects
  • Lecture 25
November 29 Constructive Type Theory - Continued
December 1 Finding Computational Content and Course Summary