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
Welcome to Applied Logic
CS/Math 4860  Fall 2016 course
Course Narrative
In addition to basic firstorder logic, when taught by Computer Science this course involves elements of Formal Methods and Automated Reasoning.
Formal Methods is concerned with proving properties of algorithms, specifying programming tasks and synthesizing programs from proofs.
We will illustrate formal methods tools such as interactive proof assistants (see www.nuprl.org).
We will also discuss constructive type theory, the language used by the Coq and Nuprl proof assistants.
CS Topics include:
 formal methods
 automated reasoning

interactive proof assistants

constructive type theory
Instructor
Professor Robert Constable
320 Gates Hall
Office Hours: After class and by appointment
email: rc at cs dot cornell dot edu
Time: Tues/Thurs 1:25PM  2:40PM
Location: Rockefeller Hall 112
Prerequisites
Prerequisites: Math 2210  Math 2220, Math 2230  Math 2240, or Math 1920 and Math 2940; CS 2800 (or Math 3360, Math 4320, Math 4340, or Math 4810); and some additional courses in mathematics and computer science.
Texts & Resources
Required
 FirstOrder Logic, Raymond M. Smullyan.
Recommended
Resources
See previous course web pages for CS/Math 4860:
Grading
TBA
Homework Policies
Cornell University has a Code of Academic
Integrity, with which you should be familiar. Violations of this code are
treated very seriously by Cornell and can have longterm repercussions. In
this course, you are encouraged to discuss the content of the course with
other students, and you may also discuss homework problems with other students.
However, you must do your own work, write up assignments yourself, and if you
discuss a problem with another student, you are expected to document this
fact in your writeup. It is a violation of the code to copy work, including
programs, from other students; it is also a violation to use solutions to
homework problems from previous iterations of the same course. Note that
Cornell holds responsible for the code violation both the recipient and
the donor of improper information.