Formalization of the Poincaré disc model of hyperbolic geometry

DOI10.1007/s10817-020-09551-2OpenAlexW3022308686MaRDI QIDQ2031408

Danijela Simić, Filip Marić, Pierre Boutry

Publication date: 9 June 2021

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

Full work available at URL: https://hal.inria.fr/hal-03120829/file/Poincare.pdf

zbMATH Keywords

Poincaré modelIsabelle/HOLformalization of geometry

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Automated triangle constructions in hyperbolic geometry

Uses Software

• Coq
• Isabelle/HOL
• Isabelle/Isar
• Transfer
• Lifting
• Archive Formal Proofs
• GeoCoq
• Poincare_Disc
• Complex_Geometry

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• A case study in formalizing projective geometry in Coq: Desargues theorem
• A constructive version of Tarski's geometry
• Tarski geometry axioms
• Isabelle/HOL. A proof assistant for higher-order logic
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Klein-Beltrami model. I
• Klein-Beltrami model. II
• The foundation of a generic theorem prover
• Formalizing generalized maps in Coq
• The axioms of constructive geometry
• Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
• Formalizing complex plane geometry
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• A synthetic proof of Pappus' theorem in Tarski's geometry
• Finding proofs in Tarskian geometry
• Theorem proving in infinitesimal geometry
• Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls
• From Tarski to Hilbert
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• Without Loss of Generality
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Tarski's System of Geometry
• Natural deduction as higher-order resolution
• Mechanical Theorem Proving in Tarski’s Geometry
• Automated Deduction in Geometry
• Alfred Tarski
• Formal Study of Plane Delaunay Triangulation
• Interpretation of Locales in Isabelle: Theories and Proof Contexts

This page was built for publication: Formalization of the Poincaré disc model of hyperbolic geometry