Integrating a CAS as Proof Planer in the OMEGA Proof Development Environment
Date: July 17th (Wednesday)
Time: 14:25-14:50
Abstract
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.
