CS 4860 Applied Logic - (Fall 2019)
Overview
In addition to basic first-order logic, when taught by Computer Science this course involves elements of Formal Methods and Automated Reasoning.
Applied logic is increasingly important in mathematics, philosophy, and computer science. The course Applied Logic, is joint between Computer Science and Mathematics. This semester the course is taught by CS. It stresses how logic is an integral part of CS (AI, systems, program verification, programming languages). The course casts large parts of logic in terms of computability, formal specification, computer assisted verification, intelligent systems, and automated reasoning. These ideas are increasingly important in mathematics and philosophy as well.
Topics covered include propositional calculi, predicate calculi, formal number theory, programming logics, and type theory. The first lecture will provided an overview of the course and course mechanics.
Meeting Times:Tue/Thr 1:25pm - 2:40pm
Location: Thurston Hall 202
Instructor:
Robert Constable
rc at cs dot cornell dot edu
Office: 320 Gates Hall
Office Hours: By appointment
Texts & Resources
Required
- First-Order Logic, by Raymond M. Smullyan
Recommended Texts
- Implementing Mathematics with the Nuprl Proof Development System
- Type Theory and Functional Programming, by Simon Thompson
- Logic for Applications, by Anil Nerode and Richard Shore (free on-line resource)
Resources
- See previous course web page for CS 4860
- http://www.cs.cornell.edu/Courses/cs486/2001sp/
- http://www.cs.cornell.edu/Courses/cs486/2003sp/
- http://www.cs.cornell.edu/courses/CS486/2005sp/
- http://www.cs.cornell.edu/courses/CS4860/2009sp/
- http://www.cs.cornell.edu/courses/CS4860/2010fa/
- http://www.cs.cornell.edu/courses/CS4860/2018sp/
- http://www.cs.cornell.edu/courses/CS4860/2018fa/
Grading
See the Course Mechanics
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.