Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Simplifying Polynomial Expressions in a Proof Assistant

Laurent Théry 1 
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper presents a simple way of performing polynomial simplifications in a proof assistant. This method has been implemented and tested within the Coq prover.
Document type :
Reports (Research report)
Complete list of metadata

https://hal.inria.fr/inria-00070394
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 8:22:31 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:21 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:06:46 PM

Identifiers

  • HAL Id : inria-00070394, version 1

Collections

Citation

Laurent Théry. Simplifying Polynomial Expressions in a Proof Assistant. [Research Report] RR-5614, INRIA. 2005, pp.16. ⟨inria-00070394⟩

Share

Metrics

Record views

126

Files downloads

173