A combination of a dynamic geometry software with a proof assistant for interactive formal proofs - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

A combination of a dynamic geometry software with a proof assistant for interactive formal proofs

(1) , (1)
1
Tuan Minh Pham
  • Function : Author
  • PersonId : 898947
Yves Bertot

Abstract

This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software - Geogebra[11] with a proof assistant - Coq[8]. Thanks to the features of Geogebra, users can create and manipulate geometric constructions, they discover conjectures and interactively build formal proofs with the support of Coq. Our system allows users to construct fully traditional proofs in the same style as the ones in high school. For each step of proving, we provide a set of applicable rules veri ed in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
Fichier principal
Vignette du fichier
paper8.pdf (500.37 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00585400 , version 1 (12-04-2011)

Identifiers

  • HAL Id : inria-00585400 , version 1

Cite

Tuan Minh Pham, Yves Bertot. A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. 9th International Workshop On User Interfaces for Theorem Provers FLOC'10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom. ⟨inria-00585400⟩

Collections

INRIA INRIA2
179 View
395 Download

Share

Gmail Facebook Twitter LinkedIn More