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:
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.