# CS 4860 Applied Logic - (Fall 2012)

## 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 10:10-11:25

**Location**: Upson 315

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

rc at cs dot cornell dot edu

Office: 4147 Upson Hall

Office Hours: Wed. 11:00-12:00 and by appointment

**Co-Instructor: Christoph Kreitz**

kreitz at cs dot uni-potsdam dot de

Office: 4114 Upson Hall

Office Hours: Tue. 1:00-2:00 and whenever the door is open

**Senior Teaching Assistant: Abhishek Anand**

Office: 4126A Upson Hall

Office Hours: Fri. 3:00-4:00 and by appointment

## Texts & Resources

### Required

*First-Order Logic*, by Raymond M. Smullyan

### Recommended Texts

*Computability & Logic,*G.S. Boolos, R.C. Jeffrey*Logic for Applications*, by Anil Nerode and Richard Shore (free on-line resource)*Proofs and Refutations*, by Imre Lakatos

### Resources

- See previous course web pages for CS 4860

## Homework Policies

Homework is to be brought to class or turned in to Prof. Constable's office, Upson 4147, before 5PM.

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.