# CS 4860 Applied Logic - (Fall 2020)

## 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**: M/W 3:00 - 4:15

**Location**: Zoom only

**Instructor:**
**Robert Constable**

rc at cs dot cornell dot edu

Office: 320 Gates Hall

Office Hours: By appointment

## Texts & Resources

### Required

### Recommended Texts

- Intuitionistic Mathematics and Logic
- Understanding and Using Brouwer's Continuity Principle
- Nuprl Rules
*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/
- http://www.cs.cornell.edu/courses/CS4860/2019fa/

## Grading

See the Course Mechanics