TCS /
Studies /
Tik-79.144 /
2000
Tik-79.144 Logic in Computer Science: Foundations
Autumn 2000
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]
[Feedback]
[Home Assignments]
[Program]
[TOPI]
[Autumn 2001]
[Autumn 1999]
- Registration is no longer possible for this academic year.
- Lectures by
Tomi Janhunen,
on Tuesdays, 10-12, hall T1
- Tutorials by
Tommi Syrjänen and
Toni Jussila,
on Tuesdays, 15-16, or Wednesdays, 9-10,
or 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 (ps/pdf-format 4/2-slides per page)
in three packages:
Propositional Logic,
Predicate Logic,
Applications
(PDF)
- Lecture notes can be ordered from Otatieto (opetusmonisteet).
- Please avoid unnecessary printing of the material
to save printers, paper and thus nature !!!
It is now possible to give feedback by filling a
form.
- All the three home assignments are available on our
server.
- A notification has been sent by email
to those that were registered for the course on time.
- List of students
(342/438) who have passed the first home assignment
(generated on October 24, 2000, 24:00).
- List of students
(329/387) who have passed the first two home assignments
(generated on November 23, 2000, 24:00).
- List of students
(278/393) who have passed all the three home assignments
(generated on September 25, 2001, 24:00).
- These lists are not updated in the sequel. If you have not
completed your home assignments yet, please follow
instructions and schedule given for the academic year 2001-2002.
- Some general
instructions
for solving the third home assignment (in Finnish).
Timetable and contents
-
September 12: Lecture 1 (pages 1-16, slides 1-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 26: 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 3: Lecture 4 (pages 49-51, slides 40-42, 46-56)
- Normal forms and the resolution rule
Tutorial 4
(in English),
solutions
(in English).
-
October 10: Lecture 5 (pages 52-68, slides 57-73)
- Resolution proofs and computational complexity
Tutorial 5
(in English),
solutions
(in English).
-
October 17: Lecture 6 (pages 81-99, slides 74-98)
- Syntax and semantics of predicate logic
Tutorial 6
(in English),
solutions
(in English).
-
October 24: Lecture 7 (pages 108-126, slides 99-111)
- Semantic tableaux for predicate logic
Tutorial 7
(in English),
solutions
(in English).
-
October 31: Lecture 8 (pages 127-141, slides 112-125)
- Hilbert-style axiomatization, normal forms, Skolemization,
Herbrand's theorem, unification
Tutorial 8
(in English),
solutions
(in English).
-
November 7: Lecture 9 (pages 142-153, slides 126-141)
- Unification algorithm, resolution rule
Tutorial 9
(in English),
solutions
(in English).
-
November 14: Lecture 10 (pages 154-158, slides 142-168)
- Resolution proofs, representing knowledge using logic
Tutorial 10
(in English),
solutions
(in English).
-
November 21: Lecture 11 (pages 69-80 and 159-202, slides 169-203)
- Theorem prover OTTER, logic programming
Tutorial 11
(in English),
solutions
(in English).
-
-
November 28: Lecture 12 (slides 204-228)
- Negation in PROLOG, rule-based reasoning,
applications of induction principle
Tutorial 12
(in English),
solutions
(in English).
-
-
December 5: Review of lectures 1-12
- A rehearsal exam
is handled in the tutorials.
Latest update: October 2, 2001
by Tomi Janhunen