The research work focus on the design and implementation of automated tools for the development of mathematical theories needed in industrial applications, in particular in program verification.

The tools will allow a high degree of automation of the most important relevant activities: the management of mathematical knowledge, exploration and discovery of mathematical theories, efficient proving, solving, and computing using these theories. The development of the tools will be driven by case studies of concrete theories used in applications, in particular program verification, verification of information systems, and e-learning.

The concrete activity start on three main directions of research which are described below. As the project will advance, we plan to adapt and re-focus the activities in accordance with the results obtained, as well as the evolution of the international research in the field.

1. Management of Mathematical Knowledge using Artificial Intelligence.

2. Exploration of Mathematical Theories using Computational Logic.

3. Discovering of Mathematical Algorithms using Phase Transitions.