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.

Prerequisites

Logic in Computer Science (G22.2390-001, Fall '06) or equivalent.

Lectures

Wednesday 5:00pm-6:50pm in room 102 of Warren Weaver Hall

Office hours