Élimination des quantificateurs sur les réels pour Coq

Résumé : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-00819482
Contributor : Assia Mahboubi <>
Submitted on : Wednesday, May 1, 2013 - 3:49:46 PM
Last modification on : Tuesday, November 19, 2019 - 12:04:08 PM
Long-term archiving on : Friday, August 2, 2013 - 4:05:58 AM

Files

jfla02.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00819482, version 1

Collections

Citation

Assia Mahboubi, Loïc Pottier. Élimination des quantificateurs sur les réels pour Coq. Journées Francophones des Langages Applicatifs, Jan 2002, Anglet, France. ⟨hal-00819482⟩

Share

Metrics

Record views

226

Files downloads

104