Course Information

Course Description

From very early on, philosophers have dreamed of machines that can reason. Leibniz first proposed the ambitious goal of mechanizing the process of human reasoning, saying, "Once this is done, then when a controversy arises, disputation will no more be needed between two philosophers than between two computers. It will suffice that, pen in hand, they sit down to their abacus and (calling in a friend if they so wish) say to each other: let us calculate." In this course we look at automated deduction within the context of first-order logic. We cover automated theorem proving techniques like resolution and rewriting. We also look at first-order theories for which the decision problem is decidable. We will cover a variety of problem domains and techniques and will also look at some applications.


Logic in Computer Science, or equivalent.


Wednesdays 7:10pm-9:00pm in room 317 of Warren Weaver Hall

Mailing List

Everyone in the class should subscribe to the email list, as this is where important announcements will be sent. To subscribe, visit the following URL:

Office hours

By appointment

Problem Sets & Exams

There are expected to be 3 graded homework sets and a final project. The final project will require a significant amount of programming effort, and a short, final presentation of your work in class.

There may be periodic ungraded homework sets, and they will be clearly marked as such. You are encouraged to work through them and check your answers against posted solutions, as they will help you with the course.

There are no exams.


Final grades will be based on the following:

50% Homework
50% Project


There is a textbook that will serve as a source for a lot of the information in the course. It is not necessary to buy a copy of this text.
It is available online through NYU Libraries.

Hickey's Introduction to Objective Caml is invaluable as an introduction or refresher to OCaml.

Other texts are used periodically through the semester, and will be made available as a handout, at the library, or online, and mentioned in the online notes. Homework submissions will be due on Wednesdays, the same night as class, and should be turned by 11:59pm (after class) on the date due. Any paper submissions should be made to me personally; electronic submissions are likely more convenient, though, and should be made to me at

Late homework submissions are subject to a penalty per day late, and severely late homework submissions (1 week) may or may not be accepted.

Honor Code

You may do problem sets any way that works best for you. It's best if you work on the problems yourself. You may discuss problem set questions with a partner or study group, but please indicate so on your submission. Your final write-up, and all code, must be your own.

Please review the department's academic integrity policy.

You are expected to submit original work - It is a violation of the policy to copy or derive specific solutions from anyone, from textbooks other than those noted for the course or the assignment, from the internet, or from previous instances of this course. Copying without giving appropriate acknowledgement is plagiarism, a serious offense with consequences ranging from no credit to potential expulsion.