Tik-79.144 Logic in Computer Science: Foundations

Autumn 1996 (Autumn 1997)

General Information

• Lectures by Tomi Janhunen: Mondays 12-14 (hall K)
• Tutorials by Patrik Simons: Tuesdays 11-12 (room Y427B) or Thursdays 9-10 (hall J)
• Textbook: Nerode and Shore: Logic for Applications, Springer, 1993, 365 p, Errata
  • available at the bookstore NOW !!!
• The course consists of
  • textbook (Chapters I, II and III in the extent presented at lectures)
  • attendance to lectures and tutorials (2+1 hours a week), these are held in Finnish.
  • three 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 in Finnish, course information at TOPI in Finnish

Examinations

• December 12, Results
• January 16, Results
• May 21, Results
• September 1, Results
• Still valid during autumn 1997 and spring 1998, then expired.

Home Assignments

• Results
• Still valid during autumn 1997 and spring 1998, then expired.

Lectures

September 16th: Lecture 1

Introduction, syntax of propositional logic (pages 1-9), tutorial (solutions)

September 23rd: Lecture 2

Truth tables, semantic tableaux (pages 10-29), tutorial (solutions)

September 30th

NO LECTURES NOR TUTORIALS (this week) !!!

October 7th: Lecture 3

Soundness and completeness of tableaux, Hilbert-style axiomatizations, normal forms (pages 30-43), tutorial (solutions)

October 14th: Lecture 4

Resolution in propositional logic (pages 43-69), tutorial (solutions)

October 21st: Lecture 5

Predicate logic and its semantics (pages 73-89), tutorial (solutions)

October 28th: Lecture 6

Semantic tableaux for predicate logic, Hilbert-style axiomatization (pages 97-115), tutorial (solutions)

November 4th: Lecture 7

Normal forms, skolemization, Herbrand's theorem, unification (pages 116-131), tutorial (solutions)

November 11th: Lecture 8

Constructing structures (the 2nd home assignment), resolution, knowledge representation (pages 131-144), tutorial (solutions)

November 18th: Lecture 9

Knowledge presentation with predicate logic, theorem prover OTTER, tutorial (solutions)

November 25th: Lecture 10

Resolution in PROLOG, negation by failure (pages 145-188), tutorial (solutions)

December 2nd: Lecture 11

Review of the lectures 1-10, Rehearsal examination (tutorials)