TCS / Studies / T-79.5102 Special Course in Computational Logic
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science


Special Course in Computational Logic

(4 cr) P V

Autumn 2005 (periods I and II)

[General Information] [Course Material] [Feedback] [Examinations] [Home Assignments] [Software] [TOPI]

This is an advanced course on knowledge representation, automated reasoning and decision making. Subjects covered this year are: advanced decision methods for propositional logic (Davis-Putnam, BDDs, stochastic methods) and for rule-based reasoning.

General Information

  • Please use the TOPI system for registration. Late registration is possible by contacting the lecturer.
  • This course replaces two former courses: T-79.154 Logic in Computer Science: Special Topics II and T-79.230 Foundations of Agent-Based Computing. The course contents is based on T-79.154 this term.
  • Lectures: Prof. (pro tem), D.Sc.(Tech.) Tomi Janhunen, Mondays, 12-14, room TB353
  • Tutorials: M.Sc.(Tech.) Emilia Oikarinen, Tuesdays, 15-16, room TB353
  • Course material: lecture notes and articles
  • Brochure in Finnish
  • Tentative schedule for lectures
Back to menu.

Course Material

Lecture Notes

Excercises from Tutorials

Reading List

  • [A97] Andersen, H.R.: An Introduction to Binary Decision Diagrams.
  • [F90] Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990, pp. 88-93.
  • [KS96] Kautz, H. and Selman, B.: Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. In Proceedings of the 13th National Conference on Artificial Intelligence, Portland, OR, 1996.
  • [SKC93] Selman, B., Kautz, H.A., and Cohen, B.: Local Search Strategies for Satisfiability Testing. In 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.
  • [N99] Niemelä, I.: Logic Programs with Stable Model Semantics as a Constraint Programming Paradigm. In Annals of Mathematics and Artificial Ingelligence, 24(3-4), 241-273, 1999.

Further Reading

Back to menu.

Course Feedback

We welcome feedback which is collected centrally in Finnish; the questionnaire is activated on the 9th of December, 2005.

  • To obtain a 0.5 point bonus for the exams arranged in December and March you are supposed to fill in the form by the 2nd of January, 2006 (24:00 hours).
Back to menu.


  • Please use the TOPI system in order to get registered for an exam.
  • December 21, 2005, final results (published, January 19, 2006)
  • March 7, 2006, final results (published, April 12, 2006)
  • May 9, 2006, no examinees showed up
Back to menu.

Home Assignments

  • Results
  • Home assignments are personal and supposed to be done individually.
  • We create a dedicated home directory for each student registered for the course.
  • You should expect an email (on September 20, 2005) which gives you access rights to your home directory.
  • Submission by email (preferably an URL to visit) to Emilia Oikarinen. Please mention your student ID!
  • Your report should include a short description of your approach/solution (including the translation involved), solutions (or counter examples) found and sample runs (if appropriate).
  • The first home assignment involves large boolean functions (and quite large files). Please do not send such big files (or their translations) to us.


Home assignments are to be launched as follows:
  • HA1: September 19, 2005; deadline October 3, 2005.
  • HA2: October 17, 2004; deadline November 7, 2005.
  • HA3: November 14, 2004; deadline December 5, 2005.
Back to menu.


Precompiled programs have been installed in the machines of computing centre: please consult the subdirectories of ~tomppa/T-79.5102/.


SAT solvers

LP instantiators and solvers

  • lparse developed by T. Syrjänen (source code)
  • smodels developed by P. Simons and I. Niemelä (source code)
  • GnT developed by P. Simons, T. Janhunen, and I. Niemelä (source code)

Planning as a satisfiability problem

  • Clauses can be instantiated using a program called instantiate.
  • As an example, check our encoding of the blocks world domain for instantiate; including an example due to Sussman.
  • The output of instantiate is a valid input for GnT that computes minimal models for the given set of rules/clauses.
  • Alternatively, the internal gnt/smodels format can be translated into DIMACS-format supported by most SAT solvers using a translator called dimacs.
  • When using SAT solvers, a filter called intp can be used to printing models in a symbolic (rather than numeric) form.
  • See some examples how the programs are used to solving planning problems.
Back to menu.
[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 23 May 2006. Tomi Janhunen