Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System | Zendy

David Delahaye | Zendy; Micaela Mayero | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System

Author(s) -

David Delahaye,

Micaela Mayero

Publication year - 2006

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.11.023

Subject(s) - quantifier elimination , mathematical proof , symbolic computation , algebra over a field , maple , polynomial , gas meter prover , computer science , algebraically closed field , interface (matter) , automation , programming language , mathematics , calculus (dental) , discrete mathematics , pure mathematics , engineering , maximum bubble pressure method , parallel computing , biology , mechanical engineering , medicine , dentistry , mathematical analysis , botany , geometry , bubble

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research