Welcome to Applied Logic
CS/Math 4860 - Fall 2016 course

Course Narrative

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 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

• First-Order Logic, Raymond M. Smullyan.

Recommended

• Type Theory & Functional Programming, Simon Thompson.
• Computability & Logic, G.S. Boolos, R.C. Jeffrey, and J.P. Burgess.
• Logic for Applications, Anil Nerode and Richard Shore.
• Proofs and Refutations, Imre Lakatos.

Resources

See previous course web pages for CS/Math 4860:

• Spring 2001
• Spring 2003
• Spring 2005
• Spring 2009
• Fall 2010
• Fall 2012

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 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.

---