The Coq mailing list

[Julien Narboux <Julien AT narboux.fr>]

Hello,

I formalized some chapters of the book "Metamathematische Methoden in 
der Geometrie" by Swmiliew and Tarski.
But the proof are mainly "manual".
You can find the proofs here:
http://dpt-info.u-strasbg.fr/~narboux/tarski.html
and the paper here:
http://hal.inria.fr/inria-00118812/en

Sana Stojanovic, Vesna Pavlovic and Predrag Janicic have writen a paper 
about automated deduction using Coherent Logic and applied it to some 
lemmas derived from Tarski's axioms. See the paper "A Coherent Logic 
Based Geometry Theorem Prover Capable of Producing Formal and Readable 
Proofs" which will be published in ADG 2010 post proceedings.

Some consequence of Tarski axioms also appear in standard benchmarks for 
sat based provers (TPTP). But most provers can only prove trivial 
consequences of the axioms.

Concerning automated deduction in geometry in general (not using Tarski 
axioms).
There are several well known efficient methods which can prove hundreds 
of theorems, such as:
-1- groebner basis
-2- Wu's method
-3- the area method
-4- the full angle method
-5- geometric algebra methods


The methods 1,2, 3 and 5 have been (at least partially) formalized in 
Coq, here are some references:

* Predrag Janicic, Julien Narboux, Pedro Quaresma, The Area Method - A 
Recapitulation
* Laurent Fuchs and Laurent Théry. A Formalisation of Grassmann-Cayley 
Algebra in Coq. post-proceedings of ADG 2010.
* A Coq-based Library for Interactive and Automated Theorem Proving in 
Plane Geometry Pham T. M., Bertot Y., Narboux J. The 11th International 
Conference on Computational Science and Its Applications (ICCSA 2011) 
6703 (2011)
* Proof certificates for algebra and their application to automatic 
geometry theorem proving
Benjamin Grégoire, Loïc Pottier, Laurent Théry, post-proceedings 
ADG2008, LNAI 6301, 2011

I hope this helps.

Julien


Le 20/07/2011 16:02, Christophe BAL a écrit :
> Hello,
> I would like to know if someone has made some tools for automated 
> demonstration in plane Geometry using for example the Tarski axioms.
>
> Best regards.
> Christophe.