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

• 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
  • lectures and tutorials (2+1 hours a week) held in Finnish
  • three compulsory home assignments
  • examinations (arranged four times a year)
• 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

Material

• 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 !!!

Home Assignments

• 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.

Examinations

• December 15 (in English), final results
• January 14 (in English), solutions, final results
• May 12 (in English), solutions, final results
• September 5 (in English), preliminary results
• Registration for the exams is strongly recommended.
• Questions will be provided in Finnish and in English.
• Earlier examinations

Lectures and Tutorials

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).