<正> 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 o
