UPPSALA UNIVERSITET
Matematiska institutionen
Datavetenskapliga programmet
| Höstterminen 2002
|
Tillämpad Logik DV1 (Applied Logic)
General information
-
Kursinformation/Course information ( ps-fil
| PDF-fil )
- Language: the lectures, exercises and exam are
given in English.
The main lecture notes (Konstruktiv logik, oavgörbara
problem ..., and Fullständighetssatsen ...) are however in Swedish. In the Course
information
above and Further reading below I indicate where the same material
can be found in English literature. Ask the librarians for help to
find the books.
Lectures
- Lecture plan and schedule
- Further reading (and alternative
sources
in English) sorted by lecture
- Lecture notes: Oavgörbara problem i elementär aritmetik
( ps-fil
| PDF-fil )
- Lecture notes:
Konstruktiv logik, kap 1-9 ( ps-fil
| PDF-fil ).
-
Constructive mathematics, 12 pp.,
August 22, 1997.
Lectures notes for Copenhagen Logic Summer School, 11-22 August, 1997.
(This is a brief, first introduction to the foundations of constructive
mathematics.)
- Lecture notes: Fullständighetssatsen för predikatlogik
via sekventkalkylen, by Inger Sigstam. (For sale at
UTH.)
- Decidable problems in geometry (Quantifier elimination
in Mathematica 4.0)
- Supplementary material on term rewriting and termination:
( ps-fil
| PDF-fil ).
- Supplementary material on the logical background to resolution:
( ps-fil
| PDF-fil ).
Exercise classes
- Exercises 1 ( ps-fil
| PDF-fil ).
Bonus point
- Exercises 2 ( ps-fil
| PDF-fil ).
Bonus point for 50% of 2.1(d), 2.1(e), 2.1(h). 2.2(b),
2.3(a)., 2.6(c).
- Exercises 3 ( ps-fil
| PDF-fil ). No bonus
exercises this week.
- Exercises 4 ( ps-fil
| PDF-fil ).
Bonus point for 50% of 4.1, 4.2, 4.5,
4.6, 4.7, 4.8.
- Exercises 5 ( ps-fil
| PDF-fil ).
Bonus point for 50% of 4.3, 4.4, 5.1 - 5.5.
- Exercise Exam 2002-10-08 (Övningstenta) ( ps-fil
| PDF-fil ).
Errata:
the case distinction in the recursive definition of f
in problem 6 (or rather 7!) is not complete. Fix this
by letting f(0,y,z) = 0 and f(S(x),0,z) = S(0) for
instance. The point of the problem was to illustrate
the use of well-founded relations in termination proofs.
Old exams
- Tentamen 2000-10-20 ( ps-fil
| PDF-fil ). Problem 4 and
6 covers some material that we have not treated in detail.
- Tentamen 2001-10-17 ( ps-fil
| PDF-fil ). Problem 6 and
7 covers some material that we have not treated in detail.
- Tentamen 2002-10-17 ( ps-fil
| PDF-fil ).
Laboratory work
The laboratory exercises are compulsory, and have to be handed in by
October 10 for an opportunity to correct errors and get feedback. It is also
possible to hand them in October 17, but then there will be
no feedback.
There will be one guided laboratory session on
September 19, 8.15-12.00 in room 4408 (the computers
in 4407 are too slow), which you are recommended to
attend. Prepare by studying the examples carefully.
It is also possible to
download the Alfa/Agda-system for
variety of unix-based based platforms.
See the problems from previous year
(don't do these!!):
-
Anvisningar för laboration 1, ht 2001
( ps-fil
| PDF-fil )
-
Alfa-filer för laboration 1 finns
här.
-
Anvisningar för laboration 2, ht 2001
( ps-fil
| PDF-fil )
-
Alfa-filer för laboration 2 finns
här.
Examination
The course ends with a written exam on October 17.
Remember to sign up for the exam at least 14 days
before the
exam
date, that should be October 3 at the latest.
You are permitted to bring certain texts and limited notes to the exam
(see the Exercise Exam 2002-10-08 above).
It will be possible
to earn extra credits by presenting solutions to problems at the
blackboard (Lecture 4, 8, 16, 20) and optional laboratory exercises.
At most 5 points (p) can be
earned this way, which may be added to the score of the written exam.
The maximal score is 40p. To get the grade VG 28p are required; for
the grade G the requirement is 18p.
Lecturers and assistant
Links
1 January 2003,
Erik Palmgren.
