Formalization of the Poincaré disc model of hyperbolic geometry
type: Item
instance of: scholarly article
title: Formalization of the Poincaré disc model of hyperbolic geometry
author: Danijela Simić
author: Filip Marić
author: Pierre Boutry
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
full work available at URL: Poincare.pdf
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7356967
zbMATH Keywords: Poincaré model
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: formalization of geometry
describes a project that uses: Archive Formal Proofs
describes a project that uses: GeoCoq
describes a project that uses: Isabelle/Isar
describes a project that uses: Poincare_Disc
describes a project that uses: Complex_Geometry
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Transfer
describes a project that uses: Lifting
MaRDI profile type: Publication
OpenAlex ID: W3022308686
cites work: Interpretation of Locales in Isabelle: Theories and Proof Contexts
cites work: A constructive version of Tarski's geometry
cites work: Finding proofs in Tarskian geometry
cites work: Q3270252
cites work: Formalization of the arithmetization of Euclidean plane geometry and applications
cites work: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
cites work: From Tarski to Hilbert
cites work: A synthetic proof of Pappus' theorem in Tarski's geometry
cites work: Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls
cites work: Klein-Beltrami model. I
cites work: Klein-Beltrami model. II
cites work: Q4434670
cites work: The development of Euclidean axiomatics. The systems of principles and the foundations of mathematics in editions of the \textit{Elements} in the early modern age
cites work: Formalizing generalized maps in Coq
cites work: Q4531863
cites work: Formal Study of Plane Delaunay Triangulation
cites work: Q4530838
cites work: Theorem proving in infinitesimal geometry
cites work: Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL
cites work: Without Loss of Generality
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
cites work: A case study in formalizing projective geometry in Coq: Desargues theorem
cites work: Formalizing complex plane geometry
cites work: Alfred Tarski
cites work: Formalizing Hilbert’s Grundlagen in Isabelle/Isar
cites work: Automated Deduction in Geometry
cites work: Mechanical Theorem Proving in Tarski’s Geometry
cites work: Q4556039
cites work: Q3128958
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q4094049
cites work: Natural deduction as higher-order resolution
cites work: The foundation of a generic theorem prover
cites work: Q4790670
cites work: Tarski geometry axioms
cites work: Q3678266
cites work: Q3943557
cites work: An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
cites work: Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
cites work: Tarski's System of Geometry
cites work: The axioms of constructive geometry
DOI: 10.1007/S10817-020-09551-2
Recommended article: Q4918692
Recommended article: Q5172388
Recommended article: Q2937068
Recommended article: Q4914898
Recommended article: Q3003206
Recommended article: Q3003207
Recommended article: The geometry of poincaré disks
Recommended article: Q3458551
Recommended article: Q3069541
description: scientific article; zbMATH DE number 7356967