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

1: January 18 (Friday)
Go through course syllabus.
A brief motivation for why to study this course, with an example (square root) illustrating that for the specification of software, First Order Logic (FOL) is very helpful, as is the notion of logical consequence.
Introduce "Tarski's World", using software package.
Before next time: read the introduction of LPL (the text book), start playing with the software, and preferably start reading a bit of Chap 1.
January 21 (Monday)
University Holiday (Martin Luther King)
2: January 23 (Wednesday)
Homework 1 out. The "submit" software was demonstrated.
We covered Chapter 1 of textbook. A number of worlds presented, together with corresponding variants of FOL (to be used as running examples throughout course).
Important concepts: individual constants (names), function symbols (with arity), predicates (with arity). Terms are built from constants and function symbols (can be nested); an atomic sentence is a predicate applied to one or more terms.
3: January 25 (Friday)
Using these slides, we covered Sections 2.1 and 2.5: an argument has a number of premises and one conclusion, and we distinguish between valid (some of which are also sound) and invalid arguments; counterexamples are used to demonstrate that a given argument is invalid (that is, the conclusion is "non-sequitur").
Do Exercises 2.4, 2.3, 2.8, 2.14, 2.22.
4: January 28 (Monday)
Using these slides, we covered Sections 2.2-2.4, giving examples of how to derive a conclusion from a set of premises, thereby demonstrating that the given argument is valid. For formal proofs, we use the deductive system F, implemented as the software Fitch (tuned for Tarski's world); we mention the Elimination and the Introduction rule for the identity predicate.
Demonstrate "Fitch", using Exercises 2.20 (part of HW1) and 2.17.
5: January 30 (Wednesday)
Homework 1 in. Homework 2 out.
Using these slides (except 17--20), we cover Chapter 3: Negation, Conjunction, Disjunction. Compare "\/" to "exclusive or". Ambiguities in FOL (and in English), and how to resolve them.
Do Exercises 3.28 & 3.15.
6: February 1 (Friday)
Start on Chapter 4, stating DeMorgan's laws which can be verified using truth tables, and also some other (tautological) equivalences: commutativity, associativity, distributivity, etc.
Using DeMorgan, and double negation, a sentence can be converted to Negation Normal Form (NNF).
Do Exercises 4.31(7) and 4.34.
7: February 4 (Monday)
Continue Chapter 4. The notion of a tautology. Using that \/ distributes over /\, a sentence can be converted into Conjunctive Normal Form (CNF), convenient for checking whether a tautology. Dually, we have Disjunctive Normal Form (DNF).
Do Exercises 4.17 and 4.41.
8: February 6 (Wednesday)
Finish Chapter 4. We introduce the notions of logical equivalence and TW-equivalence, forming a hierarchy (similar to Figure 4.1, p.102): for two sentences to be TW-equivalent they must be equivalent in Tarski's world; to be logically equivalent they must be equivalent in all possible worlds; to be tautologically equivalent they must be equivalent for all combinations of truth values (thereby in all possible worlds, and even some impossible worlds!) Similarly, we have a hierarchy of "necessities" (Figure 4.1), illustrated by Exercise 4.8, and a hierarchy of "consequences" which is reflected in the Fitch rules Taut Con, FO Con, Ana Con.
Graded Homework 1 back.
Last day for 100% refund for a course with 78 or more calendar days (10 or more weeks in length).
9: February 8 (Friday)
Homework 2 in. Homework 3 out.
Cover Chapter 5, introducing two crucial proof principles: proof by cases; proof by contradiction (indirect proof).
Do Exercises 5.1-5.7.
10: February 11 (Monday)
Cover Sections 6.1-6.3, presenting various elimination and introduction rules. Disjunction elimination corresponds to "proof by cases" (an example of which we see in Exercise 6.5); negation introduction corresponds to "proof by contradiction".
11: February 13 (Wednesday)
Go through model solutions for Homework 2.
Continue Chapter 6, using the rules given to construct proofs for 3 of the 4 arguments which constitute DeMorgan's laws.
Do Exercise 6.19, proving a general pattern which was used twice in Exercise 4.27.
Do Exercise 6.33, proving the law of Excluded Middle.
Last day for 50% refund for a course with 78 or more calendar days (10 or more weeks in length).
12: February 15 (Friday)
Homework 3 in. Homework 4 out. Graded Homework 2 back.
Work through Exercises 6.6 & 6.13 & 6.14 from Homework 3.
Finish Chapter 6, with more examples of how to construct proofs: the last (and most difficult) of the 4 arguments constituting DeMorgan's laws, and Exercise 6.28. Reminder: never reuse sentences from a subproof which has ended (Fitch actually prevents that).
13: February 18 (Monday)
Cover Section 7.1, introducing a new connective: "->" (which might be pronounced "implies").
Do Exercise 7.15(2,6,12); touch on Exercises 7.1, 7.2, 7.7, 7.21.
Motivated by the examples in Exercise 8.1, we show (cf. Sections 8.1 and 8.2) how to reason about -> as formalized by Elimination and Introduction rules; those are applied in Exercises 8.19 & 8.24, and also to establish the principle of contraposition (p.199).
14: February 20 (Wednesday)
Continue reasoning about ->, doing Exercises 7.6 and 8.35 (8.7).
Cover Section 7.2, introducing one more connective: "<->" (to be pronounced "if and only if", abbreviated "iff"); we touched upon Exercises 7.3 & 7.4.
Present Elimination and Introduction rules for <-> (cf. Sections 8.1 and 8.2); we did Exercise 8.27.
This Thursday (February 21) is last day to drop a course without a W being recorded for a course with 98 calendar days (14 or more weeks in length).
15: February 22 (Friday)
Homework 4 in. Homework 5 out. Graded Homework 3 back.
Wrap up the treatment of <->, in particular discussing how to prove a chain of biconditionals (cf. Exercises 7.8 and 8.15).
Introduce the notion of truth-functional completeness (Section 7.4), further illustrated by Exercise 7.30.
16: February 25 (Monday)
Motivated by Exercise 7.32, we state that the formal system F is sound, and also complete (Section 8.3, omitting the proofs of the theorems). This concludes Part I of the textbook.
Go through selected exercises from Homework 4: 6.20, 6.32, 8.25.
Do Exercises 8.48 and 8.50, showing the power and convenience of TautCon.
17: February 27 (Wednesday)
Graded Homework 4 back.
Embark on Lecture notes on Program Verification. Motivated by a program for computing the factorial function, we introduce the crucial notion of loop invariants, as described in Section 5 of the notes.
18: February 29 (Friday)
Briefly cover Sections 1-4 of Lecture notes on Program Verification: writing specifications as Hoare triples; the notions of partial correctness (never get a wrong result) versus total correctness (always get the right result); the three-stage approach to software engineering.
Apply the proof principles for program verification using loop invariants, stated in Sections 5.2 and 5.3 of Lecture notes on Program Verification, to programs (one inefficient, another efficient) computing the n'th power of x.
19: March 3 (Monday)
Present an example of how to develop a program together with its correctness proof, then show that the methodology even enables us to construct an efficient program (Section 6 of Lecture notes on Program Verification).
Amtoft has no office hours Tuesday.
20: March 5 (Wednesday)
Homework 5 in.
Discuss the general relationship between formal and informal proofs.
Cover Section 7 of Lecture notes on Program Verification: we introduce the notion of valid assertions (defined by proof rules); showing that a program is well-annotated is a formal and fine-grained way of proving its correctness.
We further illustrated the approach using Question 4 from Fall 2003, Exam III (solution here) for which we gave an informal correctness proof last Friday.
March 6 (Thursday)
4-4:45pm: Review session in N122.
21: March 7 (Friday)
Test I.
22: March 10 (Monday)
Homework 6 out.
Brief appetizer for Part II of the book: motivated by the desire to express the four Aristotelian forms (Section 9.5) in FOL, and later to handle program verification for complex data structures, we introduce variables (Section 9.1) and forall/exists quantifiers (Section 9.2).
Do selected parts of Exercises 9.16 & 9.17. We also address how to translate claims such as "at least two".
23: March 12 (Wednesday)
Graded Test I back, going through model solutions.
Continue (and finish) Chapter 9, getting more familiar with quantifiers. In addition to expressing the four Aristotelian forms, we address how to translate numeric claims such as "exactly one" or "at most one". Sketch the definition of a well-formed formula, abbreviated wff, and introduce the notion of free and bound variables (Section 9.3).
24: March 14 (Friday)
Homework 6 in. Homework 7 out.
Cover Sections 10.3 and 10.4, presenting DeMorgan as well as a number of other quantifier equivalences (summarized on p.282).
Observe that universal quantification can be expressed using existential quantification, at the price of adding two negations, as in the database query "find the companies which have customers in all states" which is equivalent to "find the companies such that there does not exist a state where they have no customers".
March 17-21
Spring (Easter) break
25: March 24 (Monday)
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). A first-order consequence (FO consequence for short) is an argument which remains valid if the predicates in question (except for the identity "=") are consistently replaced by other (even nonsense) predicates; the proof rules to be introduced in Chapters 12 and 13 enable us to prove all FO consequences (and nothing but FO consequences).
We looked into Exercises 10.1(3&5), 10.8, 10.13, 10.14, 10.18.
Last day to drop a course with 98 calendar days (14 or more weeks in length) with a "W".
26: March 26 (Wednesday)
Graded Homeworks 5 & 6 back; go through some of the model solutions.
Introduce the axiomatic method (Section 10.5) which enables us to prove consequences that (unlike first-order consequences) are due to the intrinsic meaning of predicate symbols, as illustrated by Exercise 10.30.
27: March 28 (Friday)
Homework 7 in. Homework 8 out.
Embark on Chapter 11, taking a closer look at English sentences whose translation into FOL requires both universal and existential quantification, for instance Exercise 11.16 (3) & Exercise 11.43 (3). Emphasis is (cf. Section 11.5) on the difference between "weak" (for all x there exists a y that works for that x) and "strong" (there exists a y that works for all x) readings of an English sentence: the corresponding translations are not FO-equivalent, though in certain cases they may be TW-equivalent. In general, the proper translation into FOL of an English sentence is often determined by context, as illustrated by Exercise 11.43 (1,2).
28: March 31 (Monday)
We finish Chapter 11 (not covering Section 11.7), looking at some interesting (and surprising!) translations from English to FOL: Finally, we show how to translate function symbols (Section 11.6, cf. Exercise 1.15).
29: April 2 (Wednesday)
We embark on proof rules for the quantifiers: Do Exercises 13.13 & 13.14 & 13.3.
30: April 4 (Friday)
Mention (Section 13.4) that our proof system is sound (thanks to side conditions requiring names to be fresh) and complete.
More examples of proofs (cf. Section 13.3) which use the newly introduced rules for quantifiers; we do three of the four "DeMorgan inferences".
Mention the method of General conditional proof (Section 12.3), reflected in the (other) Introduction rule for the Universal quantifier (Section 13.1).
31: April 7 (Monday)
Do the last "DeMorgan inference", showing Ex~P(x) from ~AxP(x). This inference (cf. p.355) is not accepted by "intuitionists" as it doesn't give us any clue about which x satisfies ~P; in general intuitionists don't like the ~Elim rule but we shall not follow their restricted approach!
Discuss the tricky interaction between existential instantiation and universal generalization (Section 12.4); we can prove "weak reading" from "strong reading" but (fortunately) not the other way round (due to the requirement that a boxed constant does not occur outside its subproof).
Continue the issue of axiomatization (Section 12.5), illustrated by comparing Exercise 13.32 (use of AnaCon) to Exercise 13.33 (use of an axiom).
32: April 9 (Wednesday)
Graded Homework 7 back; go through model solutions.
Homework 8 in; go through model solutions.
April 10 (Thursday)
4-4:45pm: Review session in N122.
33: April 11 (Friday)
Test II.
34: April 14 (Monday)
Discuss Test II, going through model solutions.
Prove the equivalence between two alternative ways of expressing "there exists at most one P" (something which probably cannot be done using the laws from Chapter 10), cf. Exercises 13.49 & 13.50 from the upcoming Homework 9.
35: April 16 (Wednesday)
Homework 9 out. Graded Test II back.
Verification of programs reading arrays, illustrated by developing a program for deciding whether an array is sorted (Section 8.1 in Lecture notes on Program Verification).
April 18 (Friday)
Class canceled (All-University Open House)
36: April 21 (Monday)
Do Exercises 12.28 and 12.13, presenting variants of the Catch-22 situation captured by "The Barber Paradox" (p.333) which has deep implications for modern mathematics in that it expels us from "Cantor's paradise": naive set theory leads to contradictions, as demonstrated by Exercise 13.52 which encodes Russell's paradox.
Do Exercise 12.37 where we give axioms for "MoreSides".
Specify and write a program for finding the maximum element of an array (Section 8.1 in Lecture notes on Program Verification).
37: April 23 (Wednesday)
Homework 9 in. Homework 10 out.
Verification of programs modifying arrays (Section 8.2 in Lecture notes on Program Verification).
Thursday April 24, Amtoft has office hours from 3pm to 4pm.
38: April 25 (Friday)
We embark on the exciting topic of mathematical induction (handing out lecture notes), a special case of which we have seen already in the proof principle for program invariants: if an assertion phi holds after zero loop iterations, and if phi holds after k+1 loop iterations provided that phi holds after k loop iterations, then phi holds after any number of loop iterations.
We cover Section 16.3 in the textbook, dealing with induction on natural numbers: if we prove Q(0), and prove that Q(n) implies Q(n+1), then Q holds for all natural numbers!
The textbook contains a minor error: 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. (We can start anywhere as long as we are consistent; to prove a formula for the sum of angles in an n-polygon we must start at three.)
Do Exercise 16.15.
39: April 28 (Monday)
Continue mathematical induction on natural numbers:
40: April 30 (Wednesday)
Homework 10 in. Homework 11 out.
We introduce immutable lists and show how to reason about this important data structure, cf. Section 3 in Lecture notes on Induction:
41: May 2 (Friday)
Graded Homework 9 back.
Verification of programs with procedures, using Section 9 in Lecture notes on Program Verification. Also show, using a board simulation, how to implement recursive procedures.
42: May 5 (Monday)
Show how the use of Hoare triples and quantifiers enables us to express secrecy of data as well as integrity of data, as described in Section 10 in Lecture notes on Program Verification.
43: May 7 (Wednesday)
Homework 11 in.
Go through model solutions for Homeworks 9 & 10.
As an appetizer for future encounters with logic (though not part of the exam material in this course), we introduce CTL (computation tree logic).
44: May 9 (Friday)
Review session, going through some previous exam questions.
Graded Homework 11 back; go through model solutions.
May 13 (Tuesday)
Final exam, 11:50am-1:40pm


Torben Amtoft