Using predicate logic to verify the theorems of Euclid's elements?

Question

I wanted to make a "logical" march through the entirety of Euclid's elements by proving and verifying, step by step, each theorem using Hilbert's axioms as a basis. Of course, I would want to do this all in the symbolic language of predicate logic using a natural deduction format. Has anyone out there done anything like this yet? What would Hilbert's axioms look like when translated into predicate logic? Any tips or pointers would be welcome. Thank you!

Answer 1

See :

• Sara Negri & Jan von Plato, Proof Analysis : A Contribution to Hilbert’s Last Problem (2011) : Part III. Proof systems for geometric theories, page 131-on.