A METHOD FOR MECHANICAL GEOMETRY THEOREM PROVING

摘要

A method for mechanical geometry theorem proving is presented. By using this method, if the ascending chains derived via Wu-Ritt's well ordering algorithm satisfy a condition, all the irreducible characteristic sets we need can be obtained at the same time, and the general case can be reduced to this special case. Thus whether a geometry theorem is generally true can be decided.