  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(2)
representations of knot groups by Kronheimer-Mrowka. We further show that
applying existential quantifier elimination to the encoding enables an UnKnot
Recogntion algorithm with a complexity of the order $2^{\mathcal{O}(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.
