An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time (Q3102743): Difference between revisions

@@ Property / author @@
+Jacques D. Fleuriot
@@ Property / author: Jacques D. Fleuriot / 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_11
+Normal rank
@@ Property / OpenAlex ID @@
+W1708936760
@@ Property / OpenAlex ID: W1708936760 / rank @@
+Normal rank
@@ Property / cites work @@
+Hilbert's ``Grundlagen der Geometrie''
@@ Property / cites work: Hilbert's ``Grundlagen der Geometrie'' / rank @@
+Normal rank
@@ Property / cites work @@
+Q5572275
@@ Property / cites work: Q5572275 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4001973
@@ Property / cites work: Q4001973 / 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 @@
+Automated Deduction in Geometry
@@ Property / cites work: Automated Deduction in Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+The use of machines to assist in rigorous proof
@@ Property / cites work: The use of machines to assist in rigorous proof / rank @@
+Normal rank
@@ Property / cites work @@
+Composable Discovery Engines for Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+David Hilbert and his mathematical work
@@ Property / cites work: David Hilbert and his mathematical work / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790672
@@ Property / cites work: Q4790672 / rank @@
+Normal rank