### CS 378 Automated Reasoning

This course is intended to be an introduction to the research area of
automated reasoning, which concerns the effort to produce computer
programs that can produce proofs of mathematical theorems. We will
first look at what is perhaps the first example of a computer program
for checking proofs, namely that described by Goedel in the first few
pages of his famous paper on undecidable questions. We'll next look
at perhaps the most influential paper in the history of automated
reasoning, that by J. A. Robinson on the resolution method. Finally,
we'll consider a state of the art automated reasoning system, namely
Prover9 by Bill McCune, which uses the resolution method. The
textbook for the course will be *A Fascinating
Country in the World of Computing: Your Guide to Automated
Reasoning*, by Larry Wos and Gail Pieper, World Scientific,
www.worldscientific.com, ISBN 981-02-3910-6, 2000.

Students will be expected to undertake three projects from a list of
possibilities, including implementation of a proof checker as
specified by Goedel, implementation of a resolution theorem prover, or
explorations with McCune's Prover9 system, which may be obtained
freely on the Internet. Work with any of the many available reasoning
systems mentioned in the following web pages could also be projects:

For each such project the student will be expected to produce a
written paper at least six pages in length. These papers may require
multiple revisions, giving the student multiple opportunities to
strengthen the paper and to increase the grade.
P. S. This course would probably be no fun for someone who hated
CS/Phl 313K, but those who enjoyed the formalism of 313K may find the
challenges faced by the field of automated reasoning inspiring.

P. P. S. The University of Texas has many rules and regulations.
It is highly recommend that for all courses at the University of Texas
that students be familiar with the General Information Catalog, the
Course Catalog, and of course the Course Schedule, which can all be
found on-line at http://www.utexas.edu. Also highly
recommended is
http://cns.utexas.edu/faculty/files/2006CourseworkRoutine.pdf
,
Dean Laude's memo on Coursework and Routine: Policies, Procedures, and
Recommendations.