Gröbner bases in geometry theorem proving and simplest degeneracy conditions.
Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group. Then, we prove that, using the notations of Borsuk and Szmielew in [3] “Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.” (Existence Statement 52 and Existence Statement 53) [3]. Or,...
Der Artikel ist eine Vorsetzung des ersten Teiles des Artikels und ist der Analyse und der Synthese der helikoidalen Bewegungen gewidmet. Im der Analyse der helikoidalen Bewegungen gewidmeten Teil sind die helikoidale Bewegungen als die Zweischraubenbewegungen charakterisiert und es sind die Invarianten der helikoidalen Bewegungen gefunden. Im, der Synthese der helikoidalen Bewegungen gewiemeten, Teil sind alle helikoidalen Bewegungen, die eine ebene oder gerade oder sphärische Punkttrajektorie...