Captain's Log: Logical Foundations of Programming, Spring 2003

January 17

Introduction to course; Syllabus handed out. Why study this course? Gave example of how a property in safety critical systems may be encoded in FOL.
Before next time: read the introduction of LPL, start playing with the software, and preferably start reading a bit of Chap 1.

January 20

Student/University holiday (Martin Luther King)

January 22

Homework 1 out. Covered Sections 1.1-1.4 and Section 1.6.
Three worlds (including Tarski's world) presented, together with corresponding variants of FOL. Important concepts: constants, predicates with arity, atomic sentences. Briefly introduced the notion of sets.

January 24

Covered Sections 1.5 and 2.1 (and also bits from the rest of Chapter 2).
Function symbols. Valid and sound arguments. How to derive a conclusion from a set of premises.

January 27

Covered Sections 2.2-2.4.
Formal vs. informal reasoning. The formal deductive system F; the program Fitch. Elimination and introduction rule for the identity predicate.

January 29

Homework 1 in. Homework 2 out. Covered Section 2.5 and Sections 3.1-3.3.
The use of counterexamples to demonstrate non-consequence. Negation, Conjunction, Disjunction. Compared "\/" to "exclusive or". The game in Tarski's world.

January 31

Covered Sections 3.4-3.7 and Section 4.1 (also a bit of Sect. 4.2)
Ambiguities in FOL, and how to resolve them. The hierarchy of "necessities" in Figure 4.1. The notion of a tautology (a simple, though not very powerful, way to detect logical necessity), defined using truth tables.

February 3

Covered Sections 4.2-4.5 (and a bit of Sect. 4.6)
Tautological and logical equivalence. Listed useful laws, such as DeMorgan. Tautological and logical consequence, forming a hierarchy similar to the one of Figure 4.1 and reflected in the Fitch rules Taut Con, FO Con, Ana Con. Sentences in Negation Normal Form (NNF).

February 5

Homework 2 in. Homework 3 out. Covered Sections 4.6 and 5.1.
Notion of being "possible" (if negation not necessary). Using the distributive law, a sentence can be converted into Conjunctive Normal Form (CNF); then it's cheap to check whether it is a tautology.

February 7

Completed Chapter 5, and started on Chapter 6.
Two crucial proof principles: proof by cases; proof by contradiction (indirect proof). Elimination/introduction rule for conjunction.

February 10

Covered Sections 6.1-6.4 and Section 6.6. Brought up the issue whether (and how) to integrate lab sessions in the course (cf. p. 11); if no constructive alternatives are proposed we'll proceed as we've done so far.
Elimination and introduction rules for conjunction, disjunction, negation, contradiction. Notion of subproof; never reuse sentences from a subproof which has ended! A sentence which can be proved from no premises is a logical truth.

February 12

Homework 3 in. Homework 4 out.
Completed Chapter 6, working through some examples of how to construct proofs using the rules given.

February 14

Graded pen & paper part of Homework 2 back (general comments).
Exam I announced: Monday, March 3rd. (Details will follow.)
Cover Sections 7.1, 7.2, 7.4. Two new connectives: material conditional and biconditional. Notion of truth-functional completeness.

February 17

Covered Sections 8.1 and 8.2. Elimination and Introduction rules for -> and <->.

February 19

Homework 4 in. Homework 5 out.
Covered Section 8.3 about Soundness and Completeness (omitting the proofs of the theorems), thus completing Part I of the textbook. Commented on Exercises 4.8 and 4.27 from Homework 3.

February 21

Graded pen & paper part of Homework 3 back (general comments). Recalled the notion of tautology (p.103), logical necessity, tautological consequence (p.113), logical consequence, etc. Did Exercise 6.20.

February 24

Go through some exercises (mostly taken from Chapter 8) in the construction of proofs.

February 26

Homework 5 in.
Started on Part II of the book: motivated by the desire to express the four Aristotelian forms (Section 9.5) in FOL we introduced variables (Section 9.1) and forall/exists quantifiers (Section 9.2), resulting in the definition (p.231) of a well-formed formula (wff).

February 28

Comment on Homework 5. The notion of free and bound variables (Section 9.3).

March 3

Exam I.

March 5

Homework 6 out.
Wrapped up Chapter 9, in particular describing the semantics of the quantifiers (Section 9.4).

March 7

Truth and consequences in the presence of quantifiers: while the tautological approach is still of (limited) use (Section 10.1), we shall focus on the crucial notion of first-order consequence (Section 10.2) which will be captured by the proof rules introduced in Chapter 13. To prove consequences that are due to the intrinsic meaning of predicate symbols, one can use the axiomatic method (Section 10.5).

March 10

Graded Exam I back.

March 12

Homework 6 in. Homework 7 out.
Various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4). Highlights from Chapter 11 (Sections 11.1, 11.2).

