TCS /
Studies /
Tik-79.144 /
1999
Tik-79.144 Logic in Computer Science: Foundations
Autumn 1999
This is an introductory course on logic and its applications in
computer science. Subjects covered are: propositional and predicate
logic, model theory, proof theory, semantic/analytic tableaux,
resolution.
[General Information]
[Material]
[Home Assignments]
[Examinations]
[Program]
[TOPI]
[Autumn 2000]
[Autumn 1998]
- Registration by
TOPI
or by attending the first two lectures
- Lectures by
Tomi Janhunen,
on Tuesdays, 10-12, hall T1
- Tutorials by Tommi Syrjänen,
on Tuesdays, 16-17, or on Fridays, 9-10,
hall T2
- Office hours: see the lecturer's home page
- The course consists of
- In order to pass the course one has to pass
- the three home assignments
- the exam (with a grade greater than 0)
- Newsgroup:
opinnot.tik.logiikka
- Brochure
- Textbook:
A. Nerode and R. Shore:
Logic for Applications, Springer, 1997, 456 p.
- Chapters I, II and III in the extent presented at lectures
- the first edition of the book (1993, 365 p.) can also be used
(Errata)
- Lecture Notes (opetusmonisteet)
- Questions from tutorials and answers to the questions
- Slides for the lectures (4 slides per page) in three packages:
Propositional Logic,
Predicate Logic,
Applications,
- Lecture notes can be ordered from Otatieto (opetusmonisteet).
- Please avoid unnecessary printing of the material
to save printers, paper and thus nature !!!
- All the three home assignments have been evaluated:
please consult the list of accepted assignments.
- Rejected assignments can be fetched from Ulla Kangasniemi
(room TB336, preferably available 8:30-15:30) for corrections
and resubmitted.
- The next deadline for resubmissions is September 8, 2000.
- The
second and third home assignmentsn
and available in electronic form (not in print).
- Reference Manual and Guide
for the automated theorem prover
OTTER.
- Translations
in English are also provided.
- Home assignments are personal
(your name and student ID are printed on your sheet).
- Answers to questions or corrections to answers
(including the question sheet and previous answers)
can be returned to the white mailbox outside room TB336.
Timetable and contents
-
September 14: Lecture 1 (pages 1-16, slides 2-11)
- Introduction,
syntax of propositional logic
Tutorial 1
(in English),
solutions
(in English).
-
September 21: Lecture 2 (pages 17-36, slides 12-30)
- Truth tables and semantic tableaux
Tutorial 2
(in English),
solutions
(in English).
-
September 28: Lecture 3 (pages 37-48, slides 31-39, 43-45)
- Soundness and completeness of semantic tableaux,
Hilbert-style axiomatization
Tutorial 3
(in English),
solutions
(in English).
-
October 5: Lecture 4 (pages 49-51, slides 40-42, 46-57)
- Normal forms and the resolution rule
Tutorial 4
(in English),
solutions
(in English).
-
October 12: Lecture 5 (pages 52-68, slides 58-73)
- Resolution proofs and computational complexity
Tutorial 5
(in English),
solutions
(in English).
-
October 19: Lecture 6 (pages 81-99, slides 74-97)
- Syntax and semantics of predicate logic
Tutorial 6
(in English),
solutions
(in English).
-
October 26: Lecture 7 (pages 108-126, slides 98-111)
- Semantic tableaux for predicate logic
Tutorial 7
(in English),
solutions
(in English).
-
November 2: Lecture 8 (pages 127-141, slides 112-135)
- Hilbert-style axiomatization, normal forms, Skolemization,
Herbrand's theorem, unification
Tutorial 8
(in English),
solutions
(in English).
-
November 9: Lecture 9 (pages 142-153, slides 136-148)
- Unification algorithm, resolution rule
Tutorial 9
(in English),
solutions
(in English).
-
November 16: Lecture 10 (pages 154-158, slides 149-173)
- Resolution, knowledge representation
Tutorial 10
(in English),
solutions
(in English).
-
November 23: Lecture 11 (pages 69-80 and 159-202, slides 174-203)
- Theorem prover OTTER, logic programming
Tutorial 11
(in English),
solutions
(in English).
-
November 30: No lecture
- Tutorials:
a rehearsal examination is arranged.
-
December 7: Lecture 12 (slides 204-228)
- Negation in PROLOG, rule-based reasoning,
applications of induction principle
Tutorial 12
(in English),
solutions
(in English).
Latest update: Aug 30, 2000
by Tomi Janhunen