É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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)