Tik-79.144 Logic in Computer Science: Foundations
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,
- Registration by
or by attending the first two lectures
- Lectures by
on Tuesdays, 10-12, hall T1
- Tutorials by Tommi Syrjänen,
on Tuesdays, 16-17, or on Fridays, 9-10,
- 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)
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
- Lecture Notes (opetusmonisteet)
- Questions from tutorials and answers to the questions
- Slides for the lectures (4 slides per page) in three packages:
- 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
- The next deadline for resubmissions is September 8, 2000.
second and third home assignmentsn
and available in electronic form (not in print).
- Reference Manual and Guide
for the automated theorem prover
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)
syntax of propositional logic
September 21: Lecture 2 (pages 17-36, slides 12-30)
- Truth tables and semantic tableaux
September 28: Lecture 3 (pages 37-48, slides 31-39, 43-45)
- Soundness and completeness of semantic tableaux,
October 5: Lecture 4 (pages 49-51, slides 40-42, 46-57)
- Normal forms and the resolution rule
October 12: Lecture 5 (pages 52-68, slides 58-73)
- Resolution proofs and computational complexity
October 19: Lecture 6 (pages 81-99, slides 74-97)
- Syntax and semantics of predicate logic
October 26: Lecture 7 (pages 108-126, slides 98-111)
- Semantic tableaux for predicate logic
November 2: Lecture 8 (pages 127-141, slides 112-135)
- Hilbert-style axiomatization, normal forms, Skolemization,
Herbrand's theorem, unification
November 9: Lecture 9 (pages 142-153, slides 136-148)
- Unification algorithm, resolution rule
November 16: Lecture 10 (pages 154-158, slides 149-173)
- Resolution, knowledge representation
November 23: Lecture 11 (pages 69-80 and 159-202, slides 174-203)
- Theorem prover OTTER, logic programming
November 30: No lecture
a rehearsal examination is arranged.
December 7: Lecture 12 (slides 204-228)
- Negation in PROLOG, rule-based reasoning,
applications of induction principle
Latest update: Aug 30, 2000
by Tomi Janhunen