[Club2] Fr. 13.10; 11.30h; Turing

[Norbert Schirmer]

This Friday, 13.10 at 11.30 in Room Turing (00.09.055):

Julien Narboux:

"Formalization and automation of geometric reasoning within the 
Coq proof assistant."

Abstract:

In the first part we present a mechanization of the geometry of Tarski. 
This consists in the formalization of the first eight chapters of the 
book of Schwabäuser, Szmielew and Tarski: Metamathematische Methoden in 
der Geometrie.

In the second part, we present our implementation in Coq of a decision 
procedure for affine plane geometry : the area method of Chou, Gao and 
Zhang.

In the third part, we explain the design of graphical user interface for 
formal proof in geometry: GeoProof.
GeoProof combines a dynamic geometry software with a proof assistant.

Finally, we propose a diagrammatic formal system to perform proofs in 
the field of abstract term rewriting. For instance, using this system we 
can formalize the diagrammatic proof of the Newman's lemma. The system 
is proved correct and complete for a class of formulas called the 
coherent logic.



   Norbert