World Scientific
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×

System Upgrade on Tue, May 28th, 2024 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at customercare@wspc.com for any enquiries.

ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY

    Reprinted from Scientia Sinica 21 (2), 1978.

    https://doi.org/10.1142/9789812791085_0008Cited by:5 (Source: Crossref)
    Abstract:

    The idea of proving theorems mechanically may be dated back to Leibniz in the 17th century and has been formulated in precise mathematical forms in this century through the school of Hilbert as well as his followers on mathematical logic. The problem consists in essence in replacing qualitative difficulties inherited in usual mathematical proofs by quantitative complexities of calculations on standardizing the proof procedures in an algorithmic manner. Such quantitative complexities of calculations, formerly far beyond the reach of human abilities, have become more and more trivial owing to the occurrence and rapid development of computers. In spite of vigorous efforts, however, researches in this direction give rise quite often to negative results in the form of undecidable mathematical theories. To cite a notable positive result, we may mention Tarski's method of proving theorems mechanically in elementary geometry and elementary algebra. The methods of Tarski as well as later ones are largely based on a generalization of Sturm theorem and are still too complicated to be feasible, even with the use of computers. The present paper, restricted to theorems with betweenness out of consideration and based on an entirely different principle, aims at giving a mechanical procedure which permits to prove quite non-trivial theorems in elementary geometry even by hands.