Systems for Integrated Computation and Deduction : Interim Report of the CALCULEMUS Network

Abstract

This document reports on the research progress made in all work task of the CALCULEMUS IHP Training Network HPRN-CT-2000-00102 after the first half of the 48 months funding period. The objectives of the CALCULEMUS Network are: 1. outline the design of a new generation of mathematical software systems and computer-aided verification tools; 2. the training of young researchers in the broad field of mechanical reasoning and formal methods; 3. the dissemination of the results both in industry and in academia; and 4. the cross-fertilisation and amalgamation of the automated theorem proving (ATP/DS), computer algebra (CAS), term rewriting systems (TRS) interactive proof development systems (ITP) and software engineering (SE) research communities. The work tasks of the Network are: Task 1.1: Mathematical Frameworks Task 1.2: Definition of Mathematical Service Task 2.1: Integration of CASs and DSs via Protocols Task 2.2: Enhancing the Reasoning Power of Computer Algebra System Task 2.3: Enhancing the Computation Power of Deductions Systems Task 3.1: Automated Support to Writing Mathematical Publications Task 3.2: Support to the Development of an Industrial-Strength Application of Formal Methods to Program Verification Task 3.3: Support to the Solution of Undergraduate Exam in Calculus and Economics Task 3.4: Modelling of Existing Systems as Mathematical Service Task 3.5: Challenge Mathematical Problems