Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408): Difference between revisions

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