A case-study in algebraic manipulation using mechanized reasoning tools

Abstract

In this article, two different mechanized reasoning tools (Coq and Isabelle/HOL) are used in order to prove some basic but significant properties extracted from a symbolic computation system called Kenzo. In particular, we focused on a property called ‘cancellation theorem’, which can be applied to the proof of the idempotence property of a differential morphism. This result is used as a case-study to compare the capabilities and styles of the two proof assistants. The conclusion of our comparison is that both tools are adequate to solve the case-study presented in this article in a rather similar way but depending on their specific styles. This research is part of a more general project devoted to increase the reliability of computer algebra systems for calculations in algebraic topology.

Keywords:

• mechanized reasoning tools
• symbolic computation
• algebraic manipulation
• Isabelle/HOL
• Coq

2000 AMS Subject Classifications :

• 68T15
• 68Q60

Acknowledgements

This work has been partially supported by Ministerio de Educación y Ciencia, project MTM2006-06513. We wish to thank the referees for valuable comments that have improved the final version of this article.

Notes

†Dedicated to Mirian Andrés