Formalizing constructive quantifier elimination in Agda

MaRDI QIDQ3384907zbMATH OpenFDO

Authors Jeremy Pope

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1807.04083, http://eptcs.web.cse.unsw.edu.au/paper.cgi?MSFP2018.2

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• A formal quantifier elimination for algebraically closed fields
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Linear quantifier elimination
• Linear Quantifier Elimination
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic

Cites work

• scientific article; zbMATH DE number 3349763 (Why is no real title available?)
• scientific article; zbMATH DE number 3099243 (Why is no real title available?)
• A formal quantifier elimination for algebraically closed fields
• Alfred Tarski and decidable theories
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Linear quantifier elimination

This page was built for publication: Formalizing constructive quantifier elimination in Agda

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384907)