A Graphical User Interface for Formal Proofs in Geometry.

Julien Narboux 1, 2
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : We present in this paper the design of a graphical user interface to deal with proofs in geometry. The software developed combines three tools: a dynamic geometry software to explore, measure and invent conjectures, an automatic theorem prover to check facts and an interactive proof system (Coq) to mechanically check proofs built interactively by the user.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2007, Special Issue on User Interfaces in Theorem Proving, 39 (2), pp.161-180. 〈10.1007/s10817-007-9071-4〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00118903
Contributeur : Julien Narboux <>
Soumis le : jeudi 7 décembre 2006 - 09:44:41
Dernière modification le : jeudi 10 mai 2018 - 02:06:14
Document(s) archivé(s) le : mardi 6 avril 2010 - 23:59:27

Fichiers

JARuitp-narboux.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Julien Narboux. A Graphical User Interface for Formal Proofs in Geometry.. Journal of Automated Reasoning, Springer Verlag, 2007, Special Issue on User Interfaces in Theorem Proving, 39 (2), pp.161-180. 〈10.1007/s10817-007-9071-4〉. 〈inria-00118903〉

Partager

Métriques

Consultations de la notice

293

Téléchargements de fichiers

173