Ordering in mechanical geometry theorem proving

Ordering in mechanical geometry theorem proving is studied from geometric viewpoint and some new ideas are proposed. For Thebault’s theorem which is the most difficult theorem that has ever been proved by Wu’s method, a very simple proof using Wu’s method under a linear order is discovered. Project supported by the National Natural Science Foundation of China.