The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

Hi Christophe,

We formalized Hessenberg's Theorem (Pappus implies Desargues) in Coq, 
using an automated prover for coherent logic, see [1].

The proof is based on the following axiomatization of elementary plane 
geometry
using the primitive "incidence" relation between points and lines:
- Any two points are incident with a line.
- Any two lines are incident with a point.
- Two distinct points cannot both be incident with two distinct lines.

Pappus axiom states:
  If alternate vertices of a hexagon lie on two lines, the three pairs of
  opposite sides meet in three collinear points.

Desargues' axiom:
  Two triangles perspective from a point are perspective from a line.

For more information about the formalization and the prover see 
<http://www.cs.vu.nl/~diem/research/ht/>.

[1] Marc Bezem and Dimitri Hendriks
  On the Mechanization of the Proof of Hessenberg’s Theorem in Coherent Logic
  Journal of Automated Reasoning, 40(1):61-85, 2008.
  avaliable at: <http://www.springerlink.com/content/4444557426p65637/>.

Dimitri

On Jul 20, 2011, at 16:02 , Christophe BAL wrote:

> 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.