Formalization of Wu's simple method in Coq
From MaRDI portal
Recommendations
Cites work
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- A graphical user interface for formal proofs in geometry
- A new theorem discovered by computer prover
- An introduction to Java geometry expert. (Extended abstract)
- Automated Deduction in Geometry
- Automated Deduction in Geometry
- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
- Context Aware Calculation and Deduction
- scientific article; zbMATH DE number 4164173 (Why is no real title available?)
- scientific article; zbMATH DE number 1348459 (Why is no real title available?)
- Machine Proofs in Geometry
- Proof certificates for algebra and their application to automatic geometry theorem proving
- The area method. A recapitulation
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Without Loss of Generality
Cited in
(11)- Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Towards an intelligent and dynamic geometry book
- Theorem of three circles in Coq
- Formalizing complex plane geometry
- Two cryptomorphic formalizations of projective incidence geometry
- scientific article; zbMATH DE number 1670755 (Why is no real title available?)
- Proof certificates for algebra and their application to automatic geometry theorem proving
- Computer theorem proving for verifiable solving of geometric construction problems
- Two new ways to formally prove Dandelin-Gallucci's theorem
- Automated analysis of the difficulty of secondary school geometry theorems
Describes a project that uses
Uses Software
This page was built for publication: Formalization of Wu's simple method in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100204)