March 14

More highlights from Chapter 11 (Sections 11.3, 11.6). Universal elimination and Existential introduction (Section 12.1), Existential instantiation (Section 12.2).

March 17-21

Student holidays (Spring break)

March 24

Recapitulate the method of Existential instantiation (Section 12.2). The method of General conditional proof (Section 12.3). The tricky interaction between these two methods (Section 12.4).

March 26

Homework 7 in. Homework 8 out.
Exam II announced: Wednesday, April 9th. (Details will follow.)
Introduction and Elimination rules for the Universal quantifier (Section 13.1); Introduction and Elimination rules for the Existential quantifier (Section 13.2).

March 28

No class (Open House activities).

March 31

Graded pen & paper part of Homework 6 back (general comments).
Examples of proofs with quantifiers (Section 13.3): derived the 4 DeMorgan inferences.

April 2

Homework 8 in.
Review selected parts of Homework 6: Exercise 10.1 (2,3,5); Exercises 10.10, 10.13, and 10.14. Review selected parts of Homework 7: Exercises 11.4 (3,5,7) and 11.17 (2,6,8).

April 4

Review Exercises 13.12, 13.28, 13.30, and 13.31 from Homework 8, and Exercise 11.19 from Homework 7.

April 7

Remember: we have now entered Daylight Saving Time!
Graded pen & paper part of Homework 8 back (general comments). Review Exercise 11.26 from Homework 7.
Mention that the full proof system is sound and complete (Section 13.4).

April 9

Exam II.
Homework 9 out.

April 11

Embark on Part III of the course, starting on Section 16.1. Motivated the concept of inductive definitions and inductive proofs (using the domino analogy).

April 14

Continue Section 16.1, considering the inductive definition of ambig-wffs (p.444). Prove by induction a couple of properties; for Proposition 2 (p.447) it turned out that we need to strengthen the induction hypothesis.

April 16

Homework 9 in. Homework 10 out.
Induction on natural numbers (Section 16.3): if we prove P(0), and prove that P(n) implies P(n+1), then P holds for all natural numbers! We saw an example (sum of angles in polygons) where the base case is '3' (rather than '0' or '1').
We spotted a rare error in the textbook: on p. 454, the first natural number is defined to be zero, but Proposition 4 only holds if the first natural number is assumed to be one.

April 18 (Good Friday)

Review Exercise 13.52.
More examples of induction on natural numbers; proving that every third fibonacci number is even required us to reformulate the induction principle allowing the inductive step to use not only P(n) when proving P(n+1) but also to use P(n-1), P(n-2), etc.
Brief reminder of how lists are recursively defined.

April 21

Graded Exam II back.
Distribute Additional notes on Induction.

April 23

Graded pen & paper part of Homework 9 back (general comments).
Induction principle for lists; see Additional notes on Induction.

April 25

Homework 10 in. (Solution key.)
Introduction to program verification: writing specifications; the notion of Hoare triples; the three-stage approach to software engineering. Reading material: Lecture notes on Program Verification (to be expanded so as to incorporate everything that is covered on that topic).

April 28

Homework 11 out.
Section 16.5 of LPL: program properties can be verified by induction in the number of times a loop is executed!

April 30

Emphasized the crucial role of loop invariants for program verification. Introduced the notion of a well-annotated program. Example program: one computing the factorial function. Reading material: Lecture notes on Program Verification (Section 4).

May 2

Continue covering Lecture notes on Program Verification: proof rules for valid annotations (Section 4.3); a further example of how to well-annotate programs (Appendix A).

May 5

Homework 11 in. (Solution key.)
Graded homework 10 back. (Solution key.)
Distributed the complete version of Lecture notes on Program Verification. Covered Section 5, giving an example of how to develop a program together with its correctness proof. (Typo p. 18,l.5: B should be B'.)
We have now covered all of the material of the course :)

May 7

Wrap up the course. Go through Homework 10.

May 9

Last day of semester.
Graded homework 11 back. (Solution key.)
One more example of the induction principle. And why induction cannot be used to prove that we can live forever ;)

May 12 (Monday)

Final exam, 11:50am to 1:20pm in N122.