IDP is a knowledge Base System (KB-system) for the FO(·) language. A Knowledge Base system is a system that supports multiple forms of inferences for he same Knowledge Base. FO(·) is an extension of first-order logic (FO) with types, aggregates, inductive definitions, bounded arithmetic, partial functions, etc.

More information about FO(·), including an editorial by David Warren, can be found on the FO(·) language page. For a motivation of the Knowledge Base paradigm, see an application for interactive configuration.

Using IDP, it is possible to model systems and problems, both from the real world as several artificial intelligence research problems. Solutions to these problems can then be found using one or more inference techniques. One class of real world problems that serves as a nice introduction to IDP is a scheduling problem.

Imagine for example a hospital schedule where employees are assigned to certain departments. A good schedule should meet certain rules.

- Every employee works on exactly one department.
- At every department, at least a certain minimal occupance is present

The first step is defining a vocabulary containing all symbols we'll make statements about:

vocabulary Work { type Employee type Department type Threshold isa int WorksOn(Employee, Department) MinimalOccupance(Department) : Threshold }

Next, we need a theory that describes the conditions and constraints for a correct planning.

theory SchedulingRules : Work { !e[Employee] : ?1 d[Department] : WorksOn(e, d). !d[Department] : #{e[Employee] : WorksOn(e, d)} >= MinimalOccupance(d). }

Finally, we must specify which employees and departments exist, using a structure:

structure Hospital : Work { Employee ={e1;e2;e3;e4;e5} Department = {d1;d2;d3} Threshold = {1..5} MinimalOccupance = {d1->1;d2->2;d3->1} }

Now that the problem and its constraints are expressed, several inference techniques can be used to solve different questions:

- Using model expansion inference, it is possible to generate a scheduling for the hospital.
- Using satisfiability inference, it is possible to check the validity of a certain schedule.
- Using optimization inference, it is possible to generate a schedule that is optimal according to some quantifiable criterium.

Feel free to play around with this example in our online editor, take a look at other examples on our examples page.