A formalization of metric spaces in HOL Light

DOI10.1007/s10817-017-9412-xzbMath1425.68376OpenAlexW2289810656MaRDI QIDQ682381

Marco Maggesi

Publication date: 2 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9412-x

zbMATH Keywords

metric spaceshigher-order logicformalization of mathematics

Mathematics Subject Classification ID

Metric spaces, metrizability (54E35)

Related Items

The flow of ODEs: formalization of variational equation and Poincaré map, From types to sets by local type definition in higher-order logic, Quantitative continuity and Computable Analysis in Coq

Uses Software

• Isabelle/HOL
• HOL Light
• IMPS

Cites Work

• Unnamed Item
• Some new results on decidability for elementary algebra and geometry
• IMPS: An interactive mathematical proof system
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Theorem Proving in Higher Order Logics