English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We describe how we connected three programs that compute Groebner bases toCoq, to do automated proofs on algebraic, geometrical and arithmeticalexpressions. The result is a set of Coq tactics and a certificate mechanism(downloadable at http://www-sop.inria.fr/marelle/Loic.Pottier/gb-keappa.tgz).The programs are: F4, GB \, and gbcoq. F4 and GB are the fastest (up to ourknowledge) available programs that compute Groebner bases. Gbcoq is slow ingeneral but is proved to be correct (in Coq), and we adapted it to our specificproblem to be efficient. The automated proofs concern equalities andnon-equalities on polynomials with coefficients and indeterminates in R or Z,and are done by reducing to Groebner computation, via Hilbert'sNullstellensatz. We adapted also the results of Harrison, to allow to provesome theorems about modular arithmetics. The connection between Coq and theprograms that compute Groebner bases is done using the "external" tactic of Coqthat allows to call arbitrary programs accepting xml inputs and outputs. Wealso produce certificates in order to make the proof scripts independant fromthe external programs.

Connecting Gr\"obner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics