DEDUC is a software package that integrates scientific results and practical needs in generating combinatorial schedules. The work on the system started in 1991. After ten years the powerful system is developed.

The theoretical foundation of the system is the Automated Theorem Proving based on Resolution principle and heuristic methods of the Artificial Intelligence.

The practical orientation of the system is generating class schedules with respect to the user-defined restrictions.

System is based on synchronized work of two processes: data storing and optimization of gaps in the timetable. Theorem prover controls both processes to secure that initial requirements are not violated. In the case of a delay in the process of generating a schedule, the process is enabled to be transformed into another flow, in order to generate a better schedule.

System facilities and performances:

• Automatic and interactive generating of schedules for the initial data and conditions;
• Setting up and maintenance of the initial data and requirements by using the user friendly interface;
• Setting up various initial requirements like splitting classes into groups, connecting groups and classes, enabling multiple lessons; setting restrictions in using laboratories and rooms; setting teachers requirements and the other pedagogic obligations and desirable demands;
• Generating schedules respecting school shifts;
• Screen browsing and printing the general, per-class and per-teacher schedules;
• Generating and archiving different versions of the schedules generated for the same initial data and conditions;
• Maintenance of the archived versions, data and conditions.

The practical efficiency and system limits can be observed for complicated examples as well as for the simple ones. Essentially, getting the acceptable version of the schedule depends on structure of the initial requirements and their connections with data, although the number of requirements has no influence.

In the case that contradictions are hidden in requirements, creating a timetable is disabled. Therefore, reduction of requirements is allowed in order to generate an acceptable schedule.

Practical experiences in the real world assure that DEDUC system generates timetables with quality level higher than quality level of hand-made timetables. The time needed for generating a timetable varies from few minutes to several hours, and depends on amount of data, structure of conditions as well as on computer performances.