Title
A Graphical User Interface for Formal Proofs in Geometry
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.
Year
DOI
Venue
2007
10.1007/s10817-007-9071-4
J. Autom. Reasoning
Keywords
Field
DocType
Geometry,Theorem prover,Proof assistant,Interface,Coq,Dynamic geometry,Automated theorem proving
Interactive proof system,Computer science,Theoretical computer science,Graphical user interface,Software,Graphical user interface testing,Geometry,Discrete mathematics,Algorithm,Automated proof checking,Mathematical proof,User interface,Proof assistant
Journal
Volume
Issue
ISSN
39
2
0168-7433
Citations 
PageRank 
References 
21
1.25
14
Authors
1
Name
Order
Citations
PageRank
Julien Narboux113012.49