Overview

Objectives of the proposed collaborative project (2012-2013) are in machine verifiable formalizations (within proof-assistants) of various geometries. Also, the project will aim at making progress in the field of automated theorem proving in geometry and in automated solving of geometry construction problems. More concretely, some of the goals are: formalization of Tarski's geometry using automated theorem provers for coherent logic (being developed by the Serbian partner group) and following experiences of the French partner group in similar task (formalization of Tarski's geometry within Coq). Also, some properties of algebraic methods (Wu's method and Grobner basis method) will be formalized and these methods will be integrated into interactive proof assistants. New methods for solving construction problems by ruler&compass will be developed, implemented and supported by formal proofs. Within the project, theorem proving and construction problem solving features will be integrated within dynamic geometry systems.