CS U290: Logic and Computation
Spring 2008
[Main Page]
[Lectures]
[Assignments]
CS U290 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
We will use the following textbook.

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.
Tentative Syllabus
Here is an overview of the material that we expect to cover. We
reserve the right to make modifications.
 The ACL2 programming language
 Data types
 Primitive functions
 Defining functions
 Common recursions
 Tail recursion
 Multiple values
 Mutual recursion
 Macros
 Assertions and testing
 The ACL2 logic
 Quantifierfree first orer logic
 Axioms of ACL2
 Equational Reasoning
 Recursive definitions and the definitional principle
 Induction
 Quantification
 Termination
 Godel's completeness theorem
 Mechanization of ACL2
 Organization of ACL2
 Simplification
 Decision procedures
 Proof techniques
 The method
 Inspecting failed proofs
 Proof strategies and modularity
 Applications
 Data Structures
 Logic Design
 Compilers
 Video Games
 ...