PhD Proposals Automated theorem proving (ATP) in geometry has two major lines of research:

axiomatic proof style and algebraic proof style (see [6], for instance, for a survey).

Algebraic proof style methods are based on reducing geometry properties to algebraic

properties expressed in terms of Cartesian coordinates. These methods are usually very

efficient, but the proofs they produce do not reflect the geometry nature of the problem

and they give only a yes/no conclusion. Axiomatic methods attempt to automate

traditional geometry proof methods that produce human-readable proofs. Building on

top of the existing ATPs (namely GCLCprover [5, 4, 8, 9, 10] to the area method [1, 2, 3,

7, 8, 11] or ATPs dealing with construction [6] the goal is to built an ATP capable of

producing human-readable proofs, with a clean connection between the geometric

conjectures and theirs proofs.