Logic and Proof

CPMA 511: Logic and Proof

Fall 2001

Dr. Donald Simon
Office / Phone: 416 College Hall / 396-6472
E-mail: simon@mathcs.duq.edu
Office Hours:MT 5:00-6:00

Text: Logic in Computer Science: Modelling and reasoning about systems by Michael R. A. Huth and Mark D. Ryan

There is a web page associated with the book at http://www.cis.ksu.edu/~huth/lics and also at www.cs.bham.ac.uk/research/lics.

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 both a system of natural deduction and resolution methods to find proofs. We will also discuss computational tree logic (CTL) and several other modal logics. We will use formal methods for verifying properties of simple programs. We conclude with work in axiomatic set theory including the continuum hypothesis. We will use several automated tools: Otter for resolution theorem proving, SMV for CTL, and ACL2 for program verification.

Grading:
Assignments	65%
Mid-term	10%
Final	25%

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, a mid-term, and a final.

Honor Policy: See the College of Liberal Arts policy for scholastic dishonesty. Any student guilty of plagiarism will receive a grade of ``F'' for the course. Work done in this course is to be by the individual, not a group. You may not share (copy, give, show) your homework with other students in the course.

Late Work: Late assignments will not be accepted for credit.

Tentative Schedule:

Date
Topic(s)
Readings

1. 8/28 Introduction, Propositional Logic H & R, Chap. 1.

2. 9/4 Predicate Logic, Resolution, Otter H & R, Chap. 2, notes Otter home page, notes, example, Otter manual

3. 9/11 Model Checking, SMV H & R, Chap. 3

4. 9/18 Program Verification, ACL2 H & R, Chap. 4, ACL2 Version 2.5, notes

5. 9/25 Modal Logics H & R, Chap. 5

6. 10/2 Higher Order Logic Mike Gordon on HOL in pdf

7. 10/9 Axiomatic Set Theory ZFC axioms, Infinite Sets

	Date	Topic(s)	Readings

1.	8/28	Introduction, Propositional Logic	H & R, Chap. 1.
2.	9/4	Predicate Logic, Resolution, Otter	H & R, Chap. 2, notes Otter home page, notes, example, Otter manual
3.	9/11	Model Checking, SMV	H & R, Chap. 3
4.	9/18	Program Verification, ACL2	H & R, Chap. 4, ACL2 Version 2.5, notes
5.	9/25	Modal Logics	H & R, Chap. 5
6.	10/2	Higher Order Logic	Mike Gordon on HOL in pdf
7.	10/9	Axiomatic Set Theory	ZFC axioms, Infinite Sets

Last modified: Sept. 4, 2001

Dr. Donald L. Simon, simon@mathcs.duq.edu