CS 4860 Applied Logic

Announcements

1/22/2018 - Introduction to the course
1/29/2018 - The course text First-Order Logic is available online through Cornell
2/5/2018 - Problem Set 1 is due in class 2/8/2018
2/13/2018 - Problem Set 2 is due in class 2/15/2018
2/27/2018 - Problem Set 3 is due in class 3/13/2018
3/2/2018 - Problem Set 3 has been updated
3/7/2018 - Lecture permanently reloacted to Thurston 202
3/27/2018 - Problem Set 4 is due in class on 4/12/2018
4/17/2018 - Problem Set 5 is due in class on the last day of lecture, 05/08/2018.
5/14/2018 - The final exam will be held on Tue May 22 from 2pm to 4pm in Rockefeller Hall 104
5/14/2018 - Final Exam Study Guide
5/14/2018 - Course Review
5/16/2018 - Final Exam Example Problems
5/18/2018 - Final Exam Materials - to be handed out with the exam booklet
5/20/2018 -The exam will cover only basic material on the constructive reals, and only topics in Bishop and Bridges from page 18 to 28. So the posted material in Lecture 21 but not from Lecture 22.

Overview

In addition to basic first-order 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 use formal methods tools such as interactive proof assistants (see www.nuprl.org).

We will also spend two weeks on 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

Meeting Times:Tue/Thr 1:25pm - 2:40pm

Location: Thurston 202

Instructor: Robert Constable
rc at cs dot cornell dot edu
Office: 320 Gates Hall
Office Hours: TBA

TA: Siva Somayyajula
sks266 at cornell dot edu
Hours: See the calendar

Texts & Resources

Required

First-Order Logic, by Raymond M. Smullyan

Resources

Homework Policies

Homework is to be brought to class.

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 long-term 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 write-up. 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.

CS 4860 Applied Logic - (Spring 2018)