Mechanical Theorem Proving in Geometries pp 149-211 | Cite as

# The mechanization theorem of (ordinary) unordered geometry

## Abstract

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.

## Keywords

Algebraic Variety Extension Field Mechanical Method Irreducible Factor Quadratic Relation## Preview

Unable to display preview. Download preview PDF.