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.
Torben Amtoft