Reseña: A symbolic approach to abstract algebra in HOL Light

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre álgebra titulado A symbolic approach to abstract algebra in HOL Light.

Su autor es Marco Maggesi (de la Univ. de Florencia en Italia).

Su resumen es

Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, …) is known to be challenging task which is often undertaken by exploiting various kind of extra-logical mechanisms (axiomatic classes, modules, locales, coercions, …) provided by most modern theorem provers.

We want to explore an alternative strategy, where algebraic structures are implemented via a deep embedding of mathematical formulas and are managed as first class objects in the HOL theory. Along the way, we provide a mechanism of generalised conversions, which extends Paulson’s conversions by allowing to compute with equivalence relations. We developed generalised conversions to support rewriting in our system, but they can be used independently and may have an interest in its own.

El trabajo se ha presentado en CICM 2015 (the 8th Conference on Intelligent Computer Mathematics).

El código de las correspondientes teorías en HOL Light se encuentra aquí.