首页 | 本学科首页   官方微博 | 高级检索  
     


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 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号