Computer theorem proving for verifiable solving of geometric construction problems

Abstract

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 ∀∃ 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.