zbMATH — the first resource for mathematics

On the need of radical ideals in automatic proving: A theorem about regular polygons. (English) Zbl 1195.68094
Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 157-170 (2007).
Summary: The paper deals with the problem of finding a natural geometry problem, that is, not specifically built up for the only purpose of having some concrete property, where the hypothesis is not described by a radical ideal. This problem was posed by Chou long ago. Regular polygons in the Euclidean space \(E ^{d }\) and their existence in spaces of various dimensions are studied by the technique of Gröbner bases. When proving that regular pentagons and heptagons span spaces of even dimension one encounters the case that the ideal describing the hypotheses is not radical. Thus, in order to prove that \(H\Rightarrow T\) one needs to show that \(T\) belongs to the radical of the ideal describing \(H\).
For the entire collection see [Zbl 1132.68006].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51M20 Polyhedra and polytopes; regular figures, division of spaces
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
68W30 Symbolic computation and algebraic computation
Full Text: DOI