Formalizing complex plane geometry (Q2354913): Difference between revisions

@@ Property / DOI @@
-.1007/s10472-014-9436-4
@@ Property / DOI: 10.1007/s10472-014-9436-4 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OpenGeoProver
@@ Property / describes a project that uses: OpenGeoProver / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10472-014-9436-4
+Normal rank
@@ Property / OpenAlex ID @@
+W2073744707
@@ Property / OpenAlex ID: W2073744707 / rank @@
+Normal rank
@@ Property / cites work @@
+Setoids in type theory
@@ Property / cites work: Setoids in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Pragmatic Quotient Types in Coq
@@ Property / cites work: Pragmatic Quotient Types in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q4531863
@@ Property / cites work: Q4531863 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization of Wu’s Simple Method in Coq
@@ Property / cites work: Formalization of Wu’s Simple Method in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736392
@@ Property / cites work: Q4736392 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
+Normal rank
@@ Property / cites work @@
+Constructive Type Classes in Isabelle
@@ Property / cites work: Constructive Type Classes in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Without Loss of Generality
@@ Property / cites work: Without Loss of Generality / rank @@
+Normal rank
@@ Property / cites work @@
+The HOL Light theory of Euclidean space
@@ Property / cites work: The HOL Light theory of Euclidean space / rank @@
+Normal rank
@@ Property / cites work @@
+Q5181920
@@ Property / cites work: Q5181920 / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+The area method. A recapitulation
@@ Property / cites work: The area method. A recapitulation / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Projective Plane Geometry in Coq
@@ Property / cites work: Formalizing Projective Plane Geometry in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Hilbert’s Grundlagen in Isabelle/Isar
+Normal rank
@@ Property / cites work @@
+Q2770178
@@ Property / cites work: Q2770178 / 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 @@
+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 @@
+Q3678266
@@ Property / cites work: Q3678266 / rank @@
+Normal rank
@@ Property / cites work @@
+The axioms of constructive geometry
@@ Property / cites work: The axioms of constructive geometry / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S10472-014-9436-4
@@ Property / DOI: 10.1007/S10472-014-9436-4 / rank @@
+Normal rank