CS 2800 is a 4credit course. The
Office of
the Registrar has useful information.
Course Description
Introduces formal logic and its connections to computer and
information science. Offers an opportunity to learn to translate
statements about the behavior of computer programs into logical
claims and to gain the ability to prove such assertions both by
hand and using automated tools. Considers approaches to proving
termination, correctness, and safety for programs. Discusses
notations used in logic, propositional and first order logic,
logical inference, mathematical induction, and structural
induction. Introduces the use of logic for modeling the range of
artifacts and phenomena that arise in computer and information
science.
Textbooks

ComputerAided
Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother
Moore. Kluwer Academic Publishers, June, 2000. (ISBN: 0792377443)
Note: An updated paperback version is
available on the Web. This is much cheaper than the hardcover
version.
Please
note that the book was written for at least upper level
undergraduate students, so expect parts of the book to be
hard. Nevertheless, this is the standard reference for ACL2 and
contains many exercises whose solutions are available
online. Use it as a reference and use it to supplement lectures.