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 (G22.2390-001, Fall '06) or equivalent.
Wednesday 5:00pm-6:50pm in room 102 of Warren Weaver Hall