Formalization of Wu's simple method in Coq - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Formalization of Wu's simple method in Coq

Résumé

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.

Domaines

Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
document.pdf (383.53 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Julien Narboux  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/inria-00618745

Soumis le : mardi 20 septembre 2011-07:47:06

Dernière modification le : vendredi 24 mars 2023-14:52:54

Archivage à long terme le : dimanche 4 décembre 2016-05:29:12

Télécharger pour visualiser

Dates et versions

inria-00618745 , version 1 (02-09-2011)
inria-00618745 , version 2 (20-09-2011)

Identifiants

Citer

Jean-David Génevaux, Julien Narboux, Pascal Schreck. Formalization of Wu's simple method in Coq. CPP 2011 First International Conference on Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. pp.71-86, ⟨10.1007/978-3-642-25379-9_8⟩. ⟨inria-00618745v2⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

CNRS
165 Consultations
628 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More