# zbMATH — the first resource for mathematics

Computer theorem proving for verifiable solving of geometric construction problems. (English) Zbl 1434.03032
Botana, Francisco (ed.) et al., Automated deduction in geometry. 10th international workshop, ADG 2014, Coimbra, Portugal, July 9–11, 2014. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 9201, 72-93 (2015).
Summary: Over the last sixty years, a number of methods for automated theorem proving in geometry, especially Euclidean geometry, have been developed. Almost all of them focus on universally quantified theorems. On the other hand, there are only few studies about logical approaches to geometric constructions. Consequently, automated proving of $$\forall \exists$$ theorems, that correspond to geometric construction problems, have seldom been studied. In this paper, we present a formal logical framework describing the traditional four phases process of geometric construction solving. It leads to automated production of constructions with corresponding human readable correctness proofs. To our knowledge, this is the first study in that direction. In this paper we also discuss algebraic approaches for solving ruler-and-compass construction problems. There are famous problems showing that it is often difficult to prove non-existence of constructible solutions for some tasks. We show how to put into practice well-known algebra-based methods and, in particular, field theory, to prove RC-constructibility in the case of problems from Wernick’s list.
For the entire collection see [Zbl 1316.68005].

##### MSC:
 03B35 Mechanization of proofs and logical operations 51M15 Geometric constructions in real or complex geometry 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
##### Software:
ArgoCLP; gcl; GCLC; OpenGeoProver; RegularChains
Full Text: