CAT(0) is an algorithmic property (Q1768266)

An \(M_\kappa\)-complex is a connected cell complex \(K\) formed from polyhedral cells of the model space with constant curvature \(\kappa\). Cells of the complex \(K\) are glued by isometries along faces. The authors prove that if \(\mathcal S\) is a finite collection of shapes with curvature \(\kappa\), then there exists a finite list of configurations \(\mathcal C\) such that any \(M_\kappa\)-complex \(K\) with the set of shapes in \(\mathcal S\) is locally \(\text{CAT}(\kappa)\) if and only if it avoids configurations from \(\mathcal C\). An explicit algorithm which determines whether or not a finite \(M_\kappa\)-complex is locally \(\text{CAT}(\kappa)\) is described. The authors use a special case of Tarski's theorem stating that given a Boolean combination of polynomial equations and inequalities in \(n\) variables there is an algorithm which decides whether this system has a solution.