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,
resolution.
[General Information]
[Material]
[Examinations]
[Home Assignments]
[Lectures]
[TOPI]
- Lectures by
Tomi Janhunen:
Mondays 12-14 (hall K)
- Tutorials by Tommi Syrjänen:
Tuesdays 12-13 (room Y313) or Thursdays 9-10 (room Y427B)
- Office hours:
arranged next in the beginning of September (room Y429A)
- 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 in Finnish
- Textbook:
A. Nerode and R. Shore:
Logic for Applications, Springer, 1993, 365 p.
- Chapters I, II and III in the extent presented at lectures
- available at the bookstore NOW (the second edition) !!!
- Errata
for the first edition
- Lecture Notes (opetusmonisteet)
- Questions from tutorials and answers to the questions
- Slides from the lectures (4 slides per page)
- The first set (L1-L4 and T1-T4) is ready.
- The second set (L5-L8 and T5-T8) is ready.
- The third set (L9-L10 and T9-T10) is ready.
- Your name and student id is printed on
your personal home assignment.
Check this information to get your own assignments.
- Home assignments (questions + answers) are returned
to a box on the shelf outside room Y418.
- Next deadline: June 5, 1998.
- The list of
accepted assignments.
- Rejected assignments
have to be corrected in order to be accepted.
- Rejected assignments can be fetched from tutorials or
from our secretary (Ulla Kangasniemi, room Y418).
- A corrected home assignment
(questions + answers + corrections)
is returned to the box mentioned above.
- To get help for your home assignments
attend any office hour.
Please avoid unnecessary printing of the material to save printers,
paper and thus nature. The slides and tutorials can be ordered as
lecture notes (opetusmonisteet).
Timetable and contents (page numbers refer to the first edition):
-
September 15: Lecture 1
- Introduction, syntax of propositional logic (pages 1-9),
tutorial
(solutions)
-
September 22: Lecture 2
- Truth tables, semantic tableaux (pages 10-29),
tutorial
(solutions)
-
September 29: Lecture 3
- Soundness and completeness of semantic tableaux,
Hilbert-style axiomatizations, normal forms (pages 30-43),
tutorial
(solutions)
-
October 6: Lecture 4
- Resolution in propositional logic (pages 43-69),
tutorial
(solutions)
-
October 13: Lecture 5
- Predicate logic and its semantics (pages 73-89),
tutorial
(solutions)
-
October 20: Lecture 6
- Semantic tableaux for predicate logic (pages 97-115),
tutorial
(solutions)
-
October 27: Lecture 7
- Hilbert-style axiomatization, normal forms, skolemization,
Herbrand's theorem, unification (pages 116-131),
tutorial
(solutions)
-
November 3: Lecture 8
- Constructing structures, unification algorithm,
resolution (pages 131-144),
tutorial
(solutions)
-
November 10: Lecture 9
- Knowledge presentation with predicate logic, theorem prover
OTTER
(manual),
tutorial
(solutions)
-
November 17: Lecture 10
- Resolution in PROLOG, negation by failure (pages 145-188),
tutorial
(solutions)
-
November 24: Review of Lectures 1-10
- Tutorials: help for home assignments
-
December 1: Review of Lectures 1-10
- Tutorials:
rehearsal examination
-
December 8: Additional office hour (12-14): help for home assignments
- Tutorials: help for home assignments
Latest update: June 9, 1998 by
Tomi Janhunen