Automating Elementary Number-Theoretic Proofs Using Gröbner Bases

DOI10.1007/978-3-540-73595-3_5MaRDI QIDQ3608762zbMATH OpenOpenAlexFDO

Authors

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73595-3_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Multiplicative structure; Euclidean algorithm; greatest common divisors (11A05)

Recommendations

• Theorem proving for and with Gröbner bases theory
• scientific article; zbMATH DE number 1070620
• scientific article; zbMATH DE number 62658
• Mechanical geometry theorem proving based on Gröbner bases
• scientific article; zbMATH DE number 782043

Cited in

(7)

• Formalization of Wu's simple method in Coq
• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• Formal Proof of the Group Law for Edwards Elliptic Curves
• Formal power series
• \textsc{CoqCryptoLine}: a verified model checker with certified results
• Certified verification for algebraic abstraction
• Algorithm and abstraction in formal mathematics

Describes a project that uses

Uses Software

• HOL Light

This page was built for publication: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608762)