Formalization of Wu's simple method in Coq

Abstract : We present in this paper the integration within the Coq proof assistant, of a method for automatic theorem proving in geometry. We use an approach based on the validation of a certificate. The certificate is generated by an implementation in Ocaml of a simple version of Wu's method.
Type de document :
Communication dans un congrès
Jean-Pierre Jouannaud and Zhong Shao. CPP 2011 First International Conference on Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. Springer-Verlag, 7086, pp.71-86, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-25379-9_8〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00618745
Contributeur : Julien Narboux <>
Soumis le : mardi 20 septembre 2011 - 07:47:06
Dernière modification le : samedi 13 janvier 2018 - 01:03:08
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 05:29:12

Fichier

document.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jean-David Génevaux, Julien Narboux, Pascal Schreck. Formalization of Wu's simple method in Coq. Jean-Pierre Jouannaud and Zhong Shao. CPP 2011 First International Conference on Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. Springer-Verlag, 7086, pp.71-86, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-25379-9_8〉. 〈inria-00618745v2〉

Partager

Métriques

Consultations de la notice

276

Téléchargements de fichiers

323