Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Thursday, December 7, 2006 - 9:44:41 AM
Last modification on : Friday, February 4, 2022 - 3:23:00 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 11:59:27 PM


Files produced by the author(s)



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⟩



Record views


Files downloads