Mechanical Theorem Proving in Geometries: Basic Principles

به نظر می رسد شکی وجود ندارد که هندسه از فعالیت های عملی مانند مشاهده آب و هوا و بررسی زمین نشات می گیرد. اما شیوه ها، روش ها و راه های مختلفی وجود دارد که تجربیات گوناگون را به سطح تئوری رساند تا در نهایت علم را تشکیل دهند. اف. انگلس گفت: "هدف ریاضیات مطالعه فرم های فضا و روابط کمی دنیای واقعی است." در زمان یونانیان باستان، دو روش مختلف برای برخورد با هندسه وجود داشت: یکی، که با «عناصر» اقلیدس، صرفاً روابط منطقی میان موجودات هندسی را دنبال می‌کرد و روابط کمی را کاملاً حذف می‌کرد تا نظام بدیهی هندسه را ایجاد کند. این روش به مدلی از روش های کسر در ریاضیات تبدیل شده است. دیگری، که توسط کار مربوطه ارشمیدس نشان داده شده است، بر مطالعه روابط کمی اجسام هندسی و همچنین معیارهای آنها مانند نسبت محیط دایره به قطر آن و مساحت یک سطح کروی و یک بخش سهموی اگرچه این رویکردها در سبک متفاوت هستند، ویژگی‌های خاص خود را دارند و دیدگاه‌های متفاوتی را در توسعه هندسه منعکس می‌کنند، هر دو سهم بزرگی در توسعه ریاضیات داشته‌اند. توسعه هندسه در چین همیشه به روابط کمی مربوط می شد.

There seems to be no doubt that geometry originates from such practical activ­ ities as weather observation and terrain survey. But there are different manners, methods, and ways to raise the various experiences to the level of theory so that they finally constitute a science. F. Engels said, "The objective of mathematics is the study of space forms and quantitative relations of the real world. " Dur­ ing the time of the ancient Greeks, there were two different methods dealing with geometry: one, represented by the Euclid's "Elements," purely pursued the logical relations among geometric entities, excluding completely the quantita­ tive relations, as to establish the axiom system of geometry. This method has become a model of deduction methods in mathematics. The other, represented by the relevant work of Archimedes, focused on the study of quantitative re­ lations of geometric objects as well as their measures such as the ratio of the circumference of a circle to its diameter and the area of a spherical surface and of a parabolic sector. Though these approaches vary in style, have their own features, and reflect different viewpoints in the development of geometry, both have made great contributions to the development of mathematics. The development of geometry in China was all along concerned with quanti­ tative relations.