Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 DAT060 Logic in Computer Science - 2007
25 Oct: Some asked for a systematic solution of Exercise 3 of the test exam. I did not think there was one, until one of you noticed that it is actually a covering
problem. So a systematic solution is actually the computation of a DNF of a formula.
17 Oct: Added one short note about something quite important on fixed-point
that I forgot to say in the last lecture (and which is on page 243 of the book)
17 Oct: the chapters that have been covered in the course (and required at the exams) are: Chapter 1
except 1.5.3 and 1.6, Chapter 2 except 2.6, 2.7 and Chapters 3: 3.1, 3.2, 3.4, 3.6.1, 3.7.The Section 3.6.2 is really nice, but is not required for the exam.
17 Oct: Added the solution of Exercise 6 of the test exam.
I made one mistake in the correction of Exercise 2: the CNF is simply not p /\ (not q\/ p) /\ (not r \/ q). (What
I computed was the Disjunctive Normal Form of the formula.) Also, in Exercise 8, I forgot some parentheses
in writing the second and third formula (I had forgotten that /\ binds more tightly than ->)
1 Oct: Added a short note on the reduction of the undecidability of predicate
logic by reduction to the Post Correspondence Problem here and a(n inefficient) Haskell program that tries to solve
the Post Correspondance Problem
1 Oct: Added a short note on another presentation of natural deduction
here and a test exam
30 Sept 8pm: Moved exercise session tomorrow (Oct 1st 10-12) will be in room MB! Apologies for late announcement.
19 Sept: Lecture Tuesday 25th of September is cancelled. The exercise session on Friday 28th of September is moved to the 1st of
October 10-12. (The room for the 1st of October is not clear yet since the
only person at the dept who can book rooms is on vacation until the 24th of
September. It will be posted as soon as possible.)
15 Sept: At the request of some students, a list of recommended exercises (with occasional commentary) will be maintained here as the course goes along. The recommended exercises are the same as the ones covered during the exercise sessions.
13 Sept: Since coursebook won't appear at Cremona until next week, here are pages 157-171 (exercises) from the book.
4 Sept: Since there was some delay with the coursebook at Cremona, here are pages 27 (basic rules of natural deduction) and 78-92 (exercises) from the book.
Goals of the course
The goal of the course is to present the fundamental basic
notions of logic that are important in computer science.
One presents propositional and predicate logic in natural deductions
the way it is done in most interactive theorem provers, with a
suggestive box notations for proofs. One presents also the basis of model checking and
temporal logic (LTL and CTL).
One does not cover a detailed proof of completeness theorem for predicate
logic (and one gives a sktech of completeness for propositional logic)
but what is important is that the students understand well the -meaning- of the
various completeness theorems. (On the other hand one gives a proof of
undecidability of predicate logic via Post systems.) In the same spirit,
one does not present complete proofs of decidability for LTL and CTL but
one presents in detail the fixed-point semantics of CTL.
The content of the course is roughly the 3 first chapters of
Huth and Ryan "Logic in Computer Science".
The text book is
``Logic in Computer Science''
by Michael Huth and Mark Ryan
Since there was some delay with the coursebook at Cremona, here are pages 27 (basic rules of natural deduction) and 78-92 (exercises), as well as more 157-171 (exercises).
Schema
Lectures
Tuesday 13.15 - 15:00 in EB
and Wednesday 10:00 - 11:45 in EB
At the request of some students, a list of recommended exercises (with occasional commentary) will be maintained here as the course goes along. The recommended exercises are the same as the ones covered during the friday exercise sessions.
Interesting links
An interactive introduction to
natural deduction for propositional and predicate calculus with several good examples
The chapter 7 of the book Artificial Intelligence: A Modern Approach
contains a brilliant introduction to propositional logic, complementary to the one
of the book of Huth and Ryan
A prover
to practise natural deduction (only for propositional logic)
A short note on how to decide an LTL formula. This is not required
for the exam, but I found the explanations in the book difficult to follow and wanted to have a method which
can be applied by hand on small examples.
A general presentation of some notions of the course and a nice
application of the use of temporal logic
Communications
Feel free to contact
Thierry Coquand,
in case you have any questions or problems. Almost
everything you get in the class is available electronically.
Send me a request if you have missed some stuff.