Automated Theorem Proving

Automated Theorem Proving brings together the disciplines of formal symbolic logic and computer programming. In this course, we cover the syntax and semantics of first-order logic. At the same time, we study ways of allowing sentences in first-order logic to be read by computer. When we get to procedures for proving sentences, we focus on those procedures which can are efficiently used by computers. The proof procedure which we concentrate on is called the tableau method. By the end of the semester, we have written a program which can prove any valid sentence in first-order logic.

At the end of the semester, each student does a project on a related topic which interests him or her. This semester, there are a lot of philosophy majors in the class so the topics they have chosen reflect that. Current final project topics for the 1997-98 class include:

• Using Knowledge in Verifying Sentences
• Automatic Creation of Graphical Displays of Proof Trees
• The Turing Test
• Natural Language Understanding and Generation