Reseña: A formalisation of metric spaces in HOL Light

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre topología titulado A formalisation of metric spaces in HOL Light.

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

Su resumen es

We present a computer formalisation of metric spaces in the HOL Light theorem prover. Basic results of the theory of complete metric spaces are proved. A simple decision procedure for the theory of metric space is implemented.

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