Integrating Computer Algebra Systems and Theorem Provers

Jacques Calmet

Abstract: Coupling computation and deduction is the topic of many on going 
projects.  This talk will be divided into three parts.  The first one 
investigates and assesses the different possible approaches.  A second part is 
a reminder of the experiments we have conducted in Karlsruhe.  The third part 
draws conclusions and lessons from these experiments. The talk concludes with 
a brief review of our on going research resulting from these experiments.