ArgoTriCS–automated triangle construction solver

Abstract

In this paper, a method for automatically solving a class of straightedge-and-compass construction problems is proposed. These are the problems where the goal is to construct a triangle given three located points. The method is based on identifying and systematising geometric knowledge, a specific, restricted search and handling redundant or locus-dependent instances. The proposed method is implemented and the current implementation can solve a large number of triangle construction problems. To our knowledge this is the first systematic automated construction solver focused on solving problems from the corpus given. This is also the first approach that considers proving correctness of generated constructions (using external automated theorem provers).