GeoProof: A user interface for formal proofs in geometry
Abstract:
In this paper, we demonstrate using videos the concrete use of the
software GeoProof : a user interface for formal proofs in geometry. This
paper is a multimedia complement for [20]. GeoProof is dynamic geometry
software extended with some proof related features. It can be used to
construct, explore, measure and invent conjectures about a geometric
configuration. Then, the conjecture can be proved either interactively
using the Coq proof assistant, or automatically using an automated theorem
prover. Two automated theorem provers are available : the first one is
embedded in the software and the second one is formalised in the Coq proof
assistant.