A constructive formalisation of Semi-algebraic sets and functions | Zendy

Boris Djalal | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A constructive formalisation of Semi-algebraic sets and functions

Author(s) -

Boris Djalal

Publication year - 2018

Publication title -

hal (le centre pour la communication scientifique directe)

Language(s) - English

Resource type - Conference proceedings

ISBN - 978-1-4503-5586-5

DOI - 10.1145/3167099

Subject(s) - correctness , decidability , constructive , algebraic number , quantifier elimination , computer science , exploit , algebra over a field , interpretation (philosophy) , base (topology) , algebraic operation , decomposition , mathematics , theoretical computer science , algorithm , programming language , pure mathematics , mathematical analysis , computer security , process (computing) , ecology , biology

Semi-algebraic sets and semi-algebraic functions are essential to specify and certify cylindrical algebraic decomposition algorithms. We formally define in Coq the base operations on semi-algebraic sets and functions using embedded first-order formulae over the language of real closed fields, and we prove the correctness of their geometrical interpretation. In doing so, we exploit a previous formalisation of quantifier elimination on such embedded formulae to guarantee the decidability of several first-order properties and keep our development constructive. We also exploit it to formalise formulae substitution without having to handle bound variables.

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