CPMA 511: Logic and Proof
Fall 2009
Dr. Donald Simon
Office / Phone: 416 College Hall / 396-6472
E-mail: simon@mathcs.duq.edu
Office Hours: By appointment
Home page: http://www.mathcs.duq.edu/profs/simon.html
Text: Mathematical Logic for Computer
Science, Second Edition, by Mordechai Ben-Ari
There is a web page associated with the book at http://stwww.weizmann.ac.il/g%2Dcs/benari/books/#ml2
Course Objectives: In this course, we will discuss logic, focusing in on computational logics. We begin with a background of propositional and predicate calculus using semantic tableaux, systems of natural deduction and resolution methods to find proofs. We will use formal methods for verifying properties of simple programs. We conclude with work in temporal logics. We will use several automated tools such as Prover9 for resolution theorem proving, and ACL2 for program verification.
| Grading: | |
| Assignments | 80% |
| Final | 20% |
The grading scale is:
100-90 = A, 89-80 = B, 79-70 = C, 69-60 = D, below 60 = F.
Plus/minus grading will not be used.
There will be six homework and/or computer assignments, and a final. The final will be a take-home test assigned on the last day of class. There will be a week to complete the final.
Honor Policy: Students in this class fall under the mandate of the College of Liberal Arts plagiarism policy. Any student guilty of plagiarism will receive a grade of ``F'' for the course and will be reported to the Student Committee. Work done in this course is to be by the individual, not by a group.
Late Work: Late assignments will not be accepted for credit.
Students with Disabilities: Students with documented disabilities are entitled to reasonable accommodations if needed. If you need accommodations, please contact the Office of Freshman Development and Special Student Services in 309 Duquesne Union (412-396-6657) as soon as possible. Accommodations will not be granted retrospectively.
Tentative Schedule:
Date | Topic(s) | Readings |
|
| 1. | 8/27 | Introduction, Propositional Logic | Chaps. 1, 2, Homework #1 |
| 2. | 9/3 | Deductive Systems, Resolution | Chaps. 3, 4, Homework #2 |
| 3. | 9/10 | Predicate Calculus | Chap. 5, notes Homework #3, |
| 4. | 9/17 | Predicate Calculus Deduction | Chap. 6, Homework #4 |
| 5. | 10/1 | Resolution | Chap. 7, Prover9 home page, example 1, example 2, Prover9 manual Prover9 examples, Homework #5 |
| 6. | 10/8 | Program Verification, ACL2 | Chap. 9, Homework #6, ACL2 Version 2.5,
notes
|
| 7. | 10/15 | Temporal Logic | Chap. 11, Homework #7, Final out |
| 10/22 | Final due in |
| |