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
Complete list of metadatas

https://hal.inria.fr/inria-00070394
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 8:22:31 PM
Last modification on : Thursday, February 14, 2019 - 5:48:01 PM
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

211

Files downloads

224