Abstract. 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.
A formalisation of metric spaces in HOL Light / Marco, Maggesi. - ELETTRONICO. - (2015), pp. 1-4.
A formalisation of metric spaces in HOL Light
Marco Maggesi
2015
Abstract
Abstract. 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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2015-07-15-FMM-metric.pdf
accesso aperto
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Tutti i diritti riservati
Dimensione
208.22 kB
Formato
Adobe PDF
|
208.22 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
