• Increase font size
  • Default font size
  • Decrease font size
DTAI KRR Software
KRR's software

KRR develops software aimed at combining knowledge with different inference tasks for the logic FO(·)IDP, an extension of first-order logic (FO) with types, aggregates, inductive definitions, bounded arithmetic, partial functions, etc.

Current systems

IDP3-beta Gidl
IDP2 MinisatID
IDPDraw ConfigID


Older systems

KB-system demo: 5 different forms of inference for interactive configuration software

The IDP system is a knowledge base system that implements different forms of inference for a knowledge base consisting of   FO(.)  theories. The attached system demonstrates how  an interactive configuration tool  can be built  using the IDP system.The configuration tool  supports students in selecting a study program.  The system comes as a java jar file implementing a GUI  from which IDP is called on a logic knowledge base specifying the rules governing course selection. The knowledge base is editable; changing rules have immediate effect on the behaviour of the system. This prototype tool demonstrates  a principle that separates declarative KR from programming: the possibility of applying various forms of inference on the same logic specification. In particular, this system uses 5 forms of inference to implement various  typical use cases of configuration software: propagation, model checking, model expansion, model expansion with optimisation and explanation..  For details, see:

Vlaeminck, Hanne; Vennekens, Joost; Denecker, Marc. A logical framework for configuration software, Principles and Practice of Declarative Programming, Coimbra, Portugal, 7-9 September, 2009, Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming PPDP '09

Download[Disclaimer: only contains Linux binaries of IDP.]


the A-system is an abductive query answering system for ID-logic. It is currently in use in a pilot project involving IBM and Imperial College London for monitoring policies webpage. [Disclaimer: no more research is devoted to this topic, we do not provide support any more.]

More info


MidL is a solver for the MNF format.



This is a demo for students in secondary school. It is only available in dutch. It consists of 5 problems (graph coloring, course scheduling, n-queens, towers of Hanoi, and sudoku). For each of these problems, a skeleton of a solution is provided, together with instances, automated procedures to check you solution and visualize your solution. If your solution is wrong, the visualization will emphasize your mistakes.

  • If you don't have the IDP-IDE yet, you can download a pre-configured version below. Please follow the instructions in the README:
    • Currently only supported for Windows: Download (requires 32bit java virtual machine)
    • If you are a Linux user, please donload the correct (32 or 64 bit) eclipse here, and follow the instruction to install the IDE here. Next, you can install the "wetenschapsweek demo" as described below.
  • If you already have the IDP-IDE installed, please download one of the following files and follow the instructions in the README:
  • An old version of this demo (in IDP2) can be downloaded here
Last Updated on Wednesday, 04 December 2013 18:16