\begin{center}
\LARGE
Integrating a CAS as Proof Planer in the OMEGA Proof
                  Development Environment 
\end{center}

\begin{center}
\Large
Volker Sorge
\end{center}

\noindent
Date:  July 17th (Wednesday)\\
Time:  14:25-14:50\\

\begin{center}
\large
Abstract
\end{center}

The SAPPER system integrates the proof development environment Omega with a
Computer Algebra System as a proof planner. For constructing plans it
exploits the knowledge implicit in the algorithms of the CAS. To extract
those informations the algorithms must be augmented with a verbose mode to
return a trace of single computation steps. This output is then translated
in proof plans using a tactic mechanism.

So far SAPPER uses a small prototypical CAS with verbose algorithms for
polynomial manipulations. In this setting we are able to apply it
successfully to optimization problems in economy.





