ABSTRACT. Unknot recognition is one of the fundamental questions in low dimensional topology. In this work, we show that this problem can be encoded as a validity problem in the existential fragment of the first-order theory of real closed fields. This encoding is derived using a well-known result on \su representations of knot groups by Kronheimer-Mrowka. We further show that applying existential quantifier elimination to the encoding enables an \unknot algorithm with a complexity of the order $2^{\OO(n)}$, where $n$ is the number of crossings in the given knot diagram. Our algorithm is simple to describe and has the same runtime as the currently best known unknot recognition algorithms. This leads to an interesting class of problems, of interest to both SMT solving and knot theory.