Formalization of the arithmetization of Euclidean plane geometry and applications
From MaRDI portal
Publication:1640646
DOI10.1016/j.jsc.2018.04.007zbMath1394.68349OpenAlexW2739437798MaRDI QIDQ1640646
Gabriel Braun, Julien Narboux, Pierre Boutry
Publication date: 14 June 2018
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf
Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35) Elementary problems in Euclidean geometries (51M04) Foundations of classical theories (including reverse mathematics) (03B30)
Related Items
A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Proof-checking Euclid ⋮ Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries ⋮ Euclid after Computer Proof-Checking ⋮ Tarski geometry axioms. IV: Right angle ⋮ Towards an intelligent and dynamic geometry book ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Formalization of the Poincaré disc model of hyperbolic geometry
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automated theorem proving in GeoGebra: current achievements
- On the unavoidable uncertainty of truth in dynamic geometry proving
- Towards a certified version of the encyclopedia of triangle centers
- The area method. A recapitulation
- A constructive version of Tarski's geometry
- Tarski geometry axioms
- On the existence of a equilateral triangle in \(H\)-planes
- Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
- A set of postulates for plane geometry, based on scale and protractor
- Formalization and specification of geometric knowledge objects
- Formalizing complex plane geometry
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Finding proofs in Tarskian geometry
- Proof and Computation in Geometry
- From Tarski to Hilbert
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
- An Introduction to Java Geometry Expert
- Formalization of Wu’s Simple Method in Coq
- A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- Tarski's System of Geometry
- Hilbert's ϵ‐operator in intuitionistic type theories
- Machine Proofs in Geometry
- Mechanical Theorem Proving in Tarski’s Geometry
- Theorem Proving in Higher Order Logics
- GCLC — A Tool for Constructive Euclidean Geometry and More Than That
This page was built for publication: Formalization of the arithmetization of Euclidean plane geometry and applications
