Automated Theorem Proving

Abstract

In modern algebraic methods for automated geometry theorem proving, Wu's characteristic set method (Wu, 1978, 1994; Chou, 1988) and the Gr{ö}bner basis method (Buchberger, Collins and Kutzler, 1988; Kutzler and Stifter, 1986; Kapur, 1986) are two basic ones. In these methods, the first step is to set up a coordinate system, and represent the geometric entities and constraints in the hypothesis of a theorem by coordinates and polynomial equations. The second step is to compute a characteristic set or Gr{ö}bner basis by algebraic manipulations among the polynomials. The third step is to verify the conclusion of the theorem by using the characteristic set or Gr{ö}bner basis.