A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry (Q3102734): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / 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_3
+Normal rank
@@ Property / OpenAlex ID @@
+W1523528291
@@ Property / OpenAlex ID: W1523528291 / rank @@
+Normal rank
@@ Property / cites work @@
+On the exterior calculus of invariant theory
@@ Property / cites work: On the exterior calculus of invariant theory / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q5690444
@@ Property / cites work: Q5690444 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Foundations of Combinatorial Theory: IX Combinatorial Methods in Invariant Theory
+Normal rank
@@ Property / cites work @@
+A geometric identity for Pappus' theorem.
@@ Property / cites work: A geometric identity for Pappus' theorem. / rank @@
+Normal rank
@@ Property / cites work @@
+Clifford algebra to geometric calculus. A unified language for mathematics and physics
+Normal rank
@@ Property / cites work @@
+Automated Deduction in Geometry
@@ Property / cites work: Automated Deduction in Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
+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 @@
+INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
@@ Property / cites work: INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH / rank @@
+Normal rank
@@ Property / cites work @@
+Algorithms in invariant theory
@@ Property / cites work: Algorithms in invariant theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q5690441
@@ Property / cites work: Q5690441 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3837774
@@ Property / cites work: Q3837774 / rank @@
+Normal rank