Integrating a CAS as Proof Planer in the OMEGA Proof Development Environment
Date: July 17th (Wednesday)
Time: ??.??
Abstract
The goal of the Apply Math project at the RISC institute is the expansion of
Mathematica by interactive proving facilities so that mathematical texts can be produced
that contain both mathematical text, interactive mathematical formulae, proofs of these
formulae, and algorithms based on these formulae. We present the logic concept, the syntax,
the structuring concept based on functor programming, and some first examples of
interactive theorem provers for certain mathematical domains in the frame of this project.
