Overview on the Apply Math Project at RISC

Bruno Buchberger, RISC Hagenberg, Austria

Abstract:

We started work on a project, "Apply Math" that aims at creating a uniform (logic and software) system for "doing" mathematics. The lack of support of proving seems to be the most apparent gap in present mathematical software systems. Filling this gap is one of the major aims of the Apply Math project. We choose a version of higher order logic (with set theory as a sublanguage) as the logic framework and we start from Mathematica as a software framework for working towards the general goal. We report on first steps towards