CS 2800 is a 4-credit 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
There is no required textbook. I will be providing lecture notes.
There is however an optional book that students may find useful.
The book is written for upper level undergraduate students, but
it is the best reference for ACL2 currently available.
-
Computer-Aided
Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother
Moore. Kluwer Academic Publishers, June, 2000. (ISBN: 0-7923-7744-3)
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.
- Introduction to the ACL2 programming language and review of 211
- Design recipe and review of how to design programs
- ACL2 data types
- ACL2 primitive functions
- ACL2 programming idioms
- Defining functions in ACL2
- Totality and termination
- Formalizing data definitions
- Common recursion schemes
- Tail recursion
- Formalizing pre and post conditions
- Testing
- Propositional Logic
- Basic connectives from a computational viewpoint
- Truth tables
- Satisfiability and validity
- Proof techniques (including case analysis, deduction law, instantiation)
- Equational reasoning
- Algorithmic considerations: completeness, exhaustive
testing, decision procedures
- Using propositional logic to reason about programs
- The Basic ACL2 Logic
- Variables, equality, functions
- Quantifier-free first order logic
- Specifying properties of programs
- Axioms of ACL2
- Substitution
- Equational reasoning
- Definitional principle
- Termination
- Recursion
- Induction
- Generalization
- Proving programs correct
- Quantification and its relation to recursion
- Algorithmic considerations: exhaustive testing,
completeness, incompleteness, undecidability
-
- Effective Use of the ACL2 Theorem Prover
- Organization of ACL2
- Simplification
- Decision procedures
- The method
- Inspecting failed proofs
- Proof strategies and modularity
- Applications
- Basic data structures
- Logic design
- Program equivalence
- Video games