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

https://hal.inria.fr/inria-00118903
Contributor : Julien Narboux <>
Submitted on : Thursday, December 7, 2006 - 9:44:41 AM
Last modification on : Wednesday, September 16, 2020 - 4:52:18 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 11:59:27 PM

Files

JARuitp-narboux.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

522

Files downloads

544