The HOL Light theory of Euclidean space
type: Item
instance of: scholarly article
title: The HOL Light theory of Euclidean space
zbMATH Open document ID: 1260.68373
author: Yanyan Li
published in: Journal of Automated Reasoning
publication date: 2013-04-17T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6154928
zbMATH Keywords: formalized mathematics
zbMATH Keywords: Euclidean space
zbMATH Keywords: vector space
zbMATH Keywords: \texttt{HOL Light}
describes a project that uses: Mizar
describes a project that uses: Sledgehammer
describes a project that uses: Flyspeck
describes a project that uses: Coq
describes a project that uses: Automath
describes a project that uses: Gandalf
describes a project that uses: kepler98
describes a project that uses: Jordan
describes a project that uses: HOL Light
MaRDI profile type: Publication
full work available at URL: s10817-012-9250-9
OpenAlex ID: W2091456056
cites work: Q4736392
cites work: The Jordan Curve Theorem, Formally and Informally
cites work: A revision of the proof of the Kepler conjecture
cites work: Theorem Proving in Higher Order Logics
cites work: Without Loss of Generality
cites work: Importing HOL Light into Coq
cites work: Some Combinatorial Lemmas in Topology
cites work: Q4218971
cites work: Q4258069
DOI: 10.1007/S10817-012-9250-9
description: scientific article; zbMATH DE number 6154928