Automatic theorem proving and discovering

in elementary geometry

Tomás Recio

Universidad de Cantabria at Santander, Spain

recio@matesco.unican.es

Three simple instances

The simple idea behind them

The elusive role of elimination

A formal approach