Abstract
At the end of 1976 and the beginning of 1977, the author discovered a mechanical method for proving theorems in elementary geometries. This method can be applied to various unordered elementary geometries satisfying the Pascalian Axiom, or to theorems not involving the concept of ‘order’ (e.g., thatc is ‘between’a andb) in various elementary geometries. In Section 4 we give the detailed proofs of the basic principles underlying this method. In Sections 2 and 3 we present the theory of well-ordering of polynomials and a constructive theory of algebraic varieties. Our method is based on these theories, both of which are based on the work of J. F. Ritt. In Section 5 we use Morley's theorem and the Pascal-conic theorem discovered by the author to illustrate the computer implementation of the method.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Hilbert, D.,Grundlagen der Geometrie, Teubner (1899).
Ritt, J. F.,Differential Equation from the Algebraic Standpoint, Amer. Math. Soc. (1932).
Ritt, J. F.,Differential Algebra, Amer. Math. Soc. (1950).
WuWen-tsün, ‘On the decision problem and the mechanization of theorem proving in elementary geometry’,Scientia Sinica 21 159–172 (1978).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Wen-Tsun, W. Basic principles of mechanical theorem proving in elementary geometries. J Autom Reasoning 2, 221–252 (1986). https://doi.org/10.1007/BF02328447
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02328447