The scientific and technological goal of this network is the design of a new generation of mathematical software systems and computer-aided verification tools based on the integration of the deduction and the computational power of Deduction Systems and Computer Algebra Systems respectively.
Both Deduction Systems and Computer Algebra Systems are receiving growing attention from industry and academia. On the one hand, Mathematical Software Systems have been commercially very successful in recent years. Their use is now wide-spread in industry, education, and scientific contexts: there are now literally millions of installations of computer algebra programs. On the other hand, the use of formal methods in hardware and software development has made Deduction Systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved. These systems are now making the transition from academic applications into regular industrial practice.
In spite of these successes there is still need for improvement as many application domains still fall outside the scope of existing Deduction Systems and Computer Algebra Systems. For instance, the scope of Computer Algebra Systems (CASs) could be significantly enhanced by adding deductive reasoning power. In fact this lack of expressivity together with the unsolved problem of correctness prohibit large classes of applications. Deduction systems (DSs), which - on the other hand - provide such an expressivity, as well as the guarantee of correctness, still lack computational power as they are not suited to directly carry out algebraic or numerical calculations. This severely restricts their scope of application in mathematics and - more importantly - in engineering applications.
The technical goal of the proposed network is to combine the reasoning capabilities of DSs and the computational power of CASs. The question is whether existing systems and technologies can be integrated as they stand or if a fundamental redesign will be necessary. The network will investigate both possibilities simultaneously. The feasibility of the approaches will be ascertained by carrying out theoretical investigations on the architectural requirements, by experimenting with extensions of existing systems, by developing prototype systems, and finally by devising and carrying out suitable case studies.
The field of DSs has diversified into the areas of automated theorem proving (ATP) and interactive proof-development (IPD), which have their own traditions, conferences and technical methods. The field of computer algebra (CA) has specialised on devising highly efficient methods for symbolic calculations. The research programme of the proposed network can only be achieved by bringing together the three research communities and by benefiting from the synergy and cross-fertilizing effects. This will also generate a highly stimulating training environment for the young visiting researchers.