Ordering in automated theorem proving of differential geometry (Q1299842)

The authors propose a new ordering method for automated theorem proving in differential geometry, called ``hybrid ordering method'', which is compatible with both, Cartan's method of moving frames and Wu's elimination principle. The basic idea is to change part of an element-based order to a degree-based order according to given hypotheses. In Section 2, the authors describe their so-called hybrid ordering method, then, in Section 3, they present some examples to produce such kind of orders for problems in differential geometry. For related papers see the first author: Sci. China, Ser. A 40, No. 4, 350-356 (1997; Zbl 0880.68117).