Formalizing complex plane geometry

DOI10.1007/S10472-014-9436-4zbMath1330.68264OpenAlexW2073744707MaRDI QIDQ2354913

Filip Marić, Danijela Petrović

Publication date: 27 July 2015

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-014-9436-4

zbMATH Keywords

Möbius transformationsinteractive theorem provingcomplex plane geometry

Mathematics Subject Classification ID

Möbius geometries (51B10)

Related Items (4)

Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Automated triangle constructions in hyperbolic geometry ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Formalization of the Poincaré disc model of hyperbolic geometry

Uses Software

• Isabelle/HOL
• Isar
• CeTA
• OpenGeoProver
• Transfer
• Lifting
• Archive Formal Proofs
• Matrix Operations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The area method. A recapitulation
• Isabelle/HOL. A proof assistant for higher-order logic
• The axioms of constructive geometry
• The HOL Light theory of Euclidean space
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
• Formalizing Projective Plane Geometry in Coq
• Formalization of Wu’s Simple Method in Coq
• Without Loss of Generality
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Constructive Type Classes in Isabelle
• Setoids in type theory
• Pragmatic Quotient Types in Coq
• Mechanical Theorem Proving in Tarski’s Geometry
• Theorem Proving in Higher Order Logics

This page was built for publication: Formalizing complex plane geometry