Captain's Log: Logical Foundations of Programming, Fall 2007

1: August 20 (Monday)
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.
2: August 22 (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.
No office hours, or review session, today.
August 24 (Friday)
Class canceled (Instructor out of town)
August 27 (Monday)
Class canceled (Instructor out of town)
3: August 29 (Wednesday)
Homework 1 in.
Using these slides, cover 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.
No review session today.
4: August 31 (Friday)
Homework 2 out. Go briefly through comments on Homework 1.
Using these slides, cover 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). Elimination and introduction rule for the identity predicate. Demonstrate "Fitch", using Exercise 2.20 (part of HW2).
September 3 (Monday)
Labor Day: student/university holiday
5: September 5 (Wednesday)
Using these slides (except 18--21), cover Chapter 3: Negation, Conjunction, Disjunction. Compare "\/" to "exclusive or". Ambiguities in FOL (and in English), and how to resolve them.
Do Exercises 2.7, 3.19, 3.15. Graded Homework 1 back.
6: September 7 (Friday)
Homework 2 in. Homework 3 out (including Quiz 1).
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), 4.34, and 4.17.
7: September 10 (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 Exercise 4.43.
8: September 12 (Wednesday)
Graded Homework 2 back; go through some model solutions.
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.
Today's review session will be from 5:30pm to 6:00pm (still in N122).
9: September 14 (Friday)
Homework 3 in. Homework 4 out.
Cover Chapter 5, introducing two crucial proof principles: proof by cases; proof by contradiction (indirect proof). (Do Exercises 5.1-5.7.)
10: September 17 (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: September 19 (Wednesday)
Continue Chapter 6, working through some examples of how to construct proofs using the rules given, for instance for 3 of the 4 arguments which constitute DeMorgan's laws. Reminder: never reuse sentences from a subproof which has ended (Fitch actually prevents that).
Do Exercises 6.28 and 6.19; the latter proves a general pattern which was used twice in Exercise 4.27.
12: September 21 (Friday)
Homework 4 in. Homework 5 out. Graded Homework 3 back; go through some model solutions.
Finish Chapter 6, with more examples of how to construct proofs: Exercise 6.33 (excluded middle), and the last (and most difficult) of the 4 arguments constituting DeMorgan's laws.
Cover Section 7.1, introducing a new connective: "->" (which might be pronounced "implies"). Touch on Exercises 7.1, 7.2, and 7.6; briefly touch on Exercise 7.21.
13: September 24 (Monday)
Cover Section 7.2, introducing one more connective: "<->" (to be pronounced "if and only if", abbreviated "iff"). Touch on Exercises 7.3, 7.4, 7.7, 7.8.
Cover most of Sections 8.1 and 8.2: motivated by the examples in Exercise 8.1, we show how to reason about -> as formalized by Elimination and Introduction rules; those are applied in Exercises 8.24 & 8.19, and also to establish the principle of contraposition (p.199).
14: September 26 (Wednesday)
Finish Sections 8.1 and 8.2: Elimination and Introduction rules for <->, in particular, discuss how to prove a chain of biconditionals (cf. Exercise 8.15). Do Exercises 8.27 & 8.35 (8.7)
15: September 28 (Friday)
Homework 5 in. Graded Homework 4 back (briefly touching on model solutions).
Introduce the notion of truth-functional completeness (Section 7.4), further illustrated by Exercises 7.26 & 7.30.
Do Exercise 8.48, showing the power and convenience of TautCon.
October 1 (Monday)
Student holiday
16: October 3 (Wednesday)
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.
Do Exercise 8.50, again showing the power and convenience of TautCon, and Exercise 8.29.
Graded Homework 5 back (briefly touching on model solutions).
17: October 5 (Friday)
Test I.
Homework 6 out.
18: October 8 (Monday)
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.
19: October 10 (Wednesday)
Graded Test I back.
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 the program from Question 4 in Fall 2003, Exam III (where a formal proof was required; we did an informal).
20: October 12 (Friday)
Homework 6 in. Homework 7 out.
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).
21: October 15 (Monday)
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 Wednesday.
22: October 17 (Wednesday)
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). We also address how to translate claims such as "at least two".
23: October 19 (Friday)
Homework 7 in. Homework 8 out. Graded Homework 6 back.
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). Do (parts of) Exercises 9.16 & 9.17.
24: October 22 (Monday)
Cover Sections 10.3 and 10.4, presenting DeMorgan as well as a number of other quantifier equivalences (summarized on p.282).
25: October 24 (Wednesday)
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).
The axiomatic method (Section 10.5) enables us to prove consequences that (unlike first-order consequences) are due to the intrinsic meaning of predicate symbols.
We looked into Exercises 10.1(3&5), 10.8, 10.13, 10.14, 10.18.
26: October 26 (Friday)
Homework 8 in.
Wrap up the axiomatic method (Section 10.5), doing Exercise 10.30.
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).
27: October 29 (Monday)
Homework 9 out. Graded Homework 7 back.
Continue Chapter 11, with emphasis (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.
We encounter a "donkey sentence" (p.301) which has to be paraphrased before it becomes obvious how to translate it: even though the sentence strongly suggests the use of an existential quantifier, this will not work and we have to use a universal quantifier instead.
28: October 31 (Wednesday)
Graded Homework 8 back, going through model solutions.
We wrap up Chapter 11 (not covering Section 11.7) by doing Exercise 11.18(2&5), by discussing function symbols (Section 11.6, cf. Exercise 1.15), and by Exercise 11.45 which considers two seemingly non-equivalent English sentences and shows them to be equivalent: here, the key part is our ability to infer Ex~P(x) from ~AxP(x); observe that claiming ExQ(x) does not entail that we have any idea about the name of the object satisfying Q!
29: November 2 (Friday)
Test II
30: November 5 (Monday)
We embark on proof rules for the quantifiers: Do Exercises 13.13 & 13.14 & 13.3.
31: November 7 (Wednesday)
Mention the method of General conditional proof (Section 12.3), reflected in the (other) Introduction rule for the Universal quantifier (Section 13.1).
Mention that our proof system is sound and complete (Section 13.4).
More examples of proofs which use the newly introduced rules for quantifiers (cf. Section 13.3): three of the four "DeMorgan inferences".
32: November 9 (Friday)
Homework 9 in.
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 (cf. Question 4 of test II) the issue of axiomatization (Section 12.5), illustrated by comparing Exercise 13.32 (use of AnaCon) to Exercise 13.33 (use of an axiom).
33: November 12 (Monday)
Homework 10 out. Graded Test II back.
Wrap up Chapters 12 & 13:
34: November 14 (Wednesday)
Verification of programs reading arrays, in particular develop a program for finding the maximum element of an array (Section 8.1 in Lecture notes on Program Verification).
35: November 16 (Friday)
Verification of programs modifying arrays (Section 8.2 in Lecture notes on Program Verification). Also develop a program that decides whether an array is sorted.
36: November 19 (Monday)
Homework 10 in. Homework 11 out.
Wrap up the previous weeks: look at the challenging exercises 11.20 & 11.26 from Homework 9; do Exercise 13.52 which encodes Russell's paradox; do Exercise 12.37 where we give axioms for "MoreSides".
A brief appetizer, proving a formula for the sum of angles in an n-polygon, for the "induction" principle.
November 21-23 (Wednesday-Friday)
Thanksgiving holiday
37: November 26 (Monday)
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.
Do Exercise 16.15.
Amtoft has no office hours today, due to Landon lecture.
38: November 28 (Wednesday)
Graded Homework 10 back, mentioning Exercise 12.15 and Exercise 7.
Continue mathematical induction on natural numbers. Look at Exercise 16.18 from the upcoming homework; we realized that the result cannot be proved as it is and that we need to prove a stronger property, telling not only that the sum of the first n cubes is a square but also what it is the square of!
Define the fibonacci function on natural numbers. Using the golden ratio, we can state (and prove) a formula for the value of the n'th fibonacci number, something which would be virtually impossible to do without the induction principle (a slightly different formulation of which is required, cf. Section 2.1 in Lecture notes on Induction).
Do Exercise 16.1 (induction is a pleasant principle!) and Exercise 16.2 (where premises are inconsistent).
39: November 30 (Friday)
Homework 11 in. Homework 12 out.
We introduce immutable lists (cf. Section 3 in Lecture notes on Induction):
40: December 3 (Monday)
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.
41: December 5 (Wednesday)
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.
Graded Homework 11 back.
42: December 7 (Friday)
Homework 12 in.
Go through model solutions for Homework 11 and Homework 12.
As an appetizer for future encounters with logic (though not part of the exam material in this course), we briefly introduce CTL (computation tree logic).
December 10 (Monday)
Review session CANCELED due to inclement weather forecast.
December 12 (Wednesday)
Final exam, 11:50am-1:40pm.


Torben Amtoft