A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs (Q3102745): Difference between revisions

@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / 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/978-3-642-25070-5_12
+Normal rank
@@ Property / OpenAlex ID @@
+W144472580
@@ Property / OpenAlex ID: W144472580 / rank @@
+Normal rank
@@ Property / cites work @@
+A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i>
@@ Property / cites work: A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i> / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Coherent Logic
@@ Property / cites work: Automating Coherent Logic / rank @@
+Normal rank
@@ Property / cites work @@
+On the mechanization of the proof of Hessenberg's theorem in coherent logic
+Normal rank
@@ Property / cites work @@
+Q3270252
@@ Property / cites work: Q3270252 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2902935
@@ Property / cites work: Q2902935 / rank @@
+Normal rank
@@ Property / cites work @@
+\textit{Theorema}: Towards computer-aided mathematical theory exploration
+Normal rank
@@ Property / cites work @@
+Q2751363
@@ Property / cites work: Q2751363 / rank @@
+Normal rank
@@ Property / cites work @@
+Machine Proofs in Geometry
@@ Property / cites work: Machine Proofs in Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
+Normal rank
@@ Property / cites work @@
+A deductive database approach to automated geometry theorem proving and discovering
+Normal rank
@@ Property / cites work @@
+Q4531863
@@ Property / cites work: Q4531863 / rank @@
+Normal rank
@@ Property / cites work @@
+Skolem Machines and Geometric Logic
@@ Property / cites work: Skolem Machines and Geometric Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q3234138
@@ Property / cites work: Q3234138 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4874803
@@ Property / cites work: Q4874803 / rank @@
+Normal rank
@@ Property / cites work @@
+Using Gröbner bases to reason about geometry problems
+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 @@
+A case study in formalizing projective geometry in Coq: Desargues theorem
+Normal rank
@@ Property / cites work @@
+Formalizing Hilbert’s Grundlagen in Isabelle/Isar
+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 @@
+The axioms of constructive geometry
@@ Property / cites work: The axioms of constructive geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization of Hilbert's geometry of incidence and parallelism
+Normal rank
@@ Property / cites work @@
+Automated development of Tarski's geometry
@@ Property / cites work: Automated development of Tarski's geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Q3678266
@@ Property / cites work: Q3678266 / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+Efficiency of a Good But Not Linear Set Union Algorithm
+Normal rank
@@ Property / cites work @@
+Q4153620
@@ Property / cites work: Q4153620 / rank @@
+Normal rank