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 等数据库收录! |
|