Abstract : We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correction of our implementation of the subresultant algorithm. Up to our knowledge, it is the first mechanized proof of this result.
https://hal.inria.fr/inria-00001270 Contributor : Assia MahboubiConnect in order to contact the contributor Submitted on : Friday, April 28, 2006 - 7:12:19 PM Last modification on : Thursday, January 20, 2022 - 5:30:46 PM Long-term archiving on: : Saturday, April 3, 2010 - 9:46:38 PM
Assia Mahboubi. Proving formally the implementation of an efficient gcd algorithm for polynomials. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Aug 2006, Seattle, WA, United States. pp.438-452. ⟨inria-00001270⟩