将格罗布纳基程序与Coq程序相结合进行代数、几何和算术证明
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics
摘要：
我们描述了我们如何连接三个程序，计算Groebner基地Coq，做自动证明代数，几何和算术表达式。其结果是一套Coq策略和证书机制（可在http：//www-sop.inria.fr/marelle/Loic.Pottier/gb-keappa.tgz下载）。这些程序是：F4、GB \和gbcoq。F4和GB是计算Groebner基的最快的（据我们所知）可用程序。Gbcoq通常很慢，但被证明是正确的（在Coq中），我们将其应用于我们的特定问题以提高效率。自动化证明涉及系数和不定式在R或Z中的多项式的等式和非等式，并且通过希尔伯特的零点变换（Nullstellenetron）减少到Groebner计算来完成。我们也适应哈里森的结果，允许证明一些定理的模算术。Coq和计算Groebner基的程序之间的连接是使用Coq的“外部”策略完成的，该策略允许调用接受xml输入和输出的任意程序。我们还制作证书，以使证明脚本独立于外部程序。
英文摘要：
We describe how we connected three programs that compute Groebner bases to Coq, to do automated proofs on algebraic, geometrical and arithmetical expressions. 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 our knowledge) available programs that compute Groebner bases. Gbcoq is slow in general but is proved to be correct (in Coq), and we adapted it to our specific problem to be efficient. The automated proofs concern equalities and non-equalities on polynomials with coefficients and indeterminates in R or Z, and are done by reducing to Groebner computation, via Hilbert's Nullstellensatz. We adapted also the results of Harrison, to allow to prove some theorems about modular arithmetics. The connection between Coq and the programs that compute Groebner bases is done using the "external" tactic of Coq that allows to call arbitrary programs accepting xml inputs and outputs. We also produce certificates in order to make the proof scripts independant from the external programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
