Location

Tue, Fri 1:35-3:15PM Hastings Suite 114

Contact Information

Professor: Pete Manolios
Office hours: WVH 346, Tue 3:15-4:15PM, Tue, Fri, and by request
Email:

Goals

By the end of this course, you will:

1. Understand the fundamental concepts and algorithms in the area of computer-aided reasoning.
2. Implement and evaluate a computer-aided reasoning system from scratch.
3. Be able to formalize computational systems at various level of abstraction.
4. Be able to effectively use a major theorem prover to mechanically prove non-trivial theorems about computational systems.

Course Structure

The course will consist mostly of lectures. At the end of the semester, we will have student presentations.

Textbooks

We will use the following textbooks

1. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press. The code accompanying the book can be found here.
2. Kaufmann, Manolios and Moore. Computer-Aided Reasoning. Buy the paperback version of the book, availalbe here.
3. Manolios. Reasoning about Programs.

Software

Install and familiarize yourself with the following.

1. The ACL2 Sedan
2. A Common Lisp compiler such as SBCL or Clozure Common Lisp
3. Emacs; the code for the emacs bindings I use in class.

Reference Material

The following links provide useful references. I may add more links during the semester.

1. The ACL2 Documentation
2. Steele. Common Lisp the Language, 2nd Edition. This is available online from various sources, including this one
3. Emacs
4. Data Definitions

Forum

I will provide a Piazza-Based Web forum that can be used by students to ask questions and exchange wisdom while completing the homeworks and projects in this course. You are expected to check it at least every few days, participate actively, and use it as a first place to post questions related to the projects or homeworks in this course. Please use the forum to post questions and answers that may be useful to others. Specifically, clarification questions about the homework, such as "What is the precise interpretation of homework question 2b" should be posted on the forum. Also, any questions at all about the material covered in class should be posted on the forum, e.g., "What do I wind up with when I apply Knuth-Bendix completion on this set of rewrite rules?"

Homework Assignments

This course will have regular project-based homework assignments requiring you to implement techniques and algorithms covered in class. Over the course of the semester, you will implement and evaluate a modular reasoning engine for a formal modeling language that can be used to model computational systems. Homework assignments will be done by groups of 2-3 students and will involve design, teamwork, and the implementation and evaluation of complex algorithms. To collaborate effectively, you should all be involved in all aspects of the homework problems. Homeworks will be marked 20 points off per day that they are late, up to 2 days. Important: You are responsible for finding a partner. The class forum located on Piazza is a particularly good resource for this, as there will be a thread there that serves exactly this purpose. Right before or right after lecture are also good times to look for partners. Submission instructions and more information can be found by clicking on the Assignments tab on the left. Any requests for grade changes or regrading must be made within 7 days of when the work was returned. To ask for a regrade, specify (a) the problem or problems you want to be regraded, and (b) for each of these problems, why you think the problem was misgraded.

Exams

There will be two exams. The first exam will be given approximately halfway through the semester and the second exam will be given towards the end of the semester. The first exam will be given on 10/23 and will be an in-class exam.

Presentations

Every student will pick 1-2 relevant research papers that they find interesting and will read and present them to the class. The presentation should include a motivation, it should relate the presented material to the material covered in class and it should explain why the topic is important and interesting.

Projects

Projects are required only for graduate students. Graduate students have to propose a project that I will review and approve. Projects allow you to gain hands-on experience on a topic of interest. I suggest first choosing a project topic and then selecting a paper on this topic for your presentation. Your project can be theoretical, say coming up with a new algorithm, or they can involve the implementation of an interesting algorithm, or they can involve the use and evaluation of existing tools.

Grading

The breakdown of the grades in this course for undergraduate students is as follows.

1. 40% Exams
2. 40% Homeworks
3. 10% Paper presentation
4. 10% Class participation

For graduate students grades are determined as follows.

1. 30% Exams
2. 30% Homeworks
3. 15% Paper presentation
4. 15% Project
5. 10% Class participation

Academic Integrity

It's OK to ask someone about the concepts, algorithms, or approaches needed to do the assignments. We encourage you to do so; both giving and taking advice will help you to learn. However, what you turn in must be your own, or for projects, your group's own work; copying other people's code, solution sets, or from any other sources is strictly prohibited, unless you are explicitly given permission to do so. In particular, looking at other solutions (e.g., someone else's solution to a similar project) is a direct violation of our academic integrity policy. The project assignments must be entirely the work of the students turning them in. If you have any questions about using a particular resource, ask me. All students are subject to the Northeastern Academic Integrity policy. All cases of suspected plagiarism or other academic dishonesty will be referred to the Office of Student Conduct and Conflict Resolution (OSCCR) and to the college. In addition to any penalties imposed by OSSCR and the college, each violation of the academic integrity policy will result in a full grade reduction for the class in addition to a zero grade on any affected assignments, projects, exams or graded material.

Accommodations for Students with Disabilities

If you have a disability-related need for reasonable academic accommodations in this course and have not yet met with a Disability Specialist, please visit the Northeastern Disability Resource Center and follow the outlined procedure to request services. If the Disability Resource Center has formally approved you for an academic accommodation in this class, please present the instructor with your "Professor Notification Letter" during the first week of the semester, so that we can address your specific needs as early as possible.

Schedule

The schedule below is preliminary and subject to change. Please read the material before class.

Week	Topics
9/3	L1. Introductions. Review of ACL2s, Defdata Intro, property-based testing. Slides, Code
9/10	Read Data Definitions, RAP: Chpts 1-6 L2. History ACL2, Defdata, ACL2s mode, Contracts, Static/dynamic checking, Definitions Slides, Code L3. Termination, Querying & Controlling ACL2s Slides, Code
9/17	Read CAR: Chpts 8-9, RAP: Chpt 7 L4. Equational reasoning, Induction, Lemmas, Generalization Slides L5. Organization of ACL2, waterfall, decision procedures, congruence-based reasoning Slides, Code
9/24	Read CAR: Chpts 5, 10-11 L6. Term rewriting, how to use the theorem prover, the method Slides, Code L7. State, world, Macros, using books, developing libraries, performace issues Code, Set Library
10/1	Read Harrison: Chpts 1, 2.1-2.6 (Can ignore OCaml code) L8. Propositional logic: syntax, semantics L9. Propositional logic: simplification
10/8	Read Harrison: Chpts 2.7-2.11 L10. Tseitin transformation, 2SAT, applications, SAT solving introduction Slides L11. BDDs, DP, DPLL Slides
10/15	Read Harrison: Chpts 3.1-3.6 L12. First order logic syntax and semantics, models, consequence, sat, validity Slides L13. Prenex normal form, Skolemization intro Slides
10/22	Read Harrison: Chpts 3.7-3.8 Exam 1 L14. Project presentations, Skolemization, Reducing FO validty to universal fragment & propositional unsatisfiability Slides
10/29	Read Harrison: Chpts 2.12, 3.9 L15. Propositional compactness, Herbrand Universes, FO checking Slides L16. Unification: algorithm, soundness, completeness, complexity, improvements, extensions, history Slides
11/5	Read Harrison: Chpts 3.11-3.14, 4.1 L17. FO checking with unification/resolution, subsumption, replacement, positive & semantic resolution, set of support Slides L18. Horn formulas, Logic programming, equality, ACL2: quantification, constrained functions, Skolemization, FO reasoning Slides, Code
11/12	Read Harrison: Chpts 4.2-4.3 L19. Sequent calculus, Henkin's theorem, Godel's completeness theorem Slides L20. Compactness, Lowenheim-Skolem, Theories, Axiomatization, Non-standard models, Godel's 1st incompleteness theorem Slides
11/19	Read Harrison: Chpts 4.4 L21. Equality decision procedure, Ackermann's reduction, congruence closure algorithm Slides
11/26	L22. Presentations L23. Presentations
12/3	L24. Presentations