HAL - INRIA :: [inria-00618745, version 2] Formalization of Wu's simple method in Coq

inria-00618745, version 2

Formalization of Wu's simple method in Coq

Jean-David Genevaux^a^, 1, Julien Narboux () ^1, 2, Pascal Schreck ()^a^, 1

CPP 2011 First International Conference on Certified Programs and Proofs 7086 (2011) 71-86

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.

a – Université de Strasbourg
1 : Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection (LSIIT)
CNRS : UMR7005 – Université de Strasbourg
2 : CAMUS (INRIA Lorraine)
INRIA

inria-00618745, version 2
http://hal.inria.fr/inria-00618745
oai:hal.inria.fr:inria-00618745
Contributeur : Julien Narboux <>
Soumis le : Mardi 20 Septembre 2011, 07:47:06
Dernière modification le : Mardi 7 Février 2012, 09:50:57

Voir la fiche détaillée

Documents associés

PDF :

DOI : 10.1007/978-3-642-25379-9_8

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="inria-00618745"><analytic>
<author><persName><forename>Jean-David</forename><surname>Genevaux</surname></persName>
<affiliation>
<orgName type="laboratory">LSIIT</orgName>
<orgName type="team">Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7005</orgName>
<orgName type="institution">Université de Strasbourg</orgName>
</affiliation>
</author>
<author><persName><forename>Julien</forename><surname>Narboux</surname></persName>
<affiliation>
<orgName type="laboratory">LSIIT</orgName>
<orgName type="team">Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7005</orgName>
<orgName type="institution">Université de Strasbourg</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Lorraine</orgName>
<orgName type="team">CAMUS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
</affiliation>
</author>
<author><persName><forename>Pascal</forename><surname>Schreck</surname></persName>
<affiliation>
<orgName type="laboratory">LSIIT</orgName>
<orgName type="team">Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7005</orgName>
<orgName type="institution">Université de Strasbourg</orgName>
</affiliation>
</author>
<title type="main" level="a">Formalization of Wu's simple method in Coq</title></analytic><monogr><meeting>CPP 2011 First International Conference on Certified Programs and Proofs</meeting><imprint><publisher>Springer-Verlag</publisher><pubPlace><settlement>Kenting</settlement><country>Taïwan, Province De Chine</country></pubPlace><biblScope type="publicationDate">2011-12-00</biblScope><biblScope type="vol">7086</biblScope><biblScope type="pp">71-86</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-25379-9_8</idno><idno type="HALid">http://hal.inria.fr/inria-00618745</idno><idno type="HALFile">http://hal.inria.fr/inria-00618745/PDF/document.pdf</idno></biblStruct>
</listBibl>
</listBibl>