Tik79.154 Logic in Computer Science: Special Topics II
This is an advanced course on logic and its applications in computer
science and engineering. Subjects covered this year are:
advanced decision methods for propositional logic (DavisPutnam, BDDs,
stochastic methods) and for rulebased reasoning.
 Lectures by
Ilkka Niemelä:
Tuesdays 1416, room Y427B
 Tutorials by
Patrik Simons:
Tuesdays 1617, room Y427A
 Course material:
Lecture notes.
Articles.
 In order to pass the course one has to pass
 a home assignment and
 an exam
 The first exam: 09.12.97 (1417, Y427A).
See instructions
for the exam (in Finnish).
Results
of the exam on 9.12.1997
Results
of the exam on 26.1.1998
 Summary of the
results (including the home assignments) for fall 1997

Results
of the exam on 26.5.1998
 Newsgroup: opinnot.tik.logiikka
 Brochure in Finnish,
course information at
TOPI
Lecture notes ***
Software ***
Home assignments ***
Program ***
Other Interesting Stuff
Lecture Notes
(Slides in PostScript; in Finnish)

Introduction
 Introduction to the course and a refresher on classical logic

DavisPutnam method

tutorial 1
(solutions)

Binary Decision Diagrams

tutorial 2
(solutions)

Local Search Methods

tutorial 3
(solutions)

Rulebased reasoning I

tutorial 4
(solutions)

Rulebased reasoning II

tutorial 5
(solutions)


Case study:
planning as satisfiability

Case study:
planning using logic programs +
complexity considerations
Software

Tableau (DavisPutnam method) by J. Crawford

POSIT (DavisPutnam method) by J. Freeman

CUDD (BDD) from University of Colorado

BDD Library from CMU

Walksat by Bart Selman

Smodels (logic programs with stable model semantics) by Patrik Simons
and Ilkka Niemelä
Home Assignments
There is a compulsory home assignment for each student.
The assigments are now available. If you do not yet have one, please
contact the lecturer.
For further details, see the
instructions (in Finnish).
Each student gives a short presentation (15 min) on the home
assignment on Dec 2, 1997.
For grading of the returned assignments, see summary of the
results.

Robbins Algebras Are Boolean
 Information on a proof of a famous mathematical conjecture found by
an automated theorem prover.
Latest update: Oct 7, 1997 by Ilkka.Niemela@hut.fi