Recursion and Induction -- CS 389r -- Syllabus


     Unique Number:  53182
 Class Room Number:  ENS 31NM
	Class Time:  Tuesday, Thursday, 11:00 to 12:20 pm

Reference Textbook:  Computer-Aided Reasoning:  An Approach
  Textbook Authors:  Kaufmann, Manolios, and Moore
 Purchase Location:  Lulu

	Instructor:  Warren A. Hunt, Jr.
   Office Location:  Main 2014
      Office Hours:  Thursday, 4:00 to 6:00 pm

This course concerns itself with the study of recursion and induction. This course will be broken into several parts. We will first learn something about the ACL2 logic (see We will write recursive definitions and use induction to analyze them. The next part of the course will be spent formalizing the syntax and semantics of a language to specify and decide Boolean functions. The remainder of the semester will be spent considering other topics involving the use of ACL2 to specify complex systems (e.g., SAT, hardware description language, regular expressions). Students may also present problems of general interest. Paperback copies of "Computer-Aided Reasoning, An Approach" by Kaufmann, Manolios, and Moore, which describes the ACL2 logic and its use, are available from Carol Hyink (who works in the Chairman's office) for $15.

A series of increasingly difficult problems will be assigned. Some of these problems will be discussed by students at the board. Class participation is expected, and student grades will, in part, reflect each student's contributions. Not showing up for class is a sure way to have the class-participation grade lowered. There will be one in-class exam. Each student will work on a project proposed by the student. Students will present their projects in class. There will be one exam given. Homework will be assigned each week, and it may be collected any time after its due date. The weighting of the grades for the various aspects of the course are: in-class exam - 25%, homework - 25%, class projects - 30%, and class participation 20%. The two lowest homework grades will be dropped in the computation of the final homework grade. Homework will not be accepted late. Projects may be turned in one week late with a 20% reduction of the grade given for the content of the project. The examination must be taken at the scheduled time.

Below is an approximate syllabus for the class. We will adjust the content to suit our pace and the interests of the class.

   Aug 30  Introduction -- Recursion and Induction -- so what?

   Sep  4  Using ACL2 for Modeling, Recursive Definitions
   Sep  6  Programming and modeling in ACL2
   Sep 11  ACL2 Logic presentation, data types, terms
   Sep 13  Axioms, terms as formulas
   Sep 18  Function Definition
   Sep 20  Substitution, abbreviations
   Sep 25  Principle of Definition
   Sep 27  Induction Principle, Examples

   Oct  2  Proof Examples
   Oct  4  Low-level representation of Boolean formulas
   Oct  9  Boolean formula semantics
   Oct 11  SAT
   Oct 16  Student project discussion
   Oct 18  Student project discussion
   Oct 23  ACL2 System Demonstration (Matt Kaufmann)
   Oct 25  Correctness of BDD package
   Oct 30  Quantified Boolean Formulas

   Nov  1  High-performance SAT
   Nov  6  High-performance SAT
   Nov  8  HDL syntax and semantics
   Nov 13  HDL syntax and semantics
*  Nov 15  In-Class Exam
   Nov 20  Exam discussion, Further discussion of SAT and HDL
   Nov 22  UT Holiday
   Nov 27  Free Topic
   Nov 29  Free Topic

   Dec  4  Student Presentations
   Dec  6  Student Presentations

In general, the information found in Code of Conduct is a good guide on how to conduct yourself in this class. Additional general information about College of Natural Sciences (CNS) class coursework and procedures can be found in Dean Laude's memorandum to the CNS faculty. Any scholastic dishonesty will be referred to the Dean of Students Office. The following passage is taken from the University of Texas at Austin Information Handbook for Faculty.

This course should comply with the requirements of the University and the State of Texas. Texas House Bill 2504 specifies a number of items regarding course materials and instructor qualifications. In addition, the material contained in the class webpages are designed to be compliant with Gretchen Ritter's (Vice Provost for Undergraduate Education and Faculty Governance) August 3, 2012, memorandum. Ritter's memorandum also addresses issues concerning campus safety and security. Please familiarize yourself with this information, and let me know if you believe the class Website does not comply with these requirements.

As a reminder, the "UT Honor Code" is included below.

I fully support the University's scholastic honesty policies, and I will follow the University's policies in the event of any scholastic dishonesty. If you are ever unsure whether some act would be considered in violation of the University's policies, do not hesitate to ask me or other University academic representatives.

Return to CS389r course homepage.