TKK / Department of Information and Computer Science / Research / Computational Logic


Helsinki University of Technology, Department of Information and Computer Science

Computational Logic Group


[Personnel] [Alumni] [Software] [Projects] [Theses] [Publications] [Interesting links]


The research area of the Computational Logic Group led by Professor Ilkka Niemelä in the Department of Information and Computer Science at Aalto University is applications of logic in computer science and engineering. The group develops automated reasoning techniques for solving challenging computational problems in engineering and science. The current focus is on efficient computational methods for solving large constraint satisfaction problems including SAT, SMT and rule-based constraints and on their applications in areas such as computer aided verification, automated testing, product configuration, planning, combinatorial problems, and logical cryptanalysis. This involves basic research on foundational issues, relationships, and computational complexity of such constraints but also developing computational methods and efficient implementation techniques. In fact, the research has lead to a number of software tools that are widely used (see below Software). For example, the Smodels system is actively used in dozens of research groups all over the world.

The long-term goal is to develop methodology using which domain specialists with limited computer science background could solve computationally challenging engineering problems. The idea is to achieve this by offering a language where solutions to a problem can be described/defined in a natural and compact way and by developing efficient methods for computing solutions. This is a basic idea underlying a novel programming paradigm called Answer Set Programming (ASP) for which the group has been one of the first pioneers. For example, the Smodels system can be seen as a first generation ASP system which offers a rule-based language for representing a variety of engineering problems ranging from product data to combinatorial problems and a computational engine for solving them.

Ongoing projects:



Personnel



Summer interns 2010


  • Rehan Abdul Aziz
  • Iiro Kiviranta
  • Chi Mai Nguyen
  • Timo Niemi
  • Jonatan Ropponen
  • Tao Sun

Alumni



Previous projects



Software


  • lp2diff, a translator mapping logic programs to SMT theories implemented by Tomi Janhunen.
  • Smodels - an implementation of the stable model semantics for logic programs with cardinality and weight constraints
  • lparse - a front-end for the Smodels system
  • GnT - a solver for disjunctive logic programs
  • circ2dpl - translating parallel circumscriptions into disjunctive logic programs
  • psmodels - psmodels is a modification of smodels that can be used to compute preferred answer sets under the ordered disjunction semantics.
  • (D)LPEQ - software for verifying the equivalence of (disjunctive) logic programs
  • ssokoban - a smodels/perl program that solves sokoban levels. Contains also a patch for xsokoban.
  • mcsmodels - a deadlock and reachability checker. It uses finite complete prefixes generated by the PEP tool from 1-safe Petri nets and employes smodels as its computational engine.
  • punroll - a bounded reachability checker based on process semantics.
  • boundsmodels - a bounded model checker for LTL
  • unfsmodels - an LTL model checker using net unfoldings
  • Bomotest - testing tool
  • BCSat - an implementation of a tableau method for Boolean circuit satisfiability checking; the description of the file format for Boolean circuits and a translator from Boolean circuits to CNF is also available.
  • genfacbm - a benchmark generator based on factoring for SAT and ASP solvers
  • lbtt - a testbench for implementations of algorithms for translating linear temporal logic (LTL) formulas into Büchi automata.

Interesting Links




Latest update: 15 January 2011.