Verification of non-linear overconstraints in Euclidean geometry with linear programming

This paper is about one representation of constructible numbers which allows use of solver of linear constraints. A implementation is given in PrologIII and experiments are discussed.