A Graphical User Interface for Formal Proofs in Geometry |
| |
| Authors: | Julien Narboux |
| |
| Affiliation: | 1.Project PCRI P?le Commun de Recherche en Informatique du plateau de Saclay, CNRS, école Polytechnique, INRIA,Université Paris-Sud,Paris,France |
| |
| 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. |
| |
| Keywords: | Geometry Theorem prover Proof assistant Interface Coq Dynamic geometry Automated theorem proving |
| 本文献已被 SpringerLink 等数据库收录！ |
|
