A case-study in algebraic manipulation using mechanized reasoning tools

  1. Aransay, J. 1
  2. Domínguez, C. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
International Journal of Computer Mathematics

ISSN: 0020-7160

Año de publicación: 2010

Volumen: 87

Número: 9

Páginas: 1936-1949

Tipo: Artículo

DOI: 10.1080/00207160802676604 SCOPUS: 2-s2.0-77954906427 WoS: WOS:000280153000003 GOOGLE SCHOLAR

Otras publicaciones en: International Journal of Computer Mathematics

Proyectos relacionados

Gestión Mecanizada del Conocimiento Matemático. Aplicaciones en Topología Algebraica y en Lógica.

2009/00207/001

Resumen

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. © 2010 Taylor & Francis.