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

Examinations

• December 19, 2000 (in English), final results
• January 9, 2001 (in English), final results
• May 10, 2001 (in English), results
• September 4, 2001 (in English), results
• Registration for the exams is compulsory and binding (if you register for an exam, then you must attend it).
  Registration is possible two weeks before each examination.
• Questions will be provided in Finnish and in English.
• Earlier examinations

Feedback

Home Assignments

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

Lectures and Tutorials

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.