Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System |
| |
Authors: | David Delahaye Micaela Mayero |
| |
Affiliation: | CPR (CEDRIC), CNAM, Paris, France;LCR (LIPN), Université Paris Nord (Paris 13), Villetaneuse, France |
| |
Abstract: | We propose a decision procedure for algebraically closed fields based on a quantifier elimination method. The procedure is intended to build proofs for systems of polynomial equations and inequations. We describe how this procedure can be carried out in a proof assistant using a Computer Algebra system in a purely skeptical way. We present an implementation in the particular framework of Coq and Maple giving some details regarding the interface between the two tools. This allows us to show that a Computer Algebra system can be used not only to bring additional computational power to a proof assistant but also to enhance the automation of such tools. |
| |
Keywords: | Theorem Proving Computer Algebra Algebraically Closed Fields Coq" target="_blank">Coq Maple" target="_blank">Maple |
本文献已被 ScienceDirect 等数据库收录! |