Description: 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.
To Search:
File list (Check if you may need any files):
PhDPropsversion4.pdf
Download