GeoView is a tool that combines the Coq theorem prover with the dynamic geometry drawing tool GeoplanJ developed at CNAM. GeoView is an extension of the user-interface Pcoq and is dedicated to the visualization of formal statements of plane geometrical theorems. The statements of geometrical theorems and their proofs are constructed and verified with Coq theorem prover. A dynamic figure is automatically associated to mathematical formulas to show the meaning of these statements. The figures generated with GeoView can be integrated as interactive and dynamic figures in HTML files using the GeoplanJ applet.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon: Automated theorem proving in GeoGebra: current achievements (2015)
- Pham, Tuan Minh; Bertot, Yves: A combination of a dynamic geometry software with a proof assistant for interactive formal proofs (2012)
- Quaresma, Pedro: Thousands of geometric problems for geometric theorem provers (TGTP) (2011)
- Janičić, Predrag: Geometry constructions language (2010)
- Janičić, Predrag; Quaresma, Pedro: Automatic verification of regular constructions in dynamic geometry systems (2007)
- Narboux, Julien: A graphical user interface for formal proofs in geometry (2007)
- Quaresma, Pedro; Janičić, Predrag: GeoThms -- a web system for Euclidean constructive geometry (2007)
- Quaresma, Pedro; Janičić, Predrag: Integrating dynamic geometry software, deduction systems, and theorem repositories (2006)