Published January 28, 2002 | Version v1
Conference paper Metadata-only

Élimination des quantificateurs sur les réels pour Coq

Creators

Contributors

Description

On présente ici l'implémentation en OCaml d'une tactique Coq qui réalise une procédure d'élimination des quantificateurs pour les réels, basée sur la méthode de Hormander.

Abstract

National audience

Additional details

Identifiers

URL
https://inria.hal.science/hal-00819482
URN
urn:oai:HAL:hal-00819482v1

Origin repository

Origin repository
UNICA