Mon 12 Jan 2026 11:44 - 12:06 at Belvédère - Formalized mathematics Chair(s): Marie Kerjean, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
The Cylindrical Algebraic Decomposition (CAD in short) is a fundamental tool of semi-algebraic geometry. It is a doubly- exponential time algorithm that enables most famously to eliminate quantifiers from a formula in the theory of real closed fields. In particular, it allows to decide the satisfiability of problems involving sets of comparisons between polyno- mials. The present article describes the first formalization of a correctness proof of this algorithm in a proof assistant.
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:50 | Formalized mathematicsCPP at Belvédère Chair(s): Marie Kerjean CNRS, Université Sorbonne Paris Nord, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Inria, Université Jean Monnet Saint-Étienne | ||
11:00 22mTalk | Bar Inductive Predicates for Constructive Algebra in Rocq CPP Dominique Larchey-Wendling Université de Lorraine, CNRS, LORIA DOI Pre-print | ||
11:22 22mTalk | Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq CPP Holger Thies Kyoto University | ||
11:44 22mTalk | Cylindrical Algebraic Decomposition in Coq/Rocq CPP Quentin Vermande Université Côte d'Azur, Inria | ||
12:06 22mTalk | Adhesive Category Theory for Graph Rewriting in Rocq CPP | ||
12:28 22mTalk | Formalizing polynomial laws and the universal divided power algebra CPP | ||