scientific article; zbMATH DE number 1745043
From MaRDI portal
Publication:4531863
Recommendations
Cited in
(22)- Formalization of Hilbert's geometry of incidence and parallelism
- A common axiom set for classical and intuitionistic plane geometry
- Formalizing mathematics in higher-order logic: A case study in geometric modelling
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Retrieving geometric information from images: the case of hand-drawn diagrams
- Formalization of the Poincaré disc model of hyperbolic geometry
- Formalizing complex plane geometry
- A synthetic proof of Pappus' theorem in Tarski's geometry
- A review and prospect of readable machine proofs for geometry theorems
- From informal to formal proofs in Euclidean geometry
- Two cryptomorphic formalizations of projective incidence geometry
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Formal specification and proofs for the topology and classification of combinatorial surfaces
- The area method. A recapitulation
- A case study in formalizing projective geometry in Coq: Desargues theorem
- An intuitionistic formula hierarchy based on high‐school identities
- Mechanical Theorem Proving in Tarski’s Geometry
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Complex_Geometry
- Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4531863)
