Integrating a CAS as Proof Planer in the OMEGA Proof Development Environment

Volker Sorge

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.

______________
__________________________________________

Previous page RISC SWP Linz Austria