The mechanization theorem of (ordinary) unordered geometry

  • Wen-tsün Wu
Part of the Texts and Monographs in Symbolic Computation book series (TEXTSMONOGR)


This is the principal chapter of the book. It aims to prove that if the associated number system of a certain geometry is a number field, i.e., multiplication is commutative, then the proving of theorems whose hypotheses and conclusions can be expressed as polynomial equality relations is mechanizable. This class of theorems will be called theorems of equality type. In fact, this class contains most of the important theorems in elementary geometries though it excludes theorems involving order relations and thus polynomial inequalities in the algebraic relations. However, the latter does not often occur except in high school Euclidean geometry. In modern geometries such as algebraic geometry, the associated number fields are usually the complex field and arbitrary fields of characteristic 0, so no order relation is involved. Therefore it is compatible with the current state of geometry to restrict mechanical proving to theorems that can be expressed by means of only equalities.


Algebraic Variety Extension Field Mechanical Method Irreducible Factor Quadratic Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Wien 1994

Authors and Affiliations

  • Wen-tsün Wu
    • 1
  1. 1.Institute of Systems ScienceAcademia SinicaBeijingPeople’s Republic of China

Personalised recommendations