Simplifying Polynomial Expressions in a Proof Assistant

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.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/inria-00070394
Author Théry, Laurent
Maintainer CCSD
Last Updated May 16, 2026, 05:19 (UTC)
Created May 16, 2026, 05:19 (UTC)
Identifier Report N°: RR-5614
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Software and mathematics (LEMME) ; Centre Inria d'Université Côte d'Azur ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
creator Théry, Laurent
date 2005-05-16T00:00:00
harvest_object_id 2fb4379c-d541-4d5a-a2a6-9ee687ede1ab
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-08-26T00:00:00
set_spec type:REPORT