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.
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.]
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:
- 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